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
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
.