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.