first order arithmetic, Peano, Dedekind, Grassmann, arithmetic, formal, axiomatic, axioms, Presburger

Back to title page.

Is the notion of natural numbers independent in mathematics, or it depends on other, more complicated mathematical notions - the notion of real numbers, and Cantor's notion of arbitrary infinite sets? I.e., could we define natural numbers separately from all the other mathematics? At first glance, it seems that the answer "must" be positive. If natural numbers are the most fundamental mathematical concept (more fundamental than real numbers and Cantor's infinite sets), then an independent definition of them "must" be possible?

One more reason to search for an independent formalization of natural numbers are paradoxes of set theory. Zermelo-Fraenkel's set theory does not allow you to derive Russell's paradox, Cantor's paradox and Burali-Forti paradox. Still, who could guarantee that there are no other inconsistencies? Still, have you ever thought about paradoxes in arithmetic of natural numbers? Natural number system seems to be the most reliable branch of mathematical reasoning.

So, let us try. Our work will result in the so-called Peano axioms. This terminology is one of numerous strange naming traditions in mathematics, since: "It is rather well-known, through Peano's own acknowledgment, that Peano borrowed his axioms from Dedekind and made extensive use of Grassmann's work in his development of the axioms." (see Hao Wang [1957], p.145).

Indeed, about 90% of the entire work were done already by Hermann Grassmann in his book published in 1861:

**H. Grassmann.** Lehrbuch der Arithmetik, 1861

The traditional recursive definitions of addition and multiplication are due to Grassmann (see Hao Wang [1957]):

x+0=x; x+(y+1)=(x+y)+1;

x*0=0; x*(y+1)=(x*y)+x.

In this way addition and multiplication of natural numbers are
derived from one single argument operation x+1. By using these
definitions Grassmann proved all the other principal properties
of arithmetical operations (associativity, commutativity etc.).
Grassmann's axioms included also the **induction principle**
(see P3 below). Of course, the hard part of the work was not the
invention of the above simple formulas, but the idea that they
are necessary.

Richard Dedekind made another attempt in his essay published in 1888:

**R. Dedekind.** Was sind und was sollen die Zahlen.
Braunschweig, 1888 (see also http://thoralf2.uwaterloo.ca/htdocs/scav/dedek/dedek.html)

Dedekind's intention was not axiomatization of arithmetic, but - giving an "algebraic" characterization of natural numbers as a mathematical structure. He writes in a letter to Dr. H. Keferstein (dated 27 February 1890, I will quote English translation from Hao Wang [1957]):

"[...]

(1) The number sequence N is a system of individuals or elements which are called numbers. This leads to a general study of systems as such (section 1 of my essay).

(2) The elements of the system N stand in a certain relation to one another, they are in a certain order determined, in the first place, by the fact that to each definite number n, belongs again a definite number n', the number which succeeds or is next after n. This leads to the consideration of the general concept of a mapping F of a system (section 2). Since the image F(n) of each number n is again a number n' and therefore F(N) is a part of N, we are here concerned with the mapping F of a system N into itself. And so this must be studied in its full generality (section 4).

(3) Given distinct numbers a, b, their successors a', b' are also distinct; the mapping F has therefore the character of distinctness or similarity (section 3).

(4) Not every number is successor n', i.e. F(N) is a proper part of N; this (together with the preceding paragraph) constitutes the infinitude of the number sequence N (section 5).

(5) More precisely, 1 is the only number which does not lie in F(N). Thus we have listed those facts which you regard as the complete characterization of an ordered simply infinite system N.

(6) But I have shown in my reply that these facts are still far from being adequate for a complete characterization of the nature of the number-sequence. Indeed, all these facts also apply to every system S which, in addition to the number-sequence N, contains also a system T of arbitrary elements t. One can always define the mapping F so as to preserve the character of similarity and so as to make F(T)=T. [...] What must we now add to the facts above in order to cleanse our system S from such alien intruders t [...]? This was one of the most difficult points of my analysis and its mastery required much thought. [...] I shall say: an element n of S belongs to the sequence N if and only if n is an element of every such part K of S which possesses the two properties (i) that the element 1 belongs to K and (ii) that the image F(K) is part of K. [...] Only after this addition is the complete character of the sequence N determined. [...]

For a brief period last summer (1889) Frege's "Begriffschrift" and "Grundlagen der Arithmetik" came, for the first time, into my possession. I noted with pleasure that his method of defining a relation between an element and another which it follows, not necessarily immediately, in a sequence, agrees in essence with my concept of chains [...]. Only one must not be put off by his somewhat inconvenient terminology.

[...]"

Dedekind refers here to the following essay by Gottlob Frege, where a similar (to Dedekind's) analysis of the natural number system is given:

**G.Frege.** Die Grundlagen der Arithmetik. Eine
logisch-mathematische Untersuchung ueber den Begriff der Zahl.
Breslau, 1884, 119 pp. (see also http://thoralf2.uwaterloo.ca/htdocs/scav/frege/frege.html)

In section 10 of his essay Dedekind proves that his
characterization of the natural number system is complete in the
sense that any two systems N_{1} and N_{2}
satisfying the conditions (1)-(6) are isomorphic (for details see
Appendix 1).

Giuseppe Peano made the next step in 1889 - he converted Dedekind's conditions (1)-(6) into axioms:

**G.Peano.** Arithmetices pricipia, nova methodo exposita.
Torino, 1889, 40 pp. (see English translation in Heijenoort [1967], see also
online comments at http://thoralf2.uwaterloo.ca/htdocs/scav/peano/peano.html).

The modern version of Peano axioms can be put as follows. Let
variables x, y, … range over natural numbers, and let 0 denote
the number "zero", Sx - denote the operation x+1, and
let the variable F range over **sets** of natural numbers.
Then the following statements are called Peano axioms:

**P1) **Ax~(0=Sx) (a part of Dedekind's condition (5)),

**P2)** AxAy(~(x=y) -> ~(Sx=Sy) (Dedekind's condition
(3)),

**P3) **0 in F & Ax(x in F -> Sx in F)) -> Ax(x
in F) (Dedekind's condition (6), or the induction principle).

We do not need the remaining conditions (1), (2) and (4) in our list, since they can be derived from the general logical axioms and identity axioms.

One can prove easily that any two "systems" N_{1}
and N_{2} satisfying the axioms (P1)-(P3) are isomorphic
(see Appendix 1).

One of such "systems" can be constructed in the set theory ZF. Let us define 0 as the empty set, Sx - as xU{x}, and let variables range over the set w. Then the axioms P1-P3 can be proved as theorems of ZF (see Exercise 2.15). Still, this is not the kind of formalization we are searching for. Using of arbitrary sets of natural numbers seems to be less dangerous than using of Cantor's general notion of arbitrary infinite sets. Still, there is one-to-one correspondence between sets of natural numbers and real numbers. Can the notion of natural numbers depend on the notion of real numbers? If we believe that it cannot depend, we must try to formalize natural numbers without reference to arbitrary sets of these numbers.

One of the ways to do this would be replacing the axiom P3 (induction principle) by an axiom schema where the set variable F is "instantiated" by formulas in some formal language L. I.e. let us restrict the induction principle P3 to some kind of "definable" sets F. It appears that the power of the theory we obtain in this way depends essentially on the language L.

The minimum version of the language L (let us denote it by L_{0})
would contain: the constant letter 0, the function letter S, and
the predicate letter "=". In this language the notion
of term is defined as follows:

a) 0 and any variable is a term;

b) If t is a term, then St also is a term.

Hence, we have here only two types of terms: SS...S0 (i.e.
representations of particular natural numbers) and SS...Sx (i.e.
representations of functions x+n). Atomic formulas in the
language L_{0} are built by the following rule:

c) If t_{1} and t_{2} are terms, then (t_{1}=t_{2})
is an atomic formula.

