# rules of inference, language into metalanguage

There are rules of inference, e.g. in natural deduction they are listed. These rules follow the same rules than the logic language. If we see Modus ponens,

a → b, a ⊢ b

We can write for the same purpose,

((a → b) ∧ a) → b.

So, I don't understand what we gained by constructing the inference rules.

I guess that the switch from premises in logic language to the conclusion has to do with Metalanguage.

For example if we write

p ⊢ p,

what was said?

• You can type unicode ⊫ ⊢ ∨ ∧ → Commented Mar 14 at 8:59
• And yes, they are "recipes" in the meta-language. They are written as schema because they instruct us how to manipulate formulas of the object language. Commented Mar 14 at 9:00
• @MauroALLEGRANZA the first p is a premise and the second is the conclusion Commented Mar 14 at 10:06
• @Rushi I am typing with a phone and don't know how to use Unicode Commented Mar 14 at 10:07
• @MauroALLEGRANZA you write "to manipulate formula las". But I don't understand, formulas are defined by the operators, and, or, not, imply, etc. And the operators are defined by themselves. Moreover , if I write p, this says that p himself is true. May be that to say it's true is a false assumption, but the language contains in himself the content of "truthness". Commented Mar 14 at 10:44

The syntactical specifications of the language of propositional logic allows us to build formulae from propositional variables : p, q, ... and constants : ⊥,⊤ using the propositional connectives: ¬,∨,∧,→.

Thus, p → q is a formula, while, e.g. p+q is not.

With the symbol: α, φ ⊢ ψ we mean that the formula ψ is derivable in the propositional calculus from the premises α, φ, i.e. that starting with the premise we can "produce" the conclusion using a finite number of applications of rules of inference, like modus ponens.

The symbol φ ⊢ ψ is not a formula, but it expresses a relation between formulae of the calculus; is not a symbol of the language: it is not present in the syntactical specifications above.

The statements in the metalanguage express "facts" about the language and the calculus, and thus are not formulae of the language.

Rules of inference are necessary in order to "transform" formulae in input (the premises) into formulae in output: the conclusion.

They are "recipes" in the metalanguage, written as schema exactly because they instruct us how to manipulate formulae.

The symbol p ⊢ p expresses the fact (intuitively quite obvious) that from premise p we can derive the conclusion p.

• Thanks so much @Mauro. It's exactly my problem.. Commented Mar 14 at 14:57
• @kouty - you are welcome. Commented Mar 14 at 14:58

You write

We can write for the same purpose,

((a → b) ∧ a) → b

This is not accurate. What we really mean to write is

⊢ ((a → b) ∧ a) → b

In longer form

((a → b) ∧ a) → b

is just a term in logic, exactly like

1. a → b
2. a

are terms.
Whereas

⊢ ((a → b) ∧ a) → b

is a metalanguage claim about that term which could be long-form-articulated as

The term '((a → b) ∧ a) → b' is a tautology.

IOW the '⊢' is a crucial jump from the metalanguage into the object-language.