R.D. Arthan
rda@lemma-one.com
![]() |
is the language of first-order Peano arithmetic (
![]() |
![]() |
is the set of natural numbers of day-to-day thought. Augmented with the usual operations of addition, multiplication and so on,
![]() ![]() |
![]() |
is some theory (set of axioms) in the language
![]() |
![]() |
means that the theory ![]() ![]() ![]() |
![]() |
means that the formula ![]() ![]() ![]() |
![]() |
where ![]() ![]() ![]() ![]() ![]() |
![]() |
where ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
We say
is ground-complete1
iff.
proves every ground formula that is true in the standard
model. Here by ``ground formula'' we mean a formula containing no variables
(and so, in particular, no quantifiers).
Intuitively, a ground-complete theory is one that ``knows its tables'': it can derive any formula of
whose truth follows purely by dint of arithmetic calculation on particular natural numbers.
A ground-complete theory need not be consistent, but a ground-complete theory
that is consistent cannot prove a false ground formula
(this is a special case of lemma 1 below).
Ground-completeness is enjoyed by
and by
many weaker theories such as Robinson's system
.
As usual,
is consistent iff. there is a formula
such that
,
or, equivalently, iff. there is no formula
for which both
and
;
is
-consistent iff. whenever
for some formula
,
there is at least one natural number,
,
for which
.
is complete if for every formula
,
either
or
.
An -consistent theory is certainly consistent: if
is
-consistent and
is any formula, then either
or for some natural number,
,
,
so there is at least one formula that
does not prove.
Since a prenex formula with a prefix of length
is quantifier-free and, as remarked above,
-consistent theories are consistent, the base case is given by lemma 1.
There are two cases for the inductive step: (a),
has the form
or, (b),
has the form
,
where, in either case,
has a shorter prefix than
,
so that the inductive hypothesis applies to
.
I.e., if
,
then
.
In case (a), from our assumptions,
,
and so, by first-order logic,
,
since
is
.
By the inductive hypothesis
.
But
is true in a model iff. its universal closure is; so
,
i.e.,
as required to complete the inductive step for case (a).
In case (b),
has the form
and,
by assumption,
,
i.e.,
.
By
-consistency, for some natural
number
,
.
But then, by the
completeness of
,
.
By the inductive hypothesis, this implies that
,
whence
,
i.e. we may conclude that
as required to complete the inductive step for case (b) and hence the proof of the lemma.
Our arguments have made unashamed use of the notion of the natural numbers as a given;
however, our ontological demands are really very modest and our means are no more demanding than our ends:
if first-order logic is to be admitted as a topic of philosophical study, then we must admit consideration of at least one countably infinite set, namely the language of the first-order theory in question.
The only coherent way to reject theorem 2 is to deny the law of the excluded middle and so claim that both its statement and its proof are meaningless.
If one admits classical first-order logic as offering a road to philosophical truth, then one must accept the theorem and read it as saying that there is exactly one -consistent
and complete extension of Peano arithmetic.