Formulas of the language L_{0} are built from atomic
formulas by using logical connectors and quantifiers.

Let us denote by PA_{0} the theory in the language L_{0}
having the following specific axioms:

**P1**_{0}**) **Ax~(0=Sx) (the same as
P1),

**P2**_{0}**)** AxAy(~(x=y) ->
~(Sx=Sy) (the same as P2),

**P3**_{0}**)** B(0) &
Ax(B(x)->B(Sx)) -> AxB(x),

where B is arbitrary formula of the language L_{0}
containing x as a free variable, and (maybe) some other free
variables (parameters). I.e. P3_{0} is the axiom schema
replacing the axiom P3.

PA_{0} is a very poor theory.

**Exercise 3.1.** Prove that PA_{0} cannot
"express" the relationship x<y. **Hints:** a) We
would say that a formula LESS(x, y) in the language L_{0}
"expresses" the assertion "x<y", iff:

PA_{0} proves: ~LESS(x, x),

PA_{0} proves: LESS(x, Sx),

PA_{0} proves: LESS(x, y) & LESS(y, z) ->
LESS(x, z).

b) As the first step, prove that no formula LESS(x, y) in the
language L_{0} can possess the property: LESS(m, n) is
"true" iff the number m is less than the number n.

Since x<y can be "expressed" as Ez(x+Sz=y), the
addition of natural numbers also cannot be discussed in PA_{0}.

We can try to extend PA_{0} by: a) adding to the
language L_{0} the "missing" predicate letter
"<", and b) adding to PA_{0} three new
axioms: ~(x<x), x<Sx, x<y & y<z -> x<z.
Unfortunately, in this way we obtain a theory PA_{00} in
which the addition of natural numbers still cannot be discussed
(see Hilbert, Bernays
[1934], section 7.4). I.e. none of the formulas PLUS(x, y, z)
in the language of PA_{00} can possess the properties:

a) PA_{00} proves: PLUS(x, 0, x) (i.e. x+0=x),

b) PA_{00} proves: PLUS(x, y, u) -> PLUS(x, Sy, Su)
(i.e. x+Sy=S(x+y)).

As the next step, let us try to extend PA_{0} by
adding to the language L_{0 }the "missing"
function letter "+" and the constant letter 1. Then we
will no more need the function letter S (the function Sx can be
represented as x+1) and the predicate letter "<" (it
can be "expressed" as Ez(x+z+1=y)). Let us denote this
new language by L_{1}. Terms of L_{1} are defined
as follows:

a) The constants 0 and 1, and all variables are terms.

b) If t_{1} and t_{2} are terms, then (t_{1}+t_{2})
also is a term.

Atomic formulas of L_{1} are built as (t_{1}=t_{2}),
where t_{1} and t_{2} are terms. Since we can
use, for example, the expression 2*x-3*y+1=0 as a shortcut for
x+x+1=y+y+y, we can say simply that atomic formulas of L_{1 }are
linear Diophantine equations.

After this, we must modify and extend the axioms of PA_{0}:

**P1**_{1}**)** ~(0=x+1),

**P2**_{1}**)** ~(x=y) -> ~(x+1=y+1),

**P3**_{1}**)** x+0=x,

**P4**_{1}**)** x+(y+1)=(x+y)+1,

**P5**_{1}**)** B(0) &
Ax(B(x)->B(x+1)) -> AxB(x).

The axioms P3_{1} and P4_{1} represent
Grassmann's recursive definition of the addition. The induction
schema P5_{1} and our previous induction schema P3_{0}
look identical, yet actually P5_{1} is much more powerful
- in P5_{1 }we can take as B(x) formulas that contain the
addition letter.

Let us denote our new theory by PA_{1}. It is called
sometimes **Presburger's arihmetic**. In 1929 Mojsesz
Presburger established that:

a) There is an algorithm that allows deciding whether an
arbitrary closed formula in the language L_{1} is
"true" or not.

b) Using the axioms of PA_{1} we can prove each
"true" formula of L_{1}.

c) PA_{1} is consistent theory (in this last part of
his proof Presburger used only "finitistic" means of
reasoning allowed in Hilbert's program).

**M. Presburger.** Ueber die Vollstaendigkeit eines
gewissen Systems der Arithmetik ganzer Zahlen, in welchem die
Addition als einzige Operation hervortritt. C.R. du I Congr. des
Math. des pays Slaves, Warszawa, 1929, pp.92-101

Presburger's proof is a non-trivial piece of mathematics (see Hilbert, Bernays [1934], section 7.4). Of course, these results strengthened Hilbert's trust in a forthcoming solution of the entire problem... Just one more (maybe - technically very complicated) step, and we will have a "finitistic" proof that mathematics as a whole is both consistent and complete. Still, in 1930 a completely unexpected settlement followed... (see Section 5).

In 1974 Michael J.Fischer and Michael
O.Rabin proved that any algorithm for deciding whether an
arbitrary closed formula in the language L_{1} is
"true" or not requires at least 2**2**Cn units of time
for a formula consisting of n characters (** stands for
exponentiation). Could this result discourage Hilbert in 1929?

**M.J.Fischer, M.O.Rabin.** Super-Exponential Complexity of
Presburger Arithmetic. "Proceedings of the SIAM-AMS
Symposium in Applied Mathematics", 1974, vol. 7, pp.27-41
(see also Barwise [1977] -
Russian translation available)

Unfortunately, PA_{1} again is not a theory we are
searching for: in PA_{1 }multiplication of natural
numbers cannot be discussed. I.e. none of the formulas MULT(x, y,
z) in the language of PA_{1} can possess the properties:

a) PA_{1} proves: MULT(x, 0, 0) (i.e. x*0=0),

