Syntactic Entailment

Axioms

5. 
   (where is any formula with no bound occurrence of )
6. 
   ( is a formula with and is a term no variable of which occurs bound in )
7. 
   ( are formulae, , does not occur free in )

Rules of deduction

Modus ponens (MP): from and , can deduce
Generalisation (Gen): from with , can deduce provided does not occur free in any premiss used in the proof of

Definition

Let be a set of formulae in a language and be a formula in . A proof of from is a finite sequence in s.t. and for every :

1. either is an axiom, or
2. is a premiss (member of ), or
3. follows from modus ponens
4. follows by Generalisation (, s.t. , is not free in any premiss for )
   We write .

Deduction Theorem