# Formalizing the deduction theorem in the metatheory

Here is the deduction theorem, in the "$$\Leftrightarrow$$" version (I'm considering it for first order logic): $$\Delta \cup \lbrace A \rbrace \vdash \lbrace B \rbrace \Longleftrightarrow \Delta \vdash \lbrace A \rightarrow B \rbrace$$ where $$\Delta$$, $$\lbrace A \rbrace$$ and so on are sets of formulas. I'm taking set theory (ZFC, ZF or whatever) as the metatheory.

This metatheorem states that if we can prove $$B$$ assuming $$\Delta$$ and $$A$$, than we can prove $$A \rightarrow B$$ assuming only $$\Delta$$ and viceversa. With this metatheorem, if we want to prove a theorem in the form $$A \rightarrow B$$ we don't need to directly prove the implication, we just have to assume the formulas in $$\Delta \cup \lbrace A \rbrace$$ and derive $$B$$: that will be equivalent to prove $$A \rightarrow B$$ from $$\Delta$$.

This metatheorem is used in the everyday mathematics. In fact in most cases, when we want to prove an implication in the form $$A \rightarrow B$$ we always say "Assume $$A$$," and then with a chain of inferences we conclude $$B$$, and that is by the deduction theorem a proof of $$A \rightarrow B.$$

Now here is the question: in our metatheory (in this case it's set theory), we have proved an implication "$$\Longrightarrow$$" (precisely a double implication $$\Longleftrightarrow$$); the proofs of the deduction theorem that I've seen start always assuming "suppose $$\Delta \cup \lbrace A \rbrace \vdash \lbrace B \rbrace$$" and then they finish saying "...then $$\Delta \vdash \lbrace A \rightarrow B \rbrace$$" and so (doing that even in the other direction), we prove a metatheorem in the form $$\psi \Longleftrightarrow \phi$$... but aren't we implicitly assuming the deduction theorem "for our metatheory", since we proved an implication $$\psi \Longrightarrow \phi$$, assuming $$\Delta \cup \lbrace A \rbrace \vdash \lbrace B \rbrace$$ and then deriving $$\Delta \vdash \lbrace A \rightarrow B \rbrace$$?

Is this observation correct or am I wrong? From what I know I guess that since in mathematics we can't start formalizing notions from no bases and we just have to assume something in our metatheory, in a certain sense we have to "assume" the deduction theorem in our metatheory to prove it for the object theory, but I'm not sure.

Tell me what you think and thanks in advance :D

We have the logical calculus $$\mathsf {PC}$$ (a formal system) and we have the usual definition of derivation from assumptions : $$\Delta \vdash_{\mathsf {PC}} \varphi$$, that we read as :

"there is a a finite sequence $$\langle D_1, \ldots, D_n \rangle$$ of formulas of $$\mathsf {PC}$$, where $$D_n$$ is $$\varphi$$ and ...".

The part : "if $$\Delta \vdash_{\mathsf {PC}} (A \to B)$$, then $$\Delta \cup \{ A \} \vdash_{\mathsf {PC}} B$$" is proved this way.

We assume having a derivation $$D$$ from $$\Delta$$ such that $$D_n$$ is $$(A \to B)$$.

Consider the new set of assumptions $$\Delta' = \Delta \cup \{ A \}$$ and produce the new derivation $$D'$$ starting from $$\Delta'$$.

Copy-past all $$D$$ and add a new line $$D_{n+1}$$ with $$B$$ justified from $$\Delta'$$ and $$D_n$$ by an application of the modus ponens rule of inference.

The result will be the requested derivation.

In what sense we have used the $$\text {Deduction Theorem}$$ in the above proof ?

The $$\text {DT}$$ is a statement about the logical calculus $$\mathsf {PC}$$ and expresses a property of the "mathematical object" $$\vdash_{\mathsf {PC}}$$.

We have proved it with a "usual" mathematical proof, using the definition of the mathematical objects involved : formula, derivation, rule of inference.

The theorem has the logical form : "if..., then..." and in order to prove it we have used the ubiquitous Conditional proof technique.

Thus,

in order to prove the $$\text {Deduction Theorem}$$, we have used the Conditional proof technique in the meta-theory.

The $$\text {Deduction Theorem}$$, in turn, establish the formal counterpart of the conditional proof for the formal system $$\mathsf {PC}$$.

But the meta-theory is not a formal system; it is "plian" mathematics.

It is useful to compare with the calculus of Natural Deduction, where the $$\text {DT}$$ is built-in into the rules for managing the $$\to$$ connective.

• To me it looks like we are assuming the deduction theorem for our metatheory because it is proved an "if... then..." statement assuming the "if..." condition ($\Delta \cup \lbrace A \rbrace \vdash \lbrace B \rbrace$) and then deriving the "then..." conclusion ($\Delta \vdash \lbrace A \rightarrow B \rbrace$) and viceversa. – Luis Orion Mar 5 at 13:39