b) PA_{1} proves: MULT(x, y, u) & MULT(x, y+1, v)
-> u+x=v (i.e. x*(y+1)=x*y+x)).

(this result follows from Goedel's incompleteness theorem, see
Section 5.3). Hence, you cannot discuss in PA_{1}, for
example, the notion and properties of prime numbers.

As the next step, let us try again - let us extend PA_{1}
by adding to the language L_{1} the "missing"
function letter "*". Let us denote this new language by
L_{2}. Terms of L_{2} are defined as follows:

a) The constants 0 and 1, and all variables are terms.

b) If t_{1} and t_{2} are terms, then (t_{1}+t_{2})
and (t_{1}*t_{2}) also are terms.

Atomic formulas of L_{2} are built as (t_{1}=t_{2}),
where t_{1} and t_{2} are terms.

Since we can use, for example, the expression 2x^{2}-3y^{2}-1=0
as a shortcut for (1+1)*x*x=(1+1+1)*y*y+1, we can say simply that
atomic formulas of L_{2 }are arbitrary **Diophantine
equations**. After this, we must modify and extend the axioms
of PA_{1}:

**P1**_{2}**)** ~(0=x+1),

**P2**_{2}**)** ~(x=y) -> ~(x+1=y+1),

**P3**_{2}**)** x+0=x,

**P4**_{2}**)** x+(y+1)=(x+y)+1,

**P5**_{2}**)** x*0=0,

**P6**_{2}**)** x*(y+1)=(x*y)+x,

**P7**_{2}**)** B(0) &
Ax(B(x)->B(x+1)) -> AxB(x).

The axioms P5_{2} and P6_{2} represent
Grassmann's recursive definition of the multiplication. The
induction schema P7_{2} and our previous induction schema
P5_{1} look identical again, yet actually P7_{2}
is much more powerful - in P7_{2} we can take as B(x)
formulas that contain the addition and multiplication letters.
Let us denote our new theory by PA_{2}.

The language of PA_{2} is powerful enough to represent
(at least) simple assertions about natural numbers. For example:

Ey(x=y+y) represents "x is even number",

1<x & ~EyEz(y<x & z<x & x=y*z) represents "x is prime number",

AxEy(x<y & y is prime number) represents "there are infinitely many prime numbers".

**Exercise 3.2.** Put in the language of PA_{2} the
following assertions: "x and y have no common
divisors", "there are infinitely many twin prime
numbers", "sqrt(2) is not a rational number".

If PA_{2} is much more powerful than PA_{1},
then what kind of Fischer-Rabin's result can be proved for it? If
all algorithms for deciding PA_{1 }formulas (i.e. for
deciding whether an arbitrary closed formula in the language of
PA_{1} is "true" or not) are absolutely
infeasible, then, perhaps, there are no algorithms at all for
deciding of PA_{2 }formulas? In Section
6.3 we will prove that this is the case.

But how about another "next step" - why not to try
adding to the language of PA_{2} the **exponentiation**
letter and the axioms: x^{0}=1; x^{y+1}=x^{y}*x?
It appears that this is not necessary. In Section
3.3 we will prove the so-called **representation theorem**:
any computable function can be represented in PA_{2}. For
example, there is a PA_{2} formula EXP(x, y, z) such
that:

PA_{2} proves: EXP(x, 0, 1) (x^{0}=1),

PA_{2} proves: EXP(x, y, u) & EXP(x, y+1, v) ->
u*x=v (i.e. x^{y+1}=x^{y}*x).

Hence, adding of new functional letters does not improve the
power of PA_{2}.

Another estimate of the power of PA_{2} you could have
been proved in the Exercise 2.13(c): PA_{2} is equivalent
to a set theory where all sets are finite (i.e. to ZF minus
infinity axiom).

Hence, the volume of means of reasoning included in PA_{2},
is not accidental. This is the reason why PA_{2} is
called simply the **first order arithmetic**. The term
"first order" means that in PA_{2} the notion
of natural numbers is defined "in itself" (an sich) -
without using the more complicated notion of real numbers (which
is equivalent to the "second order" notion of arbitrary
sets of natural numbers). Hence, in a sense, you may think of PA_{2}
as formalization of the so-called **discrete mathematics**
(see also Section 5.2).

Traditionally, the first order arithmetic is called **Peano
arithmetic**, and is denoted simply by PA (instead of the above
PA_{2}). More about it - see Hajek, Pudlak [1993]. The
original Dedekind's system of three axioms P1, P2, P3 (see above)
is called **second order** Peano arithmetic (because it is
using not only variables for natural numbers, yet also variables
for sets of these numbers).

Our customary intuitive understanding of the language of PA (first order arithmetic) leads to an old Platonist prejudice which says that any closed formula of PA "must be" either "true" or "false". Let us clarify this. Of course, we must follow the intuition while selecting the axioms of PA. We must follow the intuition when trying to establish formal versions of statements from the usual (intuitive) number theory developed by working mathematicians (as we did it in the Exercise 3.2). Still, any attempt to go further than this, an attempt to grant our intuition of natural number sequence a mysterious informal meaning ends up in Platonism. Many people are going this way taking seriously the following "definition" of "true" formulas in PA:

a) Atomic formulas of PA are assertions about equality of polynomial values. For any particular values of variables the polynomial values can be calculated, and in this way the truth or falsity of atomic formulas can be established.

b) When a formula F is built up from two formulas A, B by using the connectors ~, &, v, ->, and the truth or falsity of A and B is known, then the truth of F is established easily by using the truth tables.

c) In PA we have two quantifier symbols E, A. The formula Ex C(x) is true, iff C(x) is true for at least one x. And the formula Ax C(x) is true, iff C(x) is true for all x's.

Hence, it seems that any closed formula of PA (i.e. a formula containing no free variables) "must be" either "true" or "false". This corresponds well to our customary intuition: a closed formula of PA asserts some completely definite property of natural number system (like as the assertion that there exist infinitely many prime numbers), and this system either possess this property or not.

Let us note, however, that in the above "definition"
the sentence "C(x) is true for all x's" is used.
According to our intuition of natural numbers, there exists an
infinite number of x's. Hence, it is impossible to establish the
truth of the assertion Ax C(x) simply by checking the truth of
C(x) for particular x's. The truth of AxC(x) could be established
(if ever) only **theoretically**, by proving the assertion
from some axioms, i.e in some theory (for example, in PA or ZF).
May we assert that any closed formula of PA must be either
"theoretically provable", or "theoretically
refutable"? We would like to assert this..., still, **which
particular theory** are we intending - PA, ZF or other? Is this
all the same? We must choose some particular theory, else our
"definition" of true formulas will hang by a thread...

