Another Proof for the Propositional Deduction Theorem

This is an appendix to Chapter I of our notes, “Post’s Theorem and other tools”. We prove here the Deduction Theorem of Propositional Logic, without doing the infamous induction on theorems (that is how we proved the Deduction Theorem in Chapter I). We will here rely instead on Post’s (completeness) theorem.

0.1 Metatheorem. For any set of formulas Γ and any individual formulas A and B, if Γ, A ⊢ B, then also Γ ⊢ A ⇒ B.

Proof. Let

C_{1}, C_{2}, C_{3}, …, C_{m}, B  (1)

be a proof of B from assumptions Γ and A, and let

D_{1}, …, D_{r}  (2)

be all those formulas among the ones in (1) that are formulas of Γ.

Remember that at any step of a proof—such as the proof in (1)—we may have written down a formula from Γ ∪ {A}.

It follows (definition of “theorem-calculation/proof”!) that

D_{1}, …, D_{r}, A ⊢ B  (3)

In (1), above, we only have used the part of Γ that consists of the formulas in (2). Thus, we could have written that proof even if we did NOT have all of Γ at our disposal, but just had the part D_{1}, …, D_{r}. That is what (3) says.

Of course, A is part of the assumptions—other than those in Γ—towards proving B, and it may also have been written down a number of times, as we were writing (1) down. Thus, we must not—and did not—forget to write A down as an assumption in (3). All we have managed to do was to cut down Γ to a finite size, by discarding what we did not need in the proof of B.

Now, by soundness, (3) yields

D_{1}, …, D_{r}, A ⊧ B  (4)

Thus,

D_{1}, …, D_{r} ⊧ A ⇒ B  (5)

To see why (5) is correct, just take any state s such that

s(D_{1}) = s(D_{2}) = ⋯ = s(D_{r}) = \underline{t}  (6)

and show that

s(A ⇒ B) = \underline{t}  (7)

as well. Now, if s(A) = \underline{f} we get (7) via the TT for “⇒”. If on the other hand s(A) = \underline{t}, then, by (4) and (6), s(B) = \underline{t} as well, so, once again, the TT for “⇒” yields (7).

In short, (5) is correct.

By Post’s theorem (completeness),

D_{1}, …, D_{r} ⊢ A ⇒ B

hence, since {D_{1}, …, D_{r}} ⊆ Γ,

Γ ⊢ A ⇒ B

Done! □

0.2 Remark. At the end of the proof above we used “if Δ ⊢ A and if Δ ⊆ Γ, then Γ ⊢ A as well”. In Chapter I we proved this obvious metatheorem by induction on theorems.

It is “obvious” because it says that if I can prove something (A, let us say) from some assumptions (Δ, let us say), then I can still prove it if I add more assumptions (I will just NOT use the additional assumptions!)

This can be seen rigorously, without doing induction on theorems, by utilizing the concept of proof:

Suppose that

P_{1}, P_{2}, …, P_{n}, A  (8)

is a proof of A from Δ. Then, some of the P_{i} are formulas from Δ.

Now these formulas from Δ are also formulas from Γ, if Δ ⊆ Γ. Thus, (8) also qualifies as a proof from Γ!