Deduction Theorem

Let be a set of formulae in a first-order Language . Let , be formulae in . Then if and only if

Proof

Assume . Write down a proof of from and add the lines

to obtain a proof of from

Now assume . Let be a proof of from We prove by induction on that Induction hypothesis at -th step: For all we have s.t. if a variable does not occur free in any premiss in the proof of from then must not occur free in any premiss used in the proof of from . We now prove that in four cases

Case 1

is an axiom or Then

is a proof of from .

Case 2

Then since in Propositional Logic

Case 3

follows by (MP), i.e. there are some s.t. By induction hypothesis, we can write down proofs of and from and append the lines

Case 4

follows by (Gen) i.e. there is some where is where and didn’t occur free in any premiss in We have two further cases

Case 4a

occurs free in Then is not amongst so this is a proof from . We append the lines

Case 4b

does not occur free in By induction hypothesis, there’s a proof of from which is s.t. does not occur free in any premiss used. We append the lines

to obtain a proof of from

In all cases, it’s easy to check that the induction hypothesis before th step is satisfied.