This problem was put elegantly by Paul Lévy (see Levy [1926]): "Ce qu'il faut admirer, c'est la puissance de l'analyse mathematique qui arrive ainsi, dans tant de cas, a reduire une infinite de verifications a un raisonnement unique. Qui peut s'etonner qu'elle n'y soit pas parvenue dans tous les cas? Non seulement cela n'a rien d'etonnant, mais il est a priory assez probable qu'il existe certains enonces, qui resument ainsi en une formule unique une infinite de cas particuliers, et pour lesquels il est impossible de jamais reduire toutes les verifications necessaires a un nombre fini d'operations..."

Maybe, the firm belief in the above-mentioned "definition" is due to the law of the excluded middle, which is a postulate in the classical logic. Of course, in PA the formula Av~A is provable for any A. Does it follow from this that for a closed A either PA proves A, or PA proves ~A? It follows from Goedel's incompleteness theorem that neither PA, nor ZF, nor any other fundamental mathematical theory can possess this perfect property - a mere postulation of the excluded middle cannot solve our problems! For an exact treatment see Section 5.

Let us return to PA as a formal theory. The principal means of
proving theorems in PA is, of course, the induction principle P7_{2}.
Let us prove, for example, the formula 0+x=x (until we prove that
x+y=y+x, this formula differs from the axiom x+0=x). Let us
denote 0+x=x by B(x). First, we must prove B(0), i.e. 0+0=0. This
is simply an instance of the axiom x+0=x. Now we must prove that
B(x)->B(x+1):

B(x) (0+x=x, hypothesis),

0+(x+1)=(0+x)+1 (an instance of the axiom x+(y+1)=(x+y)+1),

0+x=x -> (0+x)+1=x+1 (follows from identity axioms),

(0+x)+1=x+1 (by MODUS PONENS),

0+(x+1)=x+1, or B(x+1) (by transitiveness of identity).

Hence, by the Deduction Theorem, B(x)->B(x+1), i.e. also Ax(B(x)->B(x+1)). And, by the induction principle, AxB(x). Q.E.D.

In a similar way we could prove other simple theorems of PA. The only problem is to find the optimal order of proving. Try to prove directly, for example, the commutativity of multiplication (x*y=y*x). It seems to be a hard task. Still,

**Exercise 3.3.** Prove the following theorems of PA (see Mendelson [1997]):

x+z=y+z -> x=y,

0+x=x, (x+1)+y=(x+y)+1, x+y=y+x, (x+y)+z=x+(y+z),

0*x=0, (x+1)*y=(x*y)+y, x*y=y*x, x*(y*z)=(x*y)*z.

