- is true

*All the axioms are tautologies.
*

*Let
be called the set of hypotheses or premises. A
proof of a conclusion from is a finite set
with and each is either
*

- an axiom
- a member of
- such that there exist

*Then
( proves or syntactically implies ). If
then is a theorem (written ).
*

*
*

1 | Axiom 2 | |

2 | Hypothesis | |

3 | Axiom 1 | |

4 | Modus ponens on 2, 3 | |

5 | Modus ponens on 4,1 | |

6 | Hypothesis | |

7 | Modus ponens on 6,5 |

1 | Axiom 2 | |

2 | Axoim 1 | |

3 | Modus ponens on 2,1 | |

4 | Axiom 1 | |

5 | Modus ponens on 4,3 |

*Let
, . Then
iff
.
*

Hypothesis | |

Modus ponens |

Thus proving from .

Let be a proof of from . Show that for every .

If certainly as .

Otherwise if is an axiom or , write

Axiom or Hypothesis | |

Axiom 1 | |

Modus ponens |

So .

Otherwise was got from Modus Ponens, i.e. there exist such that . By induction on assume and so write

Axiom 2 | |

Modus ponens | |

Modus ponens |

*To show
show
using
modus ponens twice.
*

*Let
, then
implies
.
*

Certainly axioms (are tautologies) and elements of are true. Also modus ponens: if and then . So for all in a proof of from .

*
is inconsistent if
. Otherwise it is
consistent.
*

*A set
is deductively closed if it contains all its
consequences. If
then .
*

*Let
be consistent. Then has a model.
*

Claim. For any consistent and any at least one of and is consistent.

Proof of claim. Suppose is inconsistent. Then . So so and prove the same things so is consistent.

is countable. Let be an ordering of . Let . Let be or choosing one which is consistent. Let . Then for each at least one of or . is consistent because proofs are finite. Also deductively closed. If then does not prove (as ).

Define . is a valuation. Proof. . If then , . So so . If then so so . If then so . Enough to show . That is, .

Hypothesis | |

Axiom 1 | |

Axiom 3 |

So . So is a valuation. So there is a model for .

*Previous theorem used fact that is countable (so that is
countable) but this is not necessary by Zorn's lemma (next chapter).
*

*Let
, . Then
implies
.
*

*Let
, . Then
iff
.
*