|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, provides the standard model of theories such as .|
|is some theory (set of axioms) in the language|
|means that the theory entails the formula of by the usual rules of first-order logic.|
|means that the formula of is true in the standard model of .|
|where is a natural number denotes the representation in of ( with dashes).|
|where is any formula of , where the are terms of , and where the are variables, denotes the result of simultaneously substituting for in , taking care to avoid variable capture.|
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.