In PA we can prove all the necessary properties of the relation x<y (it can be defined by the formula Ez(x+z+1=y). In particular, we could prove the following schema of theorems:

~AxC(x) -> Ex(~C(x) & Ay(y<x -> C(y)).

I.e. if not all natural numbers possess the property C, then there is the minimum number that does not possess C.

In PA we can discuss freely the properties of the **division**
operation. Let us denote by R(x, y, z) the formula Eu(x=y*u+z
& z<y), i.e. x mod y = z in Pascal. Then we could prove in
PA that:

0<y -> EzR(x, y, z),

R(x, y, z_{1}) & R(x, y, z_{2}) -> z_{1}=z_{2}.

All these (and many more) formal proofs you can find in Mendelson [1997]. In this book formal proving of theorems about natural numbers is performed to the extent that you can start proving in PA more serious theorems of the (intuitive) elementary number theory. For example, you can try to prove that:

there are infinitely many prime numbers,

sqrt(2) is not a rational number,

e and pi are transcendent numbers,

if p(x) is the number of primes in the sequence 1, 2, ..., x, then p(x)/ln x -> 1 as x -> infinity,

etc.

Do not be surprised at the use of some real numbers and the function ln x in the above statements. If in a statement or a proof only a fixed list of computable real numbers and computable real functions is used, then this statement/proof can be translated into PA (see Exercise 3.2).

Let us introduce shortcuts for some specific terms of PA: bold
**0** will denote 0, bold **1** will denote 1, bold **2**
- (1+1), bold **3** - ((1+1)+1) etc. These terms are called **numerals**,
they are used as standard representations of particular natural
numbers. To denote numerals in schemas of PA formulas we will use
bold letters **k**, **l**, **m**, **n**, **p**, **q**,
**r**.

For example, if k is a natural number, k>0, then:

PA proves: x<**k** <-> (x=**0**) v (x=**1**)
v ... v (x=**k-1**),

PA proves: (Ex<**k**) C(x) <-> C(**0**) v C(**1**)
v ... v C(**k-1**),

PA proves: (Ax<**k**) C(x) <-> C(**0**) &
C(**1**) & ... & C(**k-1**).

**Exercise 3.4.** If some atomic formula (t_{1}=t_{2})
of PA contains variables x_{1}, x_{2}, ..., x_{n},
then by moving all components of t_{2} to the left hand
side we can obtain an arbitrary Diophantine equation t_{1}-t_{2}=0
(see Section 4.1). Our concern is solving of these equations in
natural numbers. Show that, if we have a particular solution (b_{1},
b_{2}, ..., b_{n}) of the equation t_{1}-t_{2}=0,
then

PA proves: Ex_{1}Ex_{2}...Ex_{n }(t_{1}=t_{2}).

**Hint**: show that PA proves every "true" atomic
formula s_{1}=s_{2}, where the terms s_{1}
and s_{2} do not contain variables.

In first order arithmetic (PA) the simplest of the (important) ways of mathematical reasoning is formalized, where only natural numbers (i.e. discrete objects) are used. Other, more complicated mathematical notions (real numbers, Cantor's arbitrary infinite sets) are formalized (as it should be) in more complicated formal theories. These more complicated theories are more "powerful" than PA in the sense that they are able to discuss more complicated objects (real numbers, arbitrary infinite sets). Still, how about their "power" in discussing of properties of natural numbers? Can they prove a theorem about natural numbers that cannot be proved in PA? For example, maybe, the twin prime conjecture can be proved in ZFC, yet it cannot be proved in PA? At first glance, this seems impossible, because the notion of natural numbers seems to be independent of (and "more fundamental than") other mathematical notions. Unfortunately, this is not the case... For the final solution see Section 6.5 and Appendix 2.

How to "select" natural numbers in some formal
theory T? The most general method of doing this is the so-called **relative
interpretation**. To indicate natural numbers in some theory T,
we must first provide a formula N(x) that "asserts"
that x is a natural number. The second component to be provided
is an algorithm Tr transforming atomic formulas of PA (i.e.
Diophantine equations) into formulas of T. If F is an atomic
formula of PA, then Tr(F) must be a formula of T having exactly
the free variables of F. The algorithm Tr can be extended to
cover also non-atomic formulas of PA:

Tr(~F) = ~Tr(F),

Tr(F->G) = Tr(F)->Tr(G),

Tr(F & G) = Tr(F) & Tr(G),

Tr(F v G) = Tr(F) v Tr(G),

Tr(ExF(x)) = Ex(N(x) & Tr(F(x))),

Tr(AxF(x)) = Ax(N(x) -> Tr(F(x))).

Hence, having an assertion about natural numbers, i.e. some PA formula F, we can ask: if PA proves F, then T proves Tr(F)? And, maybe, T proves some Tr(F) such that PA cannot prove F?

**Exercise 3.5.** Generalize the above definition for
arbitrary two formal theories T1 and T2.

Let us say that PA is **relatively interpretable** in the
theory T, iff there is a relative interpretation (N, Tr) such
that for each closed PA formula F: if PA proves F, then T proves
Tr(F). Of course, to establish the relative interpretability of
PA in some theory T, we need not to check all closed PA formulas.
It is sufficient to check only the axioms of PA. Let us consider,
for example, the axiom x+1=y+1 -> x=y. We must show that

T proves: N(x) & N(y) -> (Tr(x+1=y+1) -> Tr(x=y)).

If we have established this for all axioms of PA, then (since theory T contains 100% of logical means of reasoning) we have proved that T proves Tr(F), if PA proves F.

Acknowledging the fundamental role of natural numbers in
mathematics, let us call a formal theory T a **fundamental
theory**, iff PA is relatively interpretable in T.

The simplest fundamental theory is, of course, PA itself. The
set theory ZF is (of course) fundamental also. As the formula
N(x) asserting that "x is natural number" we can take
here simply the formula "x in w", where w is the set of
all natural numbers (see Section 2.3).
As you established in Exercise 2.14, "x in w" is a very
long formula in the language of ZF. The translation algorithm Tr
from PA to ZF also is somewhat complicated. Of course, Tr(x=y) =
(x=y). Since **0** is defined in ZF as the empty set, Tr(x=**0**)
= Ay~(y in x). Since **1** is defined as the set {o}, Tr(x=**1**)
= Ay(y in x <-> Tr(y=**0**)). After this, Tr(x=**2**)
can be obtained as Ay(y in x <-> Tr(y=**0**) v Tr(y=**1**)).
Etc.

Now, we can reformulate the question of the first paragraph of this section as follows: is it possible that there is a fundamental theory T and a PA formula F such that PA cannot prove F, yet T proves Tr(F)? See positive answers in Section 6.5 and Appendix 2.

**Exercise 3.6.** Generalize the result of the Exercise 1.4
by proving that the set Tr^{-1}(T) of "arithmetical
theorems" of any formal theory T is effectively enumerable.
Hint: use the computability of Tr.

For a complete treatment of relative interpretability see Feferman [1960]. The most striking result is due to Hao Wang: any formal theory T is relatively interpretable in PA+Con(T), i.e. in PA plus one more axiom - an arithmetical translation of the assertion "T is a consistent theory" (for details see Section 5.4).

How could we verify that some formula F(x) "asserts" that x is a prime number? Of course, if F(x) is the formula

1<x & ~EyEz(y<x & z<x & x=y*z),

we could say that it "corresponds" to the definition of prime numbers. Still, this is not the only formula "expressing" that x is a prime number...

As the first step, we could introduce the following "definition": formula F(x) "expresses" the predicate "x is prime number", iff for all n: F(n) is "true", iff n is indeed a prime number.

The next step would be to replace the vague notion of
"truth" by the more exact notion of provability in PA:
formula F(x) "expresses" in PA the predicate "x is
prime number", iff for all n: n is a prime number, iff PA
proves F(**n**) (where **n** is the numeral, i.e. 1+1+...+1
n times).

This definition involves unprovability (if n is not prime,
then F(**n**) must be unprovable in PA). Establishing of
unprovability is a very hard task. Indeed, if PA would be
inconsistent, then every formula would be provable in PA, and
thus, the predicate "x is prime number" could not be
"expressed" at all. Since we do not know exactly, is PA
consistent or not (for details see Section
5.4), the latter definition of "expressability" is
not satisfactory.

A much better solution: let us say that a formula F(x) expresses the predicate "x is prime number" in PA, iff for all n:

a) If n is a prime number, then PA proves F(**n**).

b) If n is not prime number, then PA proves ~F(**n**).

This definition is 100% positive in the sense that it involves only provability of formulas, and does not use unprovability. The expressability according to this definition can be established independently of our (missing) knowledge, is PA consistent or not.

Let us adopt this definition as a general one. Let us say that
a formula P(x, y) **expresses the predicate** p(x, y) in PA,
iff P has exactly two free variables x, y, and for all pairs m,
n:

a) If p(m, n), then PA proves P(**m**, **n**).

b) If not p(m, n), then PA proves ~P(**m**, **n**).

The definition of expressability for ternary etc. predicates is similar.

You could prove easily, for example, that the formula x=y
expresses the identity predicate of natural numbers. Indeed, if
m=n, then PA proves **m**=**n** (since the terms **m**, **n**
are identical). If m, n are different numbers, then (in order to
prove ~(**m**=**n**)) apply to the
formula **m**=**n** the axiom x+1=y+1 -> x=y as many
times as you can, and then apply the axiom ~(0=x+1).

If PA would be an inconsistent theory, then (according to our final definition) any formula would express any predicate, i.e. then all predicates would be expressible. If PA is consistent, then each formula can express only one predicate. Hence, in this case the set of all predicates that are expressible in PA is countable. Since the set of all possible natural number predicates is uncountable, some of these predicates cannot be expressible.

Let us assume that PA is consistent. Then only **computable**
**predicates** are expressible in PA. Indeed, let some formula
P(x, y) express in PA the predicate p(x, y). How to determine, is
p(m, n) true or false for given numbers m, n? If p(m, n) is true,
then PA proves P(**m**, **n**), and if p(m, n) is false,
then PA proves ~P(**m**, **n**). Hence, let us take a
computer that prints out all theorems of PA one by one. (Such a
computer does exist, since the set of all theorems of any formal
theory is effectively enumerable - see Exercise 1.4). Let us sit
beside the output tape of this computer waiting for one of the
formulas - P(**m**, **n**) or ~P(**m**, **n**). If P(**m**,
**n**) appears, then ~P(**m**, **n**) will not appear
(PA is assumed to be consistent), i.e. p(m, n) is true. If ~P(**m**,
**n**) appears, then P(**m**, **n**) will not appear,
and hence, p(m, n) is false. Thus we have a procedure solving
p(m, n) for any given numbers m, n, i.e. the predicate p(x, y) is
computable.

We do not know exactly, is PA consistent or not. Later in this section we will prove (without any consistency conjectures!) that each computable predicate can be expressed in PA.

For our crucial proofs in Section 5 we will need a somewhat stronger definition of "expressability" of functions in PA. The straightforward definition (the function f(x, y) is expressible iff the predicate f(x, y)=z is expressible) is too weak.

