Deduction Theorem Intuition

The symbol $\vdash$ express derivability in the calculus.

The syntax is:

$Δ ⊢ φ$, where $Δ$ is a set of formulas: the set of assumptions (or premises) used in the derivation of the conclusion $\varphi$.

Thus it is correct to write $Δ \cup \{ A \}$.

The *Deduction Theorem is a meta-theorem, i.e. a result about properties of the calculus and not a formula proved in the calculus.

The correct formulation of the Deduction Theorem is:

if we have a derivation $Δ ∪ \{ A \} ⊢ B$, then we can build a new derivation: $Δ ⊢ A→B$.


We have here two "levels": the level of the calculus, working with formulas written with the connectives. One of them is the conditional: $\to$.

Thus, $\to$ is a symbol of the language used in the calculus.

The second "level" is the meta-theory, where we have the relation of derivability between a set of formulas and a formula.

Thus, $\vdash$ is a symbol of the meta-language used to express the properties of the calculus.

The calculus is purely symbolical: it is made of "objects" called formulas, rules and sequences of formulas: derivations.

In the meta-theory we prove mathematical theorems about the calculus and its properties.

One of these theorems is the DT, expressing the fact that from an existing derivation (in the calculus) we can manufacture a new derivation.

The language of meta.theory is the usual math-English made of a mixture of symbols, like $\vdash$ and natural language; thus, there is no real advantage to use $\to$ in palce of "if..., then...".

But we can find mathematical logic textbooks where $\to$ is used as connective and $\Rightarrow$ is used in the meta-language to abbreviate "implies".


No, you really shouldn't write $(\Delta \cap \{ A \} \vdash B) \vdash (\Delta \vdash A \rightarrow B)$, because the $\vdash$ in $\Delta \cap \{ A \} \vdash B$ as well as in $\Delta \vdash A \rightarrow B$ is about the derivability of statements from other statements relative to some proof system (and so it would be best to use something like $\vdash_P$ where $P$ is the proof system you are considering), while the $\vdash$ you use in the middle is not at all that. So you really should just say that:

"If $\Delta \cap \{ A \} \vdash B$ then $\Delta \vdash A \rightarrow B$"

Likewise, I would not use $(\Delta \cap \{ A \} \vdash B) \rightarrow (\Delta \vdash A \rightarrow B)$ since $\rightarrow$ is a symbol used in a particular logic system that the derivability statements are about. Indeed, the $\rightarrow$ in $\Delta \vdash A \rightarrow B$ is part of the logical expression $A \rightarrow B$ that is claimed to be derivable from the set of formulas $\Delta$. But the $\rightarrow$ you would put between $(\Delta \cap \{ A \} \vdash B)$ and $\Delta \vdash A \rightarrow B$ is not at all combining two logic formulas, but rather two meta-logical statements about derivability. So you really don't want to mix those up!

And yes, in logic we use $\rightarrow$ to try and capture 'if .. then ...' expressions, but the match is not perfect. The $\rightarrow$ is really just a mathematically defined truth-function, but the English conditional isn't always used in that way. Look up "Paradox of Material Implication", e.g: https://en.wikipedia.org/wiki/Paradoxes_of_material_implication!

Finally, the $A$ is a statement/formula, not a sequent.