13
The FOPL proof calculus (with the logical axioms and rules described in the previous
chapter) is a
complete calculus: it proves all the logically valid formulas of FOPL. The
calculus can be viewed as a theory without special axioms. This empty theory is not a
complete theory: for instance, a simple formula like
∃x P(x) is not decidable. Thus the
calculus does not decide even simple arithmetic truths, for generally they are not logical
truths. It might seem that the calculus decides at least all the logical truths, since they are
provable. We will show as a consequence of Gödel’s first incompleteness theorem that the
problem of logical truth is also not decidable within FOPL.
To characterize arithmetic truths, we need some special axioms formulated in the
arithmetic language. As an example we adduce a theory Q, called Robinson’s arithmetic,
given by the following seven axioms:
∀x
(Sx
≠ 0)
∀
x∀
y
(Sx = Sy
→ x = y)
∀x
(x + 0 = x)
∀x∀y
(x + Sy = S(x + y))
∀x
(x * 0 = 0)
∀x∀y
(x* Sy = (x* y) + x)
∀x∀y
(x
≤ y = ∃z (z + x = y) )
The theory Q characterizes basic arithmetic operations (a successor of any number is not
equal to zero; adding zero to any number gives as a result the same number, etc.), and the
structure
N
is a model of the theory; Q is however a weak theory. General simple statements
like commutativity of adding or multiplying, i.e., sentences
∀x∀y (x+y = y+x) and
∀x∀y (x * y = y * x) cannot be proved in Q.
The theory Q proves only syntactically simple sentences. Syntactical complexity of a
sentence is determined by a number of alternating quantifiers. More precisely: We say that an
arithmetic formula
ϕ is formed from a formula ψ by a bounded quantification, if ϕ has one of
the following forms (the binary predicate symbol ‘<’ is being interpreted as the “less than”
relation, i.e., x < y abbreviates (x
≤ y) & ¬(x=y) ):
∀v (v < x → ψ), ∃v (v < x & ψ), ∀v (v ≤ x → ψ), ∃v (v ≤ x & ψ),
where v, x are distinct variables. Quantifiers of the above form are called bounded quantifiers.
A formula
ϕ is a bounded formula if it contains only bounded quantifiers. A formula ϕ is a
Σ
-
formula, if
ϕ is formed from bounded formulas using only conjunction, disjunction,
existential quantifier and any bounded quantifiers.
There is an interesting, rather non-trivial fact valid of Robinson’s arithmetic: Q is
Σ
-
complete; it proves all the
Σ-sentences that should be provable, i.e., the Σ-sentences true in
N
:
if
σ is a Σ-sentence such that
N
|=
σ, then Q |– σ.
If we extend the theory Q by the scheme of induction axioms:
[
ϕ(0) & ∀x (ϕ(x) → ϕ(Sx))] → ∀x ϕ(x),
we obtain the theory PA called
Peano arithmetic. Note that we added a
scheme of
infinitely
many axioms which can be obtained by substituting a formula for
ϕ. Yet this theory is
“reasonable”, it conforms to finitism: we added a “geometrical pattern” of formulas. Thus in
PA we have a finite number of structural relations in which the formulas stand to each other,
and proving in the theory does not involve a procedure that would make reference to actual
infinity.
14
The structure
N
is a standard model of PA. Each number n
∈ N is denoted by a term of
the arithmetic language, namely the term SS…S0 (the n
th
successor of the constant 0), called
the
n
th
–numeral. We use an abbreviated notation: n.
Peano arithmetic is rather a strong theory and many laws of arithmetic are provable in it;
however, it is not a complete theory: there is a sentence
ϕ that is true in
N
but not provable in
PA. And, of course,
¬ϕ is not provable as well, because ¬ϕ is not true in
N
and PA proves
only sentences true in its models
.
You might attempt at adding some more “geometrical
patterns of formulas” as axioms, so that to complete the theory. Providing a finite number of
such ‘structural relations’ (i.e. axioms or axiom schemas) could be found, Hilbert’s goal
would be completed. Unfortunately it is not possible. Incompleteness is not a special feature
of Peano arithmetic: any “reasonable” theory of arithmetic is incomplete. Though there is a
naïve complete theory of arithmetic (called
true arithmetic), it cannot meet the finitistic
demands on involving only such procedures that make no reference either to an infinite
number of structural properties of formulas or to an infinite number of operations on
formulas. To state these results more precisely, we have to define what is meant by a
reasonable theory:
A theory T is recursively axiomatized if there is an algorithm
17
that for any formula
ϕ decides
whether
ϕ is an axiom of the theory or not.
We also need a notion of arithmetic soundness: A theory T is arithmetically sound, if all
arithmetic sentences provable in T are valid in
N
.
Gödel’s first theorem on incompleteness: let T be a theory that contains Q (i.e., the language
of T contains the language of arithmetic and T proves all the axioms of Q). Let T be
recursively axiomatized and arithmetically sound. Then T is an incomplete theory, i.e., there
is a sentence
ϕ that is not decidable in T: T proves neither ϕ nor ¬ϕ.
Note: Actually, Gödel proved the theorem on the assumption of the theory being
omega-
consistent. Omega-consistency is a technical concept which applies to a theory T if, for no
property P, (i) T proves the general proposition that there exists some natural number with the
property P, but (ii) for every specific natural number n, T proves that n does not have the
property P. This is mostly of technical interest, since all true formal theories of arithmetic,
i.e., theories the axioms of which are true in
N
, are omega-consistent. Note that omega-
consistency implies consistency, but not vice versa. Later J. Barkley Rosser strengthened the
theorem and proved that the assumption on T being arithmetically sound (or
N
being a model
of T) could be weakened by the assumption on consistency of T.
It should be clear now what Gödel proved: it is not possible to find a recursively
axiomatized consistent theory, in which all the true arithmetic sentences about natural
numbers could be proved. Feasibility of a theory certainly involves the ability to recognize
whether a formula is an axiom or not, i.e., the axioms of the theory have to be recursively
defined; otherwise we could not execute the proof. Hence, completeness of arithmetic and
recursive axiomatization are two distinct goals which cannot be met both together.
In what follows we just outline the main ideas of the proof. First we have to introduce
Gödel’s method of arithmetization of metamathematics. Well-formed formulas are sequences
of symbols, proofs are sequences of formulas, and the set of these sequences is countable.
Hence it is possible to define an unambiguous numbering of all the formulas and proofs
(expressed in the language of a recursively defined theory T). Gödel defined a one-to-one
17
We use the notion of algorithm in an intuitive way here: a finite procedure that for any input formula
ϕ gives a
“Yes / No” output in a finite number of steps. Due to Church’s thesis it can be explicated by any computational
model, e.g., Turing machine.