Let us say that the formula F(x, y, z) **represents** in PA
the **function** f(x, y), iff F has exactly three free
variables x, y, z, and for every natural numbers k, m, n such
that f(k, m)=n:

a) PA proves F(**k**, **m**, **n**).

b) PA proves Az(~(z=**n**) -> ~F(**k**, **m**,
z)).

For simple expressability of the predicate f(x, y)=z we would need instead of b):

b_{1}) if not f(k, m) = n, then PA proves ~F(**k**,
**m**, **n**),

i.e. for each n we could provide a separate proof ~F(**k**,
**m**, **n**), yet b) requires instead of these separate
proofs a **single** general proof for all values of n.

If PA is inconsistent, then all natural number functions are representable in PA.

**Exercise 3.7.** a) Verify that if PA is consistent, then
only computable functions can be represented in PA.

b) Prove that a predicate p(x) can be expressed in PA, iff the
following function h_{p}(x) can be represented in PA: h_{p}(x)=1
if p(x), and h_{p} (x)=0 if not p(x).

Hence, we would prove that all computable predicates are expressible in PA, if we would prove the following

**Representation Theorem.** Every computable function can
be represented in PA.

**Proof**. The rest of this section.

**Note.** The formulas we will build to represent functions
in PA, will contain the letters "&" and
"v", but **not** the negation letter "~",
they will contain existential quantifiers Ex, and only **restricted
**universal quantifiers Ax(x<t -> ...), where t are
linear terms of PA. This observation will allow us to apply the
representation theorem as the starting point for the solution of
Hilbert's Tenth problem in Section 4.

Let us start the proof. We have a computable function f(x, y)
mapping pairs or natural numbers into natural numbers. And we
must build a PA formula F(x, y, z) representing f(x, y)=z in PA.
I.e. we must provide an algorithm that allows converting **computer
programs** computing natural number functions into formulas
representing these functions.

What kind of computers should we choose for this purpose -
Wintel, Macintosh, or Sun? For the simplicity of proof let us use
the so-called **Turing machines** invented in 1936 by Alan
M.Turing.

**A.Turing.** On computable
numbers, with an application to the Entscheidungsproblem.
"Proc. London Math. Soc.", 1936, vol. 42, pp.230-265
(received May 28, 1936)

Independently and almost simultaneously a similar explicit concept of abstract machines was proposed by Emil L. Post:

**E.L.Post.** Finite combinatory processes - formulation 1.
"Journ. Symb. Logic", 1936, vol.1, pp.103-105 (received
October 7, 1936)

Formally, a (somewhat modernized version of) Turing machine M consists of:

a) A finite set of internal states:

S_{M} = {s_{start}, s_{stop},
s_{1}, ..., s_{m}}.

Programmers can think of S_{M} as the main memory of
M: 2+m=2^{k}, where k is the number of memory bits.

b) A finite set of letters:

B_{M} = {b_{1}, ..., b_{n}}.

c) A finite set (not sequence!) P_{M} of instructions
(the "program") each having the form:

s, b -> s', b', e,

where s and s' are states, b and b' - letters, e = 0, +1, or
-1. Two instructions of P_{M }should not have the same
left-hand side (s, b).

This formal object works as follows. Imagine:

a) An infinite tape (the "hard disk" of M)
consisting of fixed size cells, each cell containing a letter
from B_{M}.

b) A box encapsulating some state from S_{M}, and
attached to some cell on the tape.

| Box |

| cell 0 | cell 1 | cell 2 |........................| cell n
|.........................................................

Every second the following happens: if the box is
in the state s, and if the cell it is attached to contains the
letter b, and if the program P_{M} contains the
instruction s, b -> s', b', e, then the box changes its state
from s to s', the letter b in the cell is replaced by the letter
b', and the box moves by e cells. I.e. if e = -1, then it moves
one cell to left, if e = +1, it moves one cell to right, if e =
0, it does not change the position. If the program P_{M }does
not contain an appropriate instruction, then nothing happens. If
e = -1, but the box is attached to the leftmost cell of the tape,
then the box does not move.

As you can see, Turing did not use the von Neumann's principle (invented some 10 years later) according to which data and programs should be kept in the same memory space.

Let us say that the **machine M computes the function**
f(x, y), iff for each pair m, n the following happens. Starting
in the situation where:

a) The box is in the state s_{start} and is attached
to the leftmost cell of the tape.

b) The tape contains the following sequence of letters:

1 1 ... 1 0 1 1 ... 1 0 0 0 ...,

m times ... n times.............

the machine M performs a finite number of steps according to its program and after this the situation occurs where:

a) The box is in the state s_{stop}.

b) The tape contains the following sequence of letters:

1 1 ... 1 0 ...

f(m, n) times

The rest of the tape may contain arbitrary letters.

Let us say that a function f(x, y) is a **computable function**,
iff it can be computed in the above way by some Turing machine.

As an example, let us build a machine computing the function f(x) = x+2. This machine must simply cross the array of 1's and append another two 1's to it.

S_{M} = { s_{start}, s_{stop}, s},

B_{M} = {0, 1},

P_{M} = {

s_{start}, 1 -> s_{start}, 1, +1; // skip
1's

s_{start}, 0 -> s, 1, +1; // write the first
additional 1, register this as done

s, 0 -> s_{stop}, 1, 0; // write the second
additional 1, and stop

}.

**Exercise 3.8.** a) Build some of the Turing machines
computing the following functions: x+y, x*2, x*y, 2^{x},
[log_{2}x] (or int(log2(x)) in Pascal).

b) Maybe, you cannot buy a real Turing machine in your city,
still, you can surely force your PC to emulate these machines.
Write (using your favorite programming language) an **interpreter
of Turing machines**. It should be a program, receiving as
inputs S_{M}, B_{M}, P_{M} and initial
states of the tape cells. As outputs the program should print out
final states of the tape cells.

Thus, your PC can easily emulate Turing machines. Much more striking is the converse statement: Turing machines can (not easily, yet they can!) emulate your PC, with your Pascal, C++, Lisp, Prolog etc. included. All the techniques necessary for proving this statement can be found, for example, in Mendelson [1997] or Kleene [1952].

Turing machines represent one of the possible formal reconstructions of the intuitive notion of computability (the concept of algorithm). Since 1930s, besides Turing machines, several other very different formal reconstructions of this notion were proposed: recursive functions, lambda-calculus by A. Church, canonical systems by E. Post, normal algorithms by A.A. Markov, etc. And the equivalence of all these reconstructions was proved (see Mendelson [1997] or Kleene [1952]).

The equivalence of different formal reconstructions of the
same intuitive concept means that the volume of the reconstructed
formal concepts is not accidental. This is the best reason to
abandon the (vague) intuitive concept of computability, and to
replace it by the formal concept, for example, by the concept of
computability by Turing machines. This approach is known as the **Church's
thesis**:

**If some function is computable in the intuitive sense of
the word, then an appropriate Turing machine can compute it.**

Alonzo Church stated (an equivalent of) this thesis in 1936:

**A.Church.** An unsolvable
problem in elementary number theory. "American Journal of
Mathematics", 1936, vol. 58, pp.345-363

In the original form of Church's thesis recursive functions were used instead of Turing machines.

Let us return to the proof of our representation theorem. We must represent the predicate f(x, y)=z by a formula F(x, y, z) in the language of PA. Since f(x, y) is a computable function, we can try to build F(x, y, z) by describing in PA the computation process that leads from the value pair (k, m) to the value f(k, m). Let us denote by M some Turing machine performing this computation process.

Our task would be much easier, if the language of PA contained
some additional constructs. The following sequence could be
called a **situation**:

(s, p, a_{0}, a_{1}, ..., a_{q-1}),

where s is a state from S_{M}, p is the number of the
cell to which the box M is currently attached, and a_{0},
a_{1}, ..., a_{q-1} are letters in the first q
cells of the tape (all the other cells contain the letter 0). Let
us introduce a new kind of variables C, C_{1}, C_{2},
..., their domain will consist of all possible situations. Let us
introduce also some additional function letters:

s(C) = s in C,

p(C) = p in C,

q(C) = q in C,

a_{i}(C) = a_{i} in C.

If we had all these symbols in the language of PA, our task of representing computable functions by formulas would be much easier.

Our first formula START(C, x, y) must assert that C is the initial situation having the values of arguments x and y on the tape:

s(C)=s_{start} & p(C)=0 &
q(C)=x+y+1 & (Ai<x+y+1)(a_{i}(C)=1 v (a_{i}(C)=0
& i=x))

(I'm sorry, but we need this trick to avoid negations).

The second formula STOP(C, z) must assert that C is a final situation having the function value z on the tape:

s(C)=s_{stop} & z<q(C) & a_{z}(C)=0
& (Ai<z)a_{i}(C)=1.

As the next step, we build for each instruction I: s, b ->
s', b', e the formula STEP_{I}(C_{1}, C_{2})
asserting that by applying the instruction I in the situation C_{1}
we will obtain the situation C_{2}.

**Exercise 3.9.** Write these formulas yourselves ignoring
my next few paragraphs.

First let us consider the case when e = 0:

s(C_{1})=s & s(C_{2})=s'
& EkEn(p(C_{1})=k & p(C_{2})=k & q(C_{1})=n
& q(C_{2})=n &

a_{k}(C_{1})=b & a_{k}(C_{2})=b'
& (Ai<n)(i=k v Ej(a_{i}(C_{1})=j & a_{i}(C_{2})=j)).

We did not use expressions like as p(C_{1})=p(C_{2})
to simplify our next steps.

Now the case when e = -1:

s(C_{1})=s & s(C_{2})=s'
& EkEmEn(p(C_{1})=k & p(C_{2})=m &
q(C_{1})=n & q(C_{2})=n &

a_{k}(C_{1})=b & a_{k}(C_{2})=b'
& ((k=0 & m=k) v m+1=k) &

(Ai<n)(i=k v Ej(a_{i}(C_{1})=j
& a_{i}(C_{2})=j)).

The second row of this formula says that if in C_{1}
the box is attached to the leftmost cell of the tape, then e = -1
works as e = 0.

And finally, the case e = +1:

s(C_{1})=s & s(C_{2})=s'
& EkEmEnEr(p(C_{1})=k & p(C_{2})=m &
q(C_{1})=n & q(C_{2})=r &

a_{k}(C_{1})=b & a_{k}(C_{2})=b'
& k+1=m & ((m<n & n=r) v (m=n & n+1=r & a_{m}(C_{2})=0)
&

(Ai<n)(i=k v Ej(a_{i}(C_{1})=j
& a_{i}(C_{2})=j)).

The condition a_{m}(C_{2})=0 in the second row
says that the "unregistered" rest of the tape contains
only letters 0.

The next formula COMPUTE_{M}(C_{1}, C_{2})
will assert that starting the program P_{M} in the
situation C_{1} after a finite number of steps we obtain
the situation C_{2}. To simplify the task let us
introduce one more variable L taking as its values finite
sequences of situations. We will need also the corresponding
function symbols: d(L) = the length of the sequence L, g_{i}(L)
= the i-th situation in L. Now we can easily write the formula
COMPUTE_{M}(C_{1}, C_{2}):

ELEw((d(L)=w+1 & g_{0}(L)=C_{1}
& g_{w}(L)=C_{2} & (Ai<w)EC_{3}EC_{4}
(g_{i}(L)=C_{3} & g_{i}(L)=C_{4}
& STEP_{M}(C_{3}, C_{4}))),

where STEP_{M}(C_{3}, C_{4}) is the
following formula:

STEP_{I}(C_{3}, C_{4})
v STEP_{II}(C_{3}, C_{4}) v ... v STEP_{IK}(C_{3},
C_{4}),

assuming that P_{M} = {I, II, ..., IK}.

Finally, we can write the formula F(x, y, z) asserting that f(x, y)=z as follows:

EC_{1}EC_{2} (START(C_{1},
x, y) & COMPUTE_{M}(C_{1}, C_{2})
& STOP(C_{1}, z)).

This formula is not 100% a PA formula since it contains symbols denoting states and tape letters, situation variables (and even a variable for sequences of situations), and a lot of function symbols missing in the language of PA. Hence, to complete our proof we must show how to eliminate these constructs.

As the first step, let us replace the symbols denoting states
(s_{start}, s_{stop}, s, s', etc.) and tape
letters (0, 1, b, b', etc.) of the machine M by some natural
numbers. How to replace the situation variables? If states and
tape letters are already replaced by numbers, then situations are
simply finite sequences of numbers. Hence, our situation variable
problem would be solved, if we could find a good coding algorithm
that allowed to represent any finite sequence of natural numbers
by a single natural number (or, at least by two or three
numbers). This algorithm must be "good" in the sense
that it must allow representation of the functions s(C), a_{i}(C)
etc. by formulas of PA.

It was Goedel's idea to use for this purpose the so-called Chinese remainder theorem. Could you find a number X such that (in Pascal):

X mod 3 = 2, X mod 5 = 3, and X mod 7 = 4?

Let us consider the numbers 7k+4 for k=0, 1, 2, ...:

4, 11, 18, 25, 32, 39, 46, 53, ...

Here 11 mod 3 = 2, 32 mod 3 = 2, 53 mod 3 = 2, yet only the number 53 possesses the property 53 mod 5 = 3. Hence, the least number that we can take is X = 53.

In general, if we have a sequence of divisors u_{1}, u_{2},
..., u_{n} (i.e. u_{i}>=2 for all i), and a
sequence of remainders v_{1}, v_{2}, ..., v_{n}
(i.e. 0<=v_{i}<u_{i} for all i), could we
find a number X such that X mod u_{i} = v_{i} for
all i? If some of the numbers u_{i} have a common
divisor, then this problem may have no solutions. For example, if
u_{1} = 6 and u_{2} =10, then X=6y_{1}+v_{1}=10y_{2}+v_{2},
and thus v_{1}-v_{2} must be an even number, i.e.
if v_{1} = 1 and v_{2} = 2, then our problem has
no solutions. Still, if two of the numbers u_{i} never
have common divisors, then the solution always exists. This is
the

**Chinese Remainder Theorem.** Let u_{1}, u_{2},
..., u_{n} be a sequence of natural numbers (u_{i}>=2
for all i), two of them never have common divisors. And letv_{1},
v_{2}, ..., v_{n} be a sequence of natural
numbers such that 0<=v_{i}<u_{i} for all i.
Then there is a natural number X (less than the product u_{1}u_{2}...u_{n})
such that X mod u_{i} = v_{i} for all i.

**Proof.** Let us associate with every number x such that 0
<= x < u_{1}u_{2}...u_{n}, the
"remainder vector" (x mod u_{1}, x mod u_{2},
..., x mod u_{n}). Show that if two such numbers have
equal remainder vectors, then their difference is a multiple of
the product u_{1}u_{2}...u_{n}. Q.E.D.

Using this theorem we can try to organize a coding of
sequences of natural numbers v_{0}, v_{1}, ..., v_{n-1}
by representing each number v_{i} as X mod u_{i},
where X is the "code" (possibly large, yet fixed
number) and the sequence u_{0}, u_{1}, ..., is
generated in some simple way. For example, we can try a linear
function: u_{i} = yi+z. How to choose y and z? Two
numbers u_{i} should not have common divisors. If d is a
common divisor of u_{i} and u_{j}, then d divides
also u_{i}-u_{j} = y(i-j). If we take z = y+1,
i.e. u_{i} = y(i+1)+1, then divisors of y cannot divide
neither u_{i}, nor u_{j}. Thus our common divisor
d must divide i-j, i.e. a number less than n. Hence, if we take
as y a multiple of (n-1)! (i.e. 1*2*3*...(n-1)), then the numbers
u_{0}, u_{1}, ..., u_{n-1} will have no
common divisors. And finally, if we take y large enough to ensure
that u_{0}>v_{0}, u_{1}>v_{1},
..., u_{n-1}>v_{n-1}, then according to
Chinese remainder theorem we can find a number x such that x mod
u_{i} = v_{i} for all i = 0, 1, ..., n-1.

Hence, we could use the pair (x, y) as a code of the sequence
v_{0}, v_{1}, ..., v_{n-1}. Such a code
does not include the number n, so, it would be better to code the
sequence of n, v_{0}, v_{1}, ..., v_{n-1}
instead of v_{0}, v_{1}, ..., v_{n-1}
alone.

The function:

beta(x, y, i) = x mod (1+y(i+1))

is called **Goedel's beta-function**. As we have proved,
for each sequence of natural numbers v_{1}, ..., v_{n}
a pair of natural numbers x, y can be found such that

beta(x, y, 0) = n, beta(x, y, 1) = v_{1},
..., beta(x, y, n) = v_{n}.

Note also, that we can represent beta-function in PA by the following formula BETA(x, y, i, j) (asserting that beta(x, y, i) = j):

Ez(x=(1+y*(i+1))*z+j & j<1+y*(i+1)).

Now we can start rewriting of our formulas START, STOP, STEP
etc. in the language of PA. We have already replaced by natural
numbers all states of the machine M and all tape letters. Hence,
any situation (s, p, a_{0}, a_{1}, ..., a_{q-1})
is now a sequence of natural numbers that we can replace by two
numbers x, y such that:

beta(x, y, 0) = q, beta(x, y, 1) = s, beta(x,
y, 2) = p, beta(x, y, 3) = a_{0}, ..., beta(x, y, q+2) =
a_{q-1}.

Hence, we can replace any quantifier EC by two quantifiers ExEy, where x, y are variables of PA. The additional function symbols we have introduced:

q(C)=q_{1}, s(C)=s_{1}, p(C)=p_{1},
a_{i}(C)=b,

we can replace now by:

beta(x, y, 0) = q_{1}, beta(x, y, 1) =
s_{1}, beta(x, y, 2) = p_{1}, beta(x, y, 3) = a_{0},
beta(x, y, i+3) = b.

The "illegal" inequalities such as q_{1}<q(C)
also can be eliminated:

Eq_{2}(beta(x, y, 0)=q_{2}
& q_{1}<q_{2}).

**Exercise 3.10.** Rewrite the formulas START, STOP, STEP_{I}
and STEP_{M}, and calculate the length of each.

In the formula COMPUTE_{M} we introduced the variable
L for finite sequences of situations, and function letters d(L)
and g_{i}(L). For each situation we have now a code
consisting of two numbers x, y. Hence, if the code of the
situation C_{i} is (c_{i}, d_{i}), then
we can code the sequence L = (C_{0},..., C_{n-1})
as the sequence of numbers:

n, c_{0}, d_{0}, c_{1},
d_{1}, ..., c_{n-1}, d_{n-1},

i.e. by two numbers x, y such that:

beta(x, y, 0) = n, beta(x, y, 2i+1) = c_{i},
beta(x, y, 2i+2) = d_{i}.

Now we can replace the quantifier EL by two quantifiers ExEy,
where x, y are variables of PA. Our two last additional function
symbols can be eliminated as follows. We will replace the formula
d(L)=w by beta(x, y, 0) = w, and g_{i}(L)=C - by

beta(x, y, 2*i+1)=c_{1} & beta(x,
y, 2*i+2)=d_{1},

where (c_{1}, d_{1}) is the code of the
situation C.

**Exercise 3.11.** Rewrite the formulas COMPUTE_{M}
and F(x, y, z), and calculate the length of each.

Thus we have an algorithm allowing to convert a Turing machine M computing the function f(x, y) into a PA formula F(x, y, z) asserting that f(x, y) = z. To complete the proof of the representation theorem we must show that for every natural numbers k, m, n such that f(k, m)=n:

a) PA proves: F(**k**, **m**, **n**).

b) PA proves: Az(~(z=**n**) -> ~F(**k**, **m**,
z)).

This would take a lot of time and space. See Mendelson [1997] or Kleene [1952] instead.

Let us think we have proved the representation theorem. Q.E.D.

first order arithmetic, Peano, Dedekind, Grassmann, arithmetic, formal, axiomatic, axioms, Presburger

Back to title page.