ℕ = ( | ℕ | , Zℕ , Sℕ , Aℕ , Mℕ , Eℕ , Lℕ )
to be the first-order structure in this language with
| ℕ | = { 0 , 1 , 2 , … } , the set of natural numbers , which we also call ω
Zℕ = 0 , which is the usual zero
Sℕ : n ↦ n + 1 , which is the usual successor function
Aℕ : ( m , n ) ↦ m + n , which is the usual addition
Mℕ : ( m , n ) ↦ m ⋅ n , which is the usual multiplication
Eℕ : ( m , n ) ↦ mn , which is the usual exponentiation
Lℕ ( m , n ) iff m < n , which is the usual linear ordering and happens to be a wellordering
In some other mathematics courses, ℕ and ω mean the same thing but here ℕ is a certain structure whose universe is ω.
Next we will define several theories, all of which have ℕ as a model.
It is obvious that ℕ ⊨ Q .
We remark that, in some other books, the theory Q does not include the axioms for E and L.
S ( ⋅ ⋅ ⋅ S ( Z ) ⋅ ⋅ ⋅ )
where there are n many occurences of S nested around Z.
Then, for every n ∈ ω,
Sn ( Z ) ℕ = n .
What about Sn ( Z ) ℕ' for other models ℕ' of Q ?
Let ℕ' be a model of Q.
Let π : ω ↦ | ℕ' | be defined by π ( n ) = Sn ( Z ) ℕ' .
Then π is an isomorphism from ℕ to a substructure of ℕ' .
Moreover, ran ( π ) is an initial segment of the linear ordering ( | ℕ' | , Lℕ' ) .
Sketch
There are several things to verify:
(True by definition.)
(True by definition.)
For item 3, we prove by induction on n ∈ ω, that for every n ∈ ω,
A ( Sm ( Z ) , Sn ( Z ) ) ℕ' = Sm + n ( Z ) ℕ' .
For n = 0 , this says
A ( S m ( Z ) , Z ) ℕ' = S m ( Z ) ℕ' ,
which we see holds by Axiom 4 of Q.
For n > 0 , we compute
A ( S m ( Z ) , Sn ( Z ) ) ℕ' = A ( S m ( Z ) , S n - 1 + 1 ( Z ) ) ℕ'
= S ( A ( S m ( Z ) , S n - 1 ( Z ) ) ) ℕ' by Axiom 5
= S ( S m + n - 1 ( Z ) ) ℕ' by the induction hypothesis
= S m + n ( Z ) ℕ' by definition .
The proofs of items 4, 5, 6, 7 and 8 are left as exercises.
QED
A stronger version of the next result will be proved later.
(See Lemma 5.10.)
Let φ be quantifier-free sentence.
Assume that ℕ ⊨ φ .
Then Q ⊢ φ .
Sometimes people refer to this fact by saying "all true quantifier-free sentences of arithmetic are theorems of Robinson Arithmetic."
(They use "true" to mean the sentence holds in ℕ.)
Proof of Lemma 5.2
Assume φ is quantifier-free and ℕ ⊨ φ .
By the Completeness Theorem 3.15, it is enough to show that Q ⊨ φ .
Consider an arbitrary model ℕ' of Q.
Let π : ω → | ℕ' | be defined as in the Lemma 5.1.
Write ℕ' ↾ ran ( π ) for the substructure of ℕ' whose universe is ran ( π ) .
By Lemma 4.1, ℕ' ↾ ran ( π ) ⊨ φ .
By Lemma 4.3, ℕ' ⊨ φ .
QED
By Axiom 4,
Q ⊢ ∀ u A ( u , Z ) ≈ u .
By Lemma 5.1, for each n ∈ ω ,
Q ⊢ A ( Z , S n ( Z ) ) ≈ S n ( Z ) .
However, it turns out that
Q ⊬ ∀ v A ( Z , v ) = v .
In other words, Q is not strong enough to prove that zero is the left additive identity.
[ RETURN TO WHY AT SOME POINT. ]
In the proof of Lemma 5.1, we considered an arbitrary model ℕ' of Q.
Induction on ω was used "externally" to see that members of an initial segment of | ℕ' | have certain properties in ℕ'.
This suggests adding induction axioms that might allow us to work "internally" to see that all members of | ℕ' | have these properties in ℕ'.
For example, assuming that ℕ' satisfies the right induction axiom, we hope to prove Aℕ' ( Zℕ' , x ) = x for every x ∈ | ℕ' | .
To begin to implement this plan, we introduce infinitely many induction axioms by way of a scheme.
Assume the free variables of φ are v and wi for i < n.
Let Iφ be the sentence
∀ w̅ ( ( ∀ v ( ∀ u ( L ( u , v ) → φ ( v / u ) ) → φ ) → ∀ v φ ) )
By the principle of mathematical induction, ℕ ⊨ Iφ.
The proof of this principle uses the fact that the usual linear ordering of ω is a wellordering.
Recall from Exercise 4.5 that it is not possible to express wellordering in a first-order way, not even with infinitely many axioms.
Then ℕ ⊨ PA .
We claim that Peano Arithmetic has this theorem.
That is,
PA ⊢ ∀ v A ( Z , v ) ≈ v .
Let ℕ' be a model of PA.
We must show that ℕ' ⊨ ∀ v A ( Z , v ) ≈ v .
Now we have that ℕ' ⊨ I A ( Z , v ) ≈ v .
Therefore, it suffices to see that
ℕ' ⊨ ∀ v ( ∀ u ( L ( u , v ) → A ( Z , u ) ≈ u ) → A ( Z , v ) ≈ v )
Consider an arbitrary y ∈ | ℕ' | such that
for every x ∈ | ℕ' |, if Lℕ' ( x , y ), then Aℕ' ( Zℕ' , x ) = x.
To finish, we must show that
A ℕ' ( Z ℕ' , y ) = Z ℕ' .
Because ℕ' satisfies Axiom 4 ,
A ( Z , Z ) ℕ' = Z ℕ' .
So we may assume y ≠ Zℕ'.
Since ℕ' satisfies Axiom 3,
there exists x ∈ | ℕ' | such that Sℕ' ( x ) = y .
Since ℕ' satisfies Axiom 5 and 4,
A ℕ' ( x , S ( Z ) ℕ' ) = S ℕ' ( A ℕ' ( x , Z ℕ' ) ) = S ℕ' ( x ) = y .
Then Lℕ' ( x , y ) because ℕ' satisfies Axiom 10 .
By our assumption about y ,
Aℕ' ( Zℕ' , x ) = x.
Since ℕ' satisfies Axiom 5 ,
Aℕ' ( Zℕ' , y ) = Aℕ' ( Zℕ' , Sℕ' ( x ) ) = Sℕ' ( Aℕ' ( Zℕ' , x ) ) = Sℕ' ( x ) = y .
So we are done.
Thus, adding the induction axiom I A ( Z , v ) ≈ v to Robinson Arithmetic had the desired effect.
Obviously, Theory ( ℕ ) ⊃ PA.
Notice that Theory ( ℕ ) is a complete and consistent theory in the language of arithmetic.
Axioms 1-3 of Robinson Arithmetic formalize the idea that the successor function n ↦ n + 1 is a bijection from ω to ω - { 0 }.
The partial inverse of the successor is the predecessor n ↦ n ∸ 1 where ( n + 1 ) ∸ 1 = n and 0 ∸ 1 = 0 .
It is a surjection from ω to ω.
It is an injection from { n ∈ ω ∣ n > 0 } to ω.
It is definable over ℕ.
To see this, let PRED ( u , v ) be the first-order formula
( u ≈ Z → v ≈ Z ) ∧ ( ( ¬ ( u ≈ Z ) ) → S ( v ) ≈ u )
Then, for all natural numbers m and n,
m = n ∸ 1 iff ℕ ⊨ PRED ( m , n ) .
Because PRED is quantifier-free, by Lemma 5.2,
m = n ∸ 1 iff Q ⊢ PRED ( S ( Z ) m , S ( Z ) n ) .
It is also easy to see using Axioms 1-3 that
Q ⊢ ∀ u ∃ v PRED ( u , v )
and
Q ⊢ ∀ u ∀ v ∀ v' ( ( PRED ( u , v ) ∧ PRED ( u , v' ) ) → v ≈ v' )
The combination of these two deductions is equivalent to saying that for every model ℕ' of Q, if we define a binary relation by setting
PREDℕ' = { ( x , y ) ∣ ℕ' ⊨ PRED ( x , y ) }
then PREDℕ' is a unary function from | ℕ' | to | ℕ' |.
Thus the formula PRED provides a uniform way of defining a function PREDℕ' over any model ℕ' of Q .
Once we know that the relation PREDℕ' is a function, it is easier on the eyes to write PREDℕ' ( x ) = y rather than ( x , y ) ∈ PREDℕ' or PREDℕ' ( x , y ) .
Our original predecessor function n ↦ n ∸ 1 is just PREDℕ .
It is also easy to see that
Q ⊢ ∀ u PRED ( S ( u ) , u )
and
Q ⊢ ∀ u ∀ v ( ( ( ¬ u ≈ Z ) ∧ PRED ( u , v ) ) → S ( v ) ≈ u ) .
By the Completeness Theorem, this is equivalent to saying that for every model ℕ' of Q and x ∈ | ℕ' | ,
PREDℕ' ( Sℕ' ( x ) ) = x
and
if x ≠ Zℕ', then Sℕ' ( PREDℕ' ( x ) ) = x .
Therefore PRED defines a similar kind of predecessor function over every model of Q not just over ℕ .
Finally, we remark that there are other formulas we could have used above instead of PRED ; for example, PRED ∨ ⊥ .
§ 5.2 Nonstandard models of arithmetic via compactness
Structures with the same theory are said to be elementary equivalent.
Isomorphic structures are elementary equivalent.
There are models of Theory ( ℕ ) that are not isomorphic to ℕ .
In this and the next subsection, we will see this two different ways to produce such models.
Let I be a new constant symbol and
Σ = Theory ( ℕ ) ∪ { ¬ Sn ( Z ) ≈ I ∣ n ∈ ω }.
Clearly, every finite subtheory of Σ has a model.
By the Compactness Theorem, Σ has a model; say
ℕ* = ( | ℕ* | , Zℕ* , Sℕ* , Aℕ* , Mℕ* , Eℕ* , Lℕ* , Iℕ* )
is a model of Σ .
Let ℕ' be the reduction of ℕ* to the language of arithmetic.
So
ℕ' = ( | ℕ' | , Zℕ' , Sℕ' , Aℕ' , Mℕ' , Eℕ' , Lℕ' ) = ( | ℕ* | , Zℕ* , Sℕ* , Aℕ* , Mℕ* , Eℕ* , Lℕ* )
Clearly, ℕ' ⊨ Theory ( ℕ ).
We claim that there is exactly one elementary embedding from ℕ to ℕ' .
To see this, suppose that π is a map from | ℕ | = ω to | ℕ' | = | ℕ* |.
Part of what it would mean for π to be an elementary embedding is that the following are equivalent for every natural number n:
π ( Sn ( Z ) ℕ ) = Sn ( Z ) ℕ' .
In other words, for every natural number n,
π ( n ) = Sn ( Z ) ℕ' .
So, if there exists an elementary embedding from ℕ to ℕ', it must be this particular map π.
Moreover, this map π really is an elementary embedding.
To see this, let φ be a formula with free variables among vi for i < j and consider any natural numbers ni for i < j.
Then the following are equivalent:
The equivalence of the first and last conditions above tell us that π is an elementary embedding from ℕ to ℕ' .
Because ℕ* is a model of Σ, for every natural number n,
ℕ* ⊨ ¬ Sn ( Z ) ≈ I
which implies that
π ( n ) ≠ Iℕ* ,
hence
range ( π ) ≠ | ℕ' | .
Therefore, π is not a surjection.
It is worthwhile gaining a better mental picture of ℕ'.
The first-order axioms for L being a linear ordering belong to Theory ( ℕ ).
Therefore, Lℕ' is a linear ordering of | ℕ' |.
We claim that the following is an initial segment of this linear ordering:
π ( 0 ) = Zℕ'
π ( 1 ) = S ( Z )ℕ'
π ( 2 ) = S ( S ( Z ) )ℕ'
⋮
π ( n ) = Sn ( Z )ℕ'
⋮
The Lℕ'-least point is Zℕ' because the sentence
∀ v ( ( ¬ v ≈ Z ) → L ( Z , v ) )
belongs to Theory ( ℕ).
For each natural number n, Sn+1 ( Z )ℕ' is the least point greater than Sn ( Z )ℕ' in terms of the ordering Lℕ'.
This is because, for each natural number n, the sentence
L ( Sn ( Z ) , Sn+1 ( Z ) ) ∧ ∀ v ¬ ( L ( Sn ( Z ) , v ) ∧ L ( v , Sn ( Z ) ) )
belongs to Theory ( ℕ' ).
Thus the claim is established.
The points listed in the claim form an elementary substructure of ℕ' which we call the standard part of ℕ'.
Notice that π is an isomorphism from ℕ to the standard part of ℕ'.
To simplify notation, let us use the abbreviations
ℕ' = ( | ℕ' | , Zℕ' , Sℕ' , Aℕ' , Mℕ' , Eℕ' , Lℕ' ) = ( | ℕ' | , Z' , S' , A' , M' , E' , L' )
Also, abbreviate Sℕ' by S' .
The standard part of ℕ' drawn again horizontally using these abbreviations looks like:
Z' S' ( Z' ) ( S' )2 ( Z' ) ( S' )3 ( Z' ) ⋅ ⋅ ⋅ ( S' )n ( Z' ) ⋅ ⋅ ⋅
As we saw above, Iℕ* is a nonstandard member of ℕ' so greater than any standard member in terms of L'.
Consider any nonstandard y ∈ | ℕ' | .
Abbreviate PREDℕ' by P'.
We associate to y the following segment of the ordering L'.
⋅ ⋅ ⋅ ( P' )n ( y ) ⋅ ⋅ ⋅ ( P' )3 ( y ) ( P' )2 ( y ) P' ( y ) y S' ( y ) ( S' )2 ( y ) ( S' )3 ( y ) ⋅ ⋅ ⋅ ( S' )n ( y ) ⋅ ⋅ ⋅
There are no points between those we listed and all the points we listed are above all standard points.
We omit the little argument that shows this.
Notice that this segment associated to y ordered by L' is isomorphic to ℤ ordered in the usual way.
There are other points of ℕ' that are neither standard nor in the segment associated to y.
For example, let z = A' ( y , y ).
Consider the segment associated to z.
⋅ ⋅ ⋅ ( P' )n ( z ) ⋅ ⋅ ⋅ ( P' )3 ( z ) ( P' )2 ( z ) P' ( z ) z S' ( z ) ( S' )2 ( z ) ( S' )3 ( z ) ⋅ ⋅ ⋅ ( S' )n ( z ) ⋅ ⋅ ⋅
Each of these points is above every point in the segment associated to y.
We omit the little argument that shows this.
Here is another example.
There is a first-order sentence that reflects the fact that n is even or n + 1 is even.
Namely,
∀ v ∃ u ( A ( u , u ) ≈ v ∨ A ( u , u ) ≈ S ( v ) ) .
This sentence belongs to Theory ( ℕ ) so it holds in ℕ'.
So there exists x ∈ | ℕ' | such that A' ( x , x ) = y or A' ( x , x ) = S' ( y ) .
Consider the segment associated to x.
⋅ ⋅ ⋅ ( P' )n ( x ) ⋅ ⋅ ⋅ ( P' )3 ( x ) ( P' )2 ( x ) P' ( x ) x S' ( x ) ( S' )2 ( x ) ( S' )3 ( x ) ⋅ ⋅ ⋅ ( S' )n ( x ) ⋅ ⋅ ⋅
Each of these points is between every standard point and every point on the segment associated to y.
We omit the little argument that shows this.
Pressing on in this way, one can show that the linear ordering on the segments associated to points is dense and has a left end-point but no right end-point.
Here is a way to make this conclusion more precise.
Define x ∼ y iff at least one of the following holds:
Remark: The only way both can hold is if x = y and z = Z'.
Then ∼ is an equivalence relation on | ℕ' | and [ x ]∼ is the segment of L' associated to x.
Define a binary relation L' / ∼ on | ℕ' | by setting
[ x0 ]∼ ( L' / ∼ ) [ y0 ]∼ iff x L' y for every x ∼ x0 and y ∼ y0 .
We conclude that ( | ℕ' | / ∼ , L' / ∼ ) is a dense linear ordering.
It has a left end-point, namely [ Z' ]∼ .
But it has no right end-point.
§ 5.3 Nonstandard models of arithmetic via ultrapowers
Let U be a nonprincipal ultrafilter over ω.
Let ℕ' = Ult ( ℕ , U ).
Recall Theorem 4.19, which tells us that the map
π : n ↦ [ i ↦ n ]U
is an elementary embedding from ℕ to ℕ'.
So, letting ℕ* be the restriction of ℕ' to ran ( π ), we know that π : ℕ ≈ ℕ* and ℕ* ≼ ℕ'.
For every n ∈ ω ,
This is exactly how we defined π in the previous subsection, so the situations are very similar.
Next we identify an infinite element of ℕ'.
Let e : i ↦ i.
In other words, e is the identity function on ω.
Then, for every m ∈ ω ,
Lℕ' ( π ( m ) , [ e ]U ) using the definitions.
Therefore, [ e ]U is an element of | ℕ' | that is strictly greater than every member of | ℕ* | in terms of the linear ordering Lℕ'.
So far, we know ℕ' has finite members, namely those of the form π ( n ), and one infinite member, namely [ e ]U .
One way to obtain other infinite members of ℕ' is by adding finite members to [ e ]U .
Here is a nice way to view this.
Aℕ' ( [ e ]U , π ( n ) ) = Aℕ' ( [ i ↦ i ]U , [ i ↦ n ]U ) = [ i ↦ i + n ]U
We can also subtract π ( n ) from [ e ]U as follows.
Clearly, the function i ↦ i - n maps { i ∈ ω ∣ i ≥ n } to ω.
We can construe i ↦ i - n as a function from ω to ω by saying i - n = 0 whenever i < n.
With this convention, we can say
Aℕ' ( [ i ↦ i - n ]U , [ i ↦ n ]U ) = [ i ↦ i ]U
To see why, use the definition of Aℕ' or Łoś's Theorem and the fact that { i ∈ ω ∣ i ≥ n } ∈ U because U is nonprincipal.
This shows that, in ℕ', if we subtract π ( n ) from [ e ]U , we get [ i ↦ i - n ]U.
Another sort of infinite number is obtained by adding [ e ]U to itself. Namely,
Aℕ' ( [ e ]U , [ e ]U ) = Aℕ' ( [ i ↦ i ]U , [ i ↦ i ]U ) = [ i ↦ i + i ]U .
It is easy to see that adding and substracting finite numbers from [ i ↦ i + i ]U leads to numbers that are strictly greater than [ e ]U.
Of course, adding [ e ]U to itself is the same as doubling it. That is,
Mℕ' ( π ( 2 ) , [ e ]U ) = Aℕ' ( [ e ]U , [ e ]U ) .
We can also halve [ e ]U by considering the function which takes i to i / 2 if i is even and i to ( i - 1 ) / 2 if i is odd.
Abbreviate this function by i ↦ i / 2.
It is easy to see that [ i ↦ i / 2 ]U is an infinite number strictly less than [ e ]U.
Also,
adding and subtracting
finite numbers from
[ i ↦ i / 2 ]U
leads to infinite numbers that are strictly less than
[ e ]U.
§ 5.4 Arithmetic definability hierarchy
Bounded formulas in the language of arithmetic are defined by recursion:
∃ u ( L ( u , t ) ∧ φ )
∀ u ( L ( u , t ) → φ )
Sometimes we abbreviate the last two formulas as ∃ u L t φ and ∀ u L t φ .
∃ u L t is the bounded existential quantifier corresponding to "there exists u less than t".
∀ u L t is the bounded universal quantifier corresponding to "for every u less than t".
The reason we do not allow u as a variable of t is that the quantifiers ∃ u L S ( u ) and ∀ u L S ( u ) would amount to nothing more than ∃ u and ∀ u respectively.
There is a normal form for bounded formulas in which all of the bounded quantifiers lead a quantifier-free formula. See Exercise 5.7.
Bounded formulas have two other names:
Σ0 formulas
Π0 formulas
This is the base step of a recursive definition that continues as follows.
Σn+1 formulas in the language of arithmetic are those of the form
∃ w̅ φ
where φ is a Πn formula.
Πn+1 formulas in the language of arithmetic are those of the form
∀ w̅ φ
where φ is a Σn formula.
Consider an arbitrary R ⊆ ωk.
Keep in mind that two formulas may be needed to witness that R is a Δnℕ relation.
Obviously, Δ0ℕ means the same thing as Σ0ℕ and Π0ℕ.
We identify ω and ω1 in the obvious way to define Σnℕ, Πnℕ and Δnℕ sets.
A k-ary relation R on ω is called computable iff there is a computer program that takes k-tuples of natural numbers as inputs and decides whether they belong to R.
A k-ary relation R on ω is called computable enumerable iff there is a computer program that outputs the members of R given infinite space and time.
The last two definitions depend on the choice of programming language, so pick one, like Fortran.
Every Δ0ℕ relation is computable.
Sketch
Dealing with sets instead of relations contains all the ideas.
Say A = { n ∈ ω ∣ ℕ ⊨ φ ( n ) } where φ ( u ) is a bounded formula.
The proof of Lemma 5.3 is by induction on the complexity of φ
Begin by noting that if t ( v̅ ) is a term, then there is a computer program that computes the function n̅ ↦ tℕ ( n̅ ).
This is because computers can add, multiply, divide and exponentiate, and they can compose functions.
Next note that, given terms s ( u̅ ) and t ( v̅ ), there is a computer program that takes pairs ( m̅ , n̅ ) as inputs and decides whether s ( m̅ )ℕ = t ( n̅ )ℕ.
The same is true for s ( m̅ )ℕ < t ( n̅ )ℕ .
It follows that Lemma 5.3 holds for atomic formulas.
Computers can be programmed to use truth tables; with these we get through the recursive steps for ¬, ∧, ∨, → and ↔.
The bounded quantifiers ∃ u L t ( v̅ ) and ∀ u L t ( v̅ ) are handled using bounded search algorithms.
In other words, given n̅, we can instruct the computer to check all m < t ( n̅ )ℕ using a previously established subroutine.
With this, we see how to get through the recursive steps for bounded quantification.
QED
Every Σ1ℕ relation is computably enumerable.
Sketch
Dealing with sets instead of relations contains all the ideas.
Dealing with one existential quantifier instead of finitely many contains all the ideas.
Say A = { n ∈ ω ∣ ℕ ⊨ ∃ u φ ( u , n ) } where φ ( u , v ) is a bounded formula.
By Lemma 5.3, we have a subroutine which computes the Δ0ℕ relation { ( m , n ) ∈ ω × ω ∣ ℕ ⊨ φ ( m , n ) }.
Let ( mi , ni ) for i ∈ ω be one of the usual ways to enumerate pairs of natural numbers.
There is another subroutine which takes i as an input and outputs ( mi , ni ).
Using these subroutines, instruct the computer to test whether
ℕ ⊨ φ ( m0 , n0 )
and output n0 if the result is positive, then test whether
ℕ ⊨ φ ( m1 , n1 )
and output n1 if the result is positive etc.
Obviously, given infinite space and time, this program computably enumerates A.
QED
The program above might repeat outputs but this can be avoided by simply refusing to output the same number twice.
The program might not list the members of A in increasing order, which might be impossible to do.
Notice that if there is a program which lists A in increasing order, then A is computable.
This is because, in order to decide whether n ∈ A , we just wait until a number greater than or equal to n appears on the increasing list.
Later, we will see that not every computably enumerable set is computable.
The next result strengthens Lemma 5.3.
Every Δ1ℕ relation is computable.
Sketch
Let R be a Δ1ℕ relation.
Say R is k-ary and S = ωk - R.
Then both R and S are Σ1ℕ relations.
By Lemma 5.4, there is a program that enumerates the members of R as
r̅0 , r̅1 , r̅2 , …
and another program that enumerates the members of S as
s̅0 , s̅1 , s̅2 , …
To decide whether a given n̅ belongs to R we just wait until it appears on one of the two lists as it will.
If n̅ = r̅i for some i ∈ ω, then R ( n̅ ).
If n̅ = s̅i for some i ∈ ω, then S ( n̅ ) so not R ( n̅ ).
QED
Every computable relation on ℕ is Δ1ℕ.
Every computably enumerable relation on ℕ is Σ1ℕ.
We cannot even sketch Lemma 5.6 without specifying a computer language and doing an induction on its programs.
Remember that functions are special kinds of relations.
In particular, if f is a function, then f = { ( x , f ( x ) ) ∣ x ∈ dom ( f ) } .
Here are two useful results about functions which are Σ1ℕ relations.
Consider a set A ⊆ ω and a function f : A → ω .
Suppose that f is a Σ1ℕ relation.
Then A is a Σ1ℕ set.
Sketch
Use the fact that
m ∈ A iff there exists n ∈ ω such that f ( m ) = n.
QED
Consider a set A ⊆ ω and a function f : A → ω .
Suppose that A is a Δ1ℕ set f is a Σ1ℕ relation.
Then f is a Δ1ℕ relation.
Moreover, there is a Δ1ℕ function g : ω → ω such that f = g ↾ A .
Sketch
That f is a Π1ℕ relation follows easily from the fact that
f ( m ) = n iff m ∈ A and for every n' ∈ ω , if f ( m ) = n' , then n = n' .
Define g ( m ) = f ( m ) if m ∈ A and g ( m ) = 0 if m ∉ A .
Clearly, g works.
QED
In particular, every computably enumerable function from ω to ω is computable.
This follows from Lemmas 5.3, 5.4 and 5.7,
Lemma 5.8 remains true if all instances of Δ1ℕ and Σ1ℕ are replaced by Δ0ℕ by the same proof.
Since this fact will be used later, let us record it.
Consider a set A ⊆ ω and a function f : A → ω .
Suppose that A is a Δ0ℕ set f is a Δ0ℕ relation.
Then there is a Δ0ℕ function g : ω → ω such that f = g ↾ A .
§ 5.5 True existential sentences are theorems of Robinson Arithmetic
Recall Lemma 5.1 says that if a bounded sentence holds in ℕ, then it is a theorem of Robinson Arithmetic.
Here is an illustration that motivates a stronger fact.
Example
Let φ be a bounded sentence of the form
∀ u L s ∃ v L t ψ
where s and t are closed terms and ψ ( u , v ) is a quantifier-free formula.
Say m = sℕ and n = tℕ and assume for simplicity that neither is zero.
For each i < m, let ψ i be the disjunction
ψ ( S i ( Z ) , Z ) ∨ ⋅ ⋅ ⋅ ∨ ψ ( S i ( Z ) , S j ( Z ) ) ∨ ⋅ ⋅ ⋅ ∨ ψ ( S i ( Z ) , S n-1 ( Z ) ) .
Then let φ* be the conjunction
ψ 0 ∧ ⋅ ⋅ ⋅ ∧ ψ i ∧ ⋅ ⋅ ⋅ ∧ ψ n-1 .
Obviously, φ* is quantifier-free and
ℕ ⊨ φ ↔ φ* .
Now suppose that ℕ' is an arbitary model of Q.
Let π be defined as in Lemma 5.1.
Then sℕ' = π ( sℕ ) = π ( m ) = Sm ( Z ) ℕ' and tℕ' = π ( tℕ ) = π ( n ) = Sn ( Z ) ℕ' .
Moreover, π is an isomorphism from the usual linear ordering of ω to an initial segment of the linear ordering Lℕ' of | ℕ' | .
In particular, according to L ℕ', the first m members of ℕ' are
Z ℕ' S ( Z ) ℕ' ⋅ ⋅ ⋅ Si ( Z ) ℕ' ⋅ ⋅ ⋅ Sm-1 ( Z ) ℕ'
and the first n members of ℕ' listed according to L ℕ' are
Z ℕ' S ( Z ) ℕ' ⋅ ⋅ ⋅ Sj ( Z ) ℕ' ⋅ ⋅ ⋅ Sn-1 ( Z ) ℕ' .
From this and the way we constructed φ* , it is clear that ℕ' ⊨ φ ↔ φ* .
By Lemma 5.2,
ℕ ⊨ φ* iff ℕ' ⊨ φ* .
Therefore,
ℕ ⊨ φ iff ℕ' ⊨ φ .
From this we conclude that, in the example, if ℕ ⊨ φ , then Q ⊢ φ .
(The converse too but that is obvious.)
Let φ be Σ1 sentence.
Assume that ℕ ⊨ φ .
Then Q ⊢ φ .
Sketch
Say φ is ∃ u̅ ψ ( u̅ ) where u̅ is an ℓ-tuple of variables and ψ is a bounded formula.
Assume that ℕ ⊨ φ .
Let ℕ' be an arbitrary model of Q.
Pick n̅ ∈ ω ℓ such that ℕ ⊨ ψ ( n̅ ) .
Let χ be the bounded sentence
ψ ( S n0 ( Z ) , … , S nℓ - 1 ( Z ) ) .
Then
ℕ ⊨ χ .
By Exercise 5.7, we may assume that all the bounded quantifiers of χ lead a quantifier-free subformula.
Next prove by induction that there is a quantifier-free sentence χ* such that
ℕ ⊨ χ ↔ χ* .
and
ℕ' ⊨ χ ↔ χ* .
The proof is by induction on the number of quantifiers of χ and uses the idea illustrated in the example above.
By Lemma 5.2,
ℕ' ⊨ χ .
Therefore,
ℕ' ⊨ φ .
QED
§ 5.6 Coding tuples of natural numbers
Let pi be the i'th prime number.
So p0 = 2 , p1 = 3 , p2 = 5 etc.
Given a k-tuple n̅ of natural numbers, define the code of n̅ to be the product
∏ i < k pi1 + ni .
This only makes sense if k > 0 .
The coding function that maps each k-tuple to its code is an injection.
Its inverse is the decoding function which maps the code of each k-tuple back to the k-tuple.
The following are Δ0ℕ .
The relation { ( m , n ) ∈ ω × ω ∣ m divides n } .
The set of primes.
The increasing enumeration of the primes.
For each fixed k > 0, the function that maps each k-tuples to its code.
The set of codes of tuples.
The function that maps c to k whenever c is the code of a k-tuple.
The function that maps ( c , i ) to ni whenever c is the code of a k-tuple n̅ and i < k .
Notice that some of the functions listed in Lemma 5.11 are not total in the sense that they do not have domain ω.
But their domains are Δ0ℕ sets so we can extend each to a total Δ0ℕ function by mapping points outside its domain to zero (or any other default value).
This is the content of Lemma 5.9.
Several times later in the book we will make implicit use of this fact without additional comment.
Sketch of Lemma 5.11.
Let DIVIDES ( u , w ) be the bounded formula
u ≈ w ∨ ∃ v L w ( M ( u , v ) ≈ w )
Then m divides n iff ℕ ⊨ DIVIDES ( m , n ) .
Let PRIME ( v ) be the bounded formula
L ( S ( Z ) , v ) ∧ ∀ u L v ( DIVIDES ( u , v ) → u ≈ S ( Z ) ).
Then p is a prime number iff ℕ ⊨ PRIME ( p ) .
Now we go out of order and deal with a few extra sets, relations and functions.
Let TUPLE ( w ) be the bounded formula
L ( S ( Z ) , w ) ∧ ∀ v L w ∀ u L v ( ( PRIME ( u ) ∧ PRIME ( v ) ∧ DIVIDES ( v , w ) ) → DIVIDES ( u , w ) ) .
Then c is the code of a tuple iff ℕ ⊨ TUPLE ( c ) .
Let NEXTPRIME ( u , w ) be the bounded formula
L ( u , w ) ∧ PRIME ( w ) ∧ ∀ v L w ( ¬ L ( u , v ) ∨ ¬ PRIME ( v ) ).
Then p is the least prime strictly greater than n iff ℕ ⊨ NEXTPRIME ( n , p ) .
Notice that the code of the k-tuple
( 0 , 1 , 2 , … , k-1 )
is the product
21 ⋅ 3 2 ⋅ 5 3 ⋅ ⋅ ⋅ pk-1 k .
For future reference, this product is obviously less than ( pk-1 k ) k.
For lack of a better name, let us refer to ( 0 , 1 , 2 , … , k-1 ) as a "counting" k-tuple.
It will be useful to show that the codes of counting tuples form a Δ0ℕ set.
Let COUNTINGTUPLE ( w ) be the following bounded formula.
TUPLE ( w ) ∧ DIVIDES ( S2 ( Z ) , w ) ∧ ¬ DIVIDES ( S4 ( Z ) , w ) ∧
∀ u L w ∀ u' L w ∀ v L w
( ( PRIME ( u ) ∧ PRIMESUCCESSOR ( u , u' ) ∧ DIVIDES ( E ( u , v ) , w ) ∧ ¬ DIVIDES ( E ( u , S ( v ) ) , w ) )
→ ( DIVIDES ( u' , w ) ↔ ( ( DIVIDES ( E ( u' , S ( v ) ) , w ) ∧ ¬ DIVIDES ( E ( u' , S2 ( v ) ) , w ) ) ) )
Then c is the code of a counting tuple iff ℕ ⊨ COUNTINGTUPLE ( c ) .
Let LISTOFPRIMES ( u , v ) be the bounded formula
PRIME ( v ) ∧
∃ w L E ( E ( v , S ( u ) ) , S ( u ) ) ( COUNTINGTUPLE ( w ) ∧ DIVIDES ( E ( v , S ( u ) ) , w ) ∧ ¬ DIVIDES ( E ( v , S2 ( u ) ) , w ) )
Then q = pi iff ℕ ⊨ LISTOFPRIMES ( i , q ) .
This shows that the map i ↦ pi is a Δ0ℕ function.
Let COORDINATE ( w , u , v ) be the bounded formula
TUPLE ( w ) ∧
∃ x L w ( LISTOFPRIMES ( u , x ) ∧ DIVIDES ( E ( x , S ( v ) ) , w ) ∧ ¬ DIVIDES ( E ( x , S2 ( v ) ) , w ) )
Then, for all c , i and m,
ℕ ⊨ COORDINATE ( c , i , m )
iff
there is a k-tuple n̅ such that c is the code of n̅ , i < k and m = ni .
This shows that the map
( ∏ i < k pi1 + ni , i ) ↦ ni
is a Δ0ℕ function.
We leave the remaining details to the student.
QED
Here are some useful ways to manipulate quantifiers.
Trick #1
Consider a sentence φ ( x̅ ) of the form
∃ u ∃ v ψ ( u , v , x̅ )
Let φ* be the sentence
∃ w ( TUPLE ( w ) ∧ DIV ( S3 ( Z ) , w ) ∧
∃ u L w ∃ v L w ( COORDINATE ( w , Z , u ) ∧ COORDINATE ( w , S ( Z ) , v ) ∧ ψ )
Then
ℕ ⊨ ∀ x̅ ( φ ↔ φ* )
Generalizing, this shows how in some cases we can combine finitely many existential quantifiers if we are willing to allow more bounded quantifiers on the inside.
In particular, the formula that witnesses a set, relation or function is Σ1ℕ can be taken to have just one existential quantifier followed by a bounded formula.
The dual to trick #1
Consider a formula φ ( x̅ ) of the form
∀ u ∀ v ψ ( u , v , x̅ )
Let φ* ( x̅ ) be the formula
∀ w ( ( TUPLE ( w ) ∧ DIV ( S3 ( Z ) , w ) →
∃ u L w ∃ v L w ( COORDINATE ( w , Z , u ) ∧ COORDINATE ( w , S ( Z ) , v ) ∧ ψ ) ) .
Then
ℕ ⊨ ∀ x̅ ( φ ↔ φ* )
Generalizing, this shows how in some cases we can combine finitely many universal quantifiers if we are willing to allow more bounded quantifiers on the inside.
In particular, the formula that witnesses a set, relation or function is Π1ℕ can be taken to have just one universal quantifier followed by a bounded formula.
Trick #2
Consider a formula φ ( x̅ ) of the form
∀ u L t ( x̅ ) ∃ v ψ ( u , v , x̅ )
where t ( x̅ ) is a term.
Let φ* ( x̅ ) be the formula
∃ w ( TUPLE ( w ) ∧ LENGTH ( w , t ) ∧ ∀ u L t ∃ v L w ( COORDINATE ( w , u , v ) ∧ ψ ) )
Above, LENGTH is the bounded formula given by Lemma 5.11 such that LENGTHℕ is the function that maps the code for a k-tuple to k.
(Really, all we care about here is that the length is at least t.)
Then ℕ ⊨ ∀ x̅ ( φ ↔ φ* ) .
This is especially interesting when ψ is bounded because then φ* is Σ1
Generalizing, this shows that bounded quantification over Σ1 yields the same definitions as Σ1 over ℕ.
The dual to trick #2
Bounded quantification
over Π1 yields the same definitions
as Π1 over ℕ.
§ 5.8 Gödel numbers
We will use the coding of k-tuples from the previous section to assign numbers to symbols, terms and formulas.
Since we will also assign numbers to justifications of deductions and our deduction system allows for the introduction of new constants, we will consider the expansion of the language of arithmetic by constant symbols di for i ∈ ω.
These are called Gödel numbers.
The objects we are coding will be written between an upper left corner bracket ⌜ and an upper right corner bracket ⌝ .
The first step is to assign a Gödel number to each symbol of the language.
⌜ T ⌝ = 1
⌜ F ⌝ = 3
⌜ ¬ ⌝ = 5
⌜ ∧ ⌝ = 7
⌜ ∨ ⌝ = 9
⌜ → ⌝ = 11
⌜ ↔ ⌝ = 13
⌜ ∃ ⌝ = 15
⌜ ∀ ⌝ = 17
⌜ ≈ ⌝ = 19
⌜ Z ⌝ = 21
⌜ S ⌝ = 23
⌜ A ⌝ = 25
⌜ M ⌝ = 27
⌜ E ⌝ = 29
⌜ L ⌝ = 31
⌜ vi ⌝ = 33 + ( 4 × i )
⌜ di ⌝ = 35 + ( 4 × i )
We will use Polish notation for terms and formulas so parentheses are not needed.
Notice that codes for k-tuples are even while Gödel numbers for symbols of the language are odd.
Next define ⌜ t ⌝ for terms t by recursion.
We already defined ⌜ Z ⌝ , ⌜ vi ⌝ and ⌜ di ⌝ .
The recursive steps are:
⌜ S t ⌝ = the code of the pair ( ⌜ S ⌝ , ⌜ t ⌝ )
⌜ ⋄ s t ⌝ = the code of the triple ( ⌜ ⋄ ⌝ , ⌜ s ⌝ , ⌜ t ⌝ )
whenever ⋄ is one of the binary function symbols A , M or E.
Next we define ⌜ φ ⌝ for formulas φ by recursion.
We already defined ⌜ T ⌝ and ⌜ F ⌝
The other atomic cases are:
⌜ ≈ s t ⌝ = the code of the triple ( ⌜ ≈ ⌝ , ⌜ s ⌝ , ⌜ t ⌝ )
⌜ L s t ⌝ = the code of the triple ( ⌜ L ⌝ , ⌜ s ⌝ , ⌜ t ⌝ )
The recursive steps are:
⌜ ¬ φ ⌝ = the code of the pair ( ⌜ ¬ ⌝ , ⌜ φ ⌝ )
⌜ ⋄ ψ φ ⌝ = the code of the triple ( ⌜ ⋄ ⌝ , ⌜ ψ ⌝ , ⌜ φ ⌝ )
whenever ⋄ is one of binary logical connectives ∧ , ∨ , → or ↔ .
⌜ ⋄ vi φ ⌝ = the code of the triple ( ⌜ ⋄ ⌝ , ⌜ vi ⌝ , ⌜ φ ⌝ )
whenever ⋄ is one of the quantifiers ∃ or ∀ .
The following are Δ0ℕ .
• The set { ⌜ t ⌝ ∣ t is a term } .
• The set { ⌜ t ⌝ ∣ t is a term in the language of arithmetic } .
• The relation { ( ⌜ u ⌝ , ⌜ t ⌝ ) ∣ u is a variable of the term t } .
• The set { ⌜ t ⌝ ∣ t is a closed term } .
• The substitution function that maps the code of the triple
( ⌜ t ⌝ , ⌜ u ⌝ , ⌜ s ⌝ )
to
⌜ t ( u / s ) ⌝
whenever s and t are terms u is a variable.
• The set { ⌜ φ ⌝ ∣ φ is a formula } .
• The set { ⌜ φ ⌝ ∣ φ is a formula in the language of arithmetic } .
• The set { ⌜ φ ⌝ ∣ φ is a bounded formula in the language of arithmetic } .
• The set { ⌜ φ ⌝ ∣ φ is a Σ1 formula in the language of arithmetic } .
• The relation { ( ⌜ u ⌝ , ⌜ φ ⌝ ) ∣ u is a variable of the formula φ } .
• The set { ⌜ φ ⌝ ∣ φ is a sentence } .
• The set { ⌜ φ ⌝ ∣ φ is an axiom of PA } .
• The function that maps the code of the triple
( ⌜ φ ⌝ , ⌜ u ⌝ , ⌜ t ⌝ )
to
⌜ φ ( u / t ) ⌝
whenever φ is a formula, t is a term and u is a variable.
All of our purely syntactical notions and operations are Δ0ℕ in the codes.
Obviously, there are some we left off the list to keep it from getting too long.
Sketch of Lemma 5.12
We focus on why { ⌜ t ⌝ ∣ t is a term } is a Δ0ℕ set and leave the other calculations to the student.
(They might be included in lecture and added here later.)
An existential definition:
n is the Gödel number of a term iff there exists an ℓ-tuple
( m0 , … , mℓ-1 )
such that mℓ-1 = n and for every k < ℓ one of the following holds:
From this and Lemma 5.11, it is easy to see that { ⌜ t ⌝ ∣ t is a term } is a Σ1ℕ set.
Bounding the existential definition:
We need to find appropriate bounds on the size of ℓ and the code for m̅ in the existential definition above.
Observe that the Gödel numbers of terms increase with complexity.
(This can be proved by induction on the complexity of terms.)
So we may assume m̅ is a nondecreasing ℓ-tuple.
In particular, mk ≤ n for every k < ℓ.
We may also assume that ℓ ≤ n.
This stems from the fact that the Gödel number of a term bounds the number of subterms.
Now we start computing upper bounds for the code for m̅ using the assumptions that ℓ ≤ n and mk ≤ n for every k ≤ ℓ.
p0m0 ⋅ ⋅ ⋅ pℓ-1mℓ-1 ≤ pℓ-1n ⋅ ⋅ ⋅ pℓ-1n = ( pℓ-1n )ℓ < ( pnn )n = pnn2 .
We claim that
pn ≤ 2nn .
The claim implies that, in the existential definition, we may bound the code for m̅ as follows:
p0m0 ⋅ ⋅ ⋅ pℓ-1mℓ-1 < ( 2nn )n2
This is sufficient for our purposes since the bound is the evaluation in ℕ of the term
E ( E ( S2 ( Z ) , E ( n , n ) ) , E ( n , S2 ( Z ) ) )
The proof of the claim is by induction on n and has nothing to do with logic.
If n = 0, then p0 = 2 = 21 = 200 .
If n > 0, then using trivial number theory and the induction hypothesis we see that
pn < p0 ⋅ ⋅ ⋅ pn-1 ≤ pn-1 ⋅ ⋅ ⋅ pn-1 = pn-1n ≤ ( 2(n-1)(n-1) )n < ( 2n(n-1) )n = 2nn .
QED
The next step is to assign numbers to justifications of deductions from PA.
Unless otherwise noted, all formulas and theories are in the language of arithmetic expanded by the constant symbols symbols di for i ∈ ω .
The only justifications we will need to consider look like:
( ( Γ0 , φ0 ) , … , ( Γk , φk ) )
where, for every j ≤ k,
If there is such a justification, then we can extend it by one step using rule R1 to see that PA ⊢ φk .
Conversely, it is not hard to see that whenever φ is a theorem of PA, there is a justification of the form described above with φk equal to φ .
What we are claiming is a slight strengthening of the Finiteness of Deductions Lemma 3.10.
To arithmetize such justifications, we consider enumerations of each of the finite theories Γi .
Say Γi = { ψ0 , … , ψℓ - 1 } .
Then we let ni be the code for the ( ℓ + 1 )-tuple ( ⌜ ψ0 ⌝ , … , ⌜ ψℓ - 1 ⌝ , ⌜ φi ⌝ ).
Finally, define the Gödel number for the justification, which we write
⌜ ( ( Γ0 , φ0 ) , … , ( Γk , φk ) ) ⌝ ,
to be the code for the ( k + 1 )-tuple ( n0 , … , nk ) .
(1) The set of Gödel numbers for justifications is Δ0ℕ .
(2) The set of Gödel numbers for theorems of Q is Σ1ℕ .
(3) The set of Gödel numbers for theorems of PA is Σ1ℕ .
Sketch
To prove (1), look at the definition of ⌜ ( ( Γ0 , φ0 ) , … , ( Γk , φk ) ) ⌝ and apply the same ideas used to prove Lemma 5.12.
For (3), a sentence φ is a theorem of PA iff there exists a derivation of φ of the form described above.
Clearly, when we arithmetize this fact, it becomes Σ1ℕ .
Q is a finite subtheory of PA so (2) is like (3) but easier.
QED
By Lemma 5.6 and Lemma 5.12(3), we know that there is a computer program which lists all the theorems of PA.
This does not say that there is a program to decide whether a given sentence is a theorem of PA.
Whether there is such a program is a very interesting question!
The answer will be provided in the next chapter.
§ 5.9 Representable functions
Let f : ω → ω be a function and T be a theory.
Then f is representable in T iff there exists a formula φ ( u , v ) such that for every m ∈ ω,
T ⊢ φ ( S m ( Z ) , S f ( m ) ( Z ) )
and
T ⊢ ∀ v ( φ ( Sm ( Z ) , v ) → v ≈ S f ( m ) ( Z ) ) .
This seems like a slightly unnatural definition but it turns out to be useful.
If a function f : ω → ω is representable in Q, then f is representable in PA.
Proof
Obvious from the definition because Q is a subtheory of PA.
QED
Let f : ω → ω be a function that is representable in PA.
Then f is a Σ1ℕ function.
Sketch
Let φ ( u , v ) be a formula which represents f in PA.
By Lemma 5.14 (3), there is a Σ1 formula, call it THEOREMPA ( u ) , such that for every sentence ψ and n ∈ ω , the following are equivalent:
By calculation like those in the proof of Lemma 5.12, there is a bounded formula, call it
SPECIALSUBSTITUTION ( u , v , w ) ,
such that for all ℓ , m , n ∈ ω, the following are equivalent:
Let θ ( u , v ) be the formula
∃ w ( SPECIALSUBSTITUTION ( u , v , w ) ∧ THEOREMPA ( w ) ) .
Then θ is logically equivalent to a Σ1 formula and, for all m , n ∈ ω, the following are equivalent:
QED
Let f : ω → ω be a Σ1ℕ function.
Then f is a function that is representable in Q by a Σ1 formula.
Sketch
It is worth seeing the proof of something more modest first.
Assume f : ω → ω is a Δ0ℕ function.
Say φ ( u , v ) is a bounded formula such that for all m , n ∈ ω, the following are equivalent:
Let φ* be the formula
φ ∧ ∀ v' L v ( ¬ φ ( u , v' ) ) .
Clearly φ* is also bounded and defines f over ℕ too.
We claim that it represents f in Q.
The first thing we must check is that for every m ∈ ω,
Q ⊢ φ* ( Sm ( Z ) , Sf ( m ) ( Z ) ) .
This is immediate from Lemma 5.10 and the fact that ℕ ⊨ φ* ( m , f ( m ) ) .
The second thing we must check is that for every m ∈ ω,
Q ⊢ ∀ v ( φ* ( Sm ( Z ) , v ) → v ≈ S f ( m ) ( Z ) )
This follows from Lemmas 5.1 and 5.10 and the definition of φ* .
Now assume instead that f : ω → ω is a Σ1ℕ function.
Say φ ( u , v ) is a Σ1 formula such that for all m , n ∈ ω, the following are equivalent:
Say φ is ∃ w ψ where ψ is a bounded formula.
Let ψ* ( u , v , x ) be the Σ1 formula
∃ w ( TUPLE ( x ) ∧ LENGTH ( x , S2 ( Z ) ) ∧ COORDINATE ( x , Z , v ) ∧ COORDINATE ( x , S ( Z ) , w ) ∧ ψ ( u , v , w ) ) .
Let φ* ( u , v ) be the Σ1 formula
∃ x ( ψ* ( u , v , x ) ∧ ∀ x' L x ∀ v' L x' ( ¬ ψ* ( u , v' , x' ) ) )
Pushing the ideas above we see that ψ* represents f in Q.
QED
Consider any function f : ω → ω.
The following are equivalent.
• f is a Σ1ℕ function.
• f is a Δ1ℕ function.
• f is a computably enumerable function.
• f is a computable function.
• f is a function that is representable in PA.
• There is a Σ1 formula that represents f in PA.
• f is a function that is representable in Q.
• There is a Σ1 formula that represents f in Q.
Proof
Apply Lemmas 5.4, 5.5, 5.6, 5.8, 5.14, 5.15 and 5.16.
QED