2 Computability

“If a ‘religion’ is defined to be a system of ideas that contains improvable statements, then Gödel taught us that mathematics is not only a religion; it is the only religion that can prove itself to be on.” – John Barrow

2.1 Recursive functions and λ-computability

Definition 2.1.1 (Partial recursive function). The class of recursive functions is the smallest class of partial functions of the form ℕk→ℕ that contains the basic functions:

  • Projections: Πim:(n1,…,nm)↦ni;

  • Successor: S+:n↦n+1;

  • Zero: z:n↦0

and is closed under:

  • Compositions: if g:ℕk→ℕ is partial recursive and so are h1,…,hk:ℕm→ℕ, then the function f:ℕm→ℕ given by f(n¯)=g(h1(n¯),…,hk(n¯)) is partial recursive.

  • Primitive recursion: Given partial recursive functions g:ℕm→ℕ and h:ℕm+2→ℕ, the function f:ℕm+1→ℕ defined by

    {f(0,n¯):=g(n¯)f(k+1,n¯):=h(f(k,n¯),k,n¯)

  • Minimisation: Suppose g:ℕm+1→ℕ is partial recursive. Then the function f:ℕm→ℕ that maps n¯ to the least n such that g(n,n¯)=0 (if it exists) is partial recursive.

    Notation: f(n¯)=μn.g(n,n¯)=0.

The class of functions produced by the same conditions but excluding minimisation is called the class of primitive recursive functions.

A partial recursive function that is defined everywhere is called a total recursive function.

The terms of the untyped λ-calculus Λ are given by the grammar

Λ:=V|λV.Λ|ΛΛ,

where V is a (countable) set of variables.

The notions we previously discussed (α-equality, β-reduction, η-reduction, etc) apply tit for tat.

Example 2.1.2. Let ω:=λx.xx and Ω:=ωω. Then Ω=(λx.xx)ω→βωω=Ω. This shows that we can have an infinite reduction chain of λ-terms.

Question: If M↠βN, M↠βN′, do we have N↠βM′ and N′↠βM′ for some M′?

Idea: “Simultaneously reduce” all the redexes in M to get a term M∗. This might have new redexes, so we can iterate the process to get terms M2∗,M3∗,….

M should reduce to M∗, so we have M↠βM∗↠βM2∗,…. We’ll see that if M reduces to N in k steps, then N↠βMk∗.

Using this, we will show (assuming s≥r):

           M

  N2                 N1


                     M r∗

             s∗
srβββββ         M

To get there, we want to build M∗ with two properties:

Definition 2.1.3 (Takahashi Translation). The Takahashi translation M∗ of a λ-term M is recursively defined as follows:

  • (1)
    x∗:=x, for x a variable;
  • (2)
    If M=(λx.P)Q is a redex, then M∗:=P∗[x:=Q∗];
  • (3)
    If M=PQ is a λ-application, then M∗:=P∗Q∗;
  • (4)
    If M=λx.P is a λ-abstraction, then M∗:=λx.P∗.

These rules are numbered by order of precedence, in case of ambiguity. We also define M0∗:=M and M(n+1)∗:=(Mn∗)∗.

Note that M∗ is not necessarily in β-normal form, for example if M=(λx.xy)(λy.y), then

M∗=(xy)∗[x:=(λy.y)∗]=(xy)[x:=λy.y]=(λy.y)y.

Lemma 2.1.4. Assuming that:

Then
  • (1)
    FV⁡(M∗)⊆FV⁡(M);
  • (2)
    M↠βM∗;
  • (3)
    If M→βN, then N↠βM∗.

Proof. Induction over the structure of λ-terms. □

Lemma 2.1.5. Takahashi translation preserves β-contraction:

((λx.P)Q)∗↠β(P[x:=Q])∗.

Proof. By definition, ((λx.P)Q)∗=P∗[x:=Q∗]. By induction over the structure of P, we can check that:

Lemma 2.1.6. Assuming that:

  • M→βN

Then M∗↠βN∗.

Proof. Induction over the structure of M. We’ll leave the easier cases as exercises, and focus on when M is a redex, or when M=P1P2, where P1 is not a λ-abstraction and N=Q1P2 with P1→βQ1.

Suppose that M=(λx.P1)P2 is a redex. Then there are three possibilities for N.

Now suppose M=P1P2, where P1 is not a λ-abstraction, and N=Q1P2 with P1→βQ1. Here M∗=P1∗P2∗. If Q1 is not a λ-abstraction, the result is clear. So let Q1=λy.R. Applying the induction hypothesis to P1→βλy.R, we get P1∗↠βλy.R∗. Thus

M∗=P1∗P2∗↠β(λy.R∗)P2∗→βR∗[y:=P2∗]=N∗.□

Corollary 2.1.7. If M↠βN, then M∗→βN∗.

Proof. Induction over the length of the chain M↠βN, using Lemma 2.1.6. □

Applying this multiple times, M↠βN implies Mn∗↠βNn∗ for all n<ω.

Theorem 2.1.8. Assuming that:

Then N↠βMn∗.

Proof. By induction over n. The base case is clear, as n=0 implies M=N.

For n>0, there is a term R with M→βR→(n−1)βN. By induction hypothesis, N↠βRn−1∗. Since M→βR, we have R↠βM∗ by Lemma 2.1.4. Thus we get Rn−1∗↠βMn∗ by the previous observation. Putting it all together:

N↠βRn−1∗↠βMn∗.□

Theorem 2.1.9 (Church, Rosser, 1936). Assuming that:

  • M,N1,N2 are λ-terms such that M↠βN1,N2

Then there is a λ-term N such that N1,N2↠βN.

Proof. Say M→rβN1, M→sβN2. Without loss of generality, say r≤s. By Theorem 2.1.8, we have that N1↠βMr∗ and N2↠βMs∗. But Mr∗↠βMs∗ by successive applications of Lemma 2.1.4 (as r≤s). So take N=Ms∗. □

Reminder of the picture to think of:

           M


  N2                 N1

                       r∗
                     M

srβββββ         M s∗

This has some important consequences:

Example. λx.x and λx.λy.x are different terms in β-normal form, so they can’t be β-equivalent.

Definition 2.1.10 (Church numeral). Let n be a natural number. Its corresponding Church numeral cn is the λ-term cn:=λs.λz.sn(z), where sn(z) denotes

s(s(…⁡(s⏟n timesz)…⁡).

Example 2.1.11. c0=λs.λz.z is the ‘function’ that takes s to the identity map.

c1=λs.λz.λs(z) is the ‘function’ that takes s to itself.

c2=λs.λz.ss(z) takes a function s to its 2-fold composite z↦s(s(z)).

Definition 2.1.12 (lambda-definability). A partial function f:ℕk→ℕ is λ-definable if there is a λ-term F such that Fcn1…cnk≡βcf(n1,…,nk).

Proposition 2.1.13 (Rosser). Define the following λ-term:

  • A+:=λx.λy.λs.λz.xs(ys(z)),

  • A∗:=λx.λy.λs.x(ys),

  • Ae:=λx.λy.yx.

Then for all n,m∈ℕ:

  • A+cncm≡βcn+m;

  • A∗cncm≡βcnm;

  • Aecncm≡βcnm if m>0.

Proof. We’ll show that A+cncm≡βcn+m, and leave the rest to you.

First note that

cnsz=(λf.λx.fn(x))sz≡β(λx.sn(x))z≡βsn(z).

So:

A+cncm=(λx.λy.λs.λz.xs(ysz))cncm≡β(λy.λs.λz.cns(ysz))cm≡βλs.λz.cns(cmsz))≡βλs.λz.sn(smz)≡βλs.λz.sn(smz)≡βλs.λz.sm+n(z)≡βcn+m□

In a similar fashion, we can also encode binary truth-values:

Proposition 2.1.14. Define the λ-terms:

  • ⊤⁡:=λx.λy.x

  • ⊥:=λx.λy.y

  • (if B then P else Q:=BPQ)

Then for λ-terms P and Q, we have

  • (i)
    (if ⊤⁡ then P else Q)≡βP;
  • (ii)
    (if ⊥ then P else Q)≡βQ.

Proof. Just compute it! □

With this, we can encode logical connectives via:

We can also encode pairs: if we define [P,Q]:=λx.xPQ, then [P,Q]⊤⁡≡βP and [P,Q]⊥≡βQ. However, it is not true that [M⊤⁡,M⊥]≡βM!

Recursively defining terms within the λ-calculus requires a clever idea: we see such a term as a solution to a fixed point equation F=λx.M where F occurs somewhere in M.

Theorem 2.1.15 (Fixed Point Theorem). There is a λ-term Y such that, for all F:

F(YF)≡βYF.

Proof. Define

Y=λf.(λx.f(xx))λx.f(xx).

If we compute YF, we get:

YF=(λf.(λx.f(xx))λx.f(xx))F≡β(λx.F(xx))λx.F(xx)≡βF((λx.F(xx))(λx.F(xx)))≡βF((λf.(λx.f(xx))λx.f(xx))F)≡βF(YF)□

We call any combinator (i.e. a λ-term without free variables) Y satisfying the property F(YF)≡βYF for all terms F a fixed-point combinator.

Corollary 2.1.16. Given a λ-term M, there is a λ-term F such that F≡βM[f:=F].

Proof. Take F=Yλf.M. Then

F≡β(λf.M)Y(λf.M)≡β(λf.M)F≡βM[f:=F].□

Example 2.1.17. Suppose D is a λ-term encoding a predicate, i.e. Pcn≡β⊥ or ⊤⁡ for every n∈ℕ. Let’s write down a λ-termthat encodes a program that takes a number and computes the next number satisfying the predicate.

First consider

M:=λf.λx.(if (Px) then x else f(Sx)),

where S encodes the successor map. Our goal is to have M run on itself. This can be done by using the term F:=YM. Indeed:

Fcn≡β(if Pcn then cn else Fcn+1)

for every n∈ℕ.

Notation. λxsz.f will be short hand for λx.λs.λz.f (and the obvious generalisation to any number of variables, labelled in any way).

Lemma 2.1.18. The basic partial recursive functions are λ-definable.

Proof. The i-th projection ℕk→ℕ is definable by πik:λx1…λxk.xi.

Successor is implemented by S:=λx.λs.λz.s(xsz).

The zero map is given by Z:=λx.c0.

Just compute! □

Lemma 2.1.19. The class of λ-definable functions is closed under composition.

Proof. Say G is a λ-term defining g:ℕk→ℕ, and that λ-terms H1,…,Hk define h1,…,hk:ℕm→ℕ. Then the composite map f:n¯↦g(h1(n¯),…,hk(n¯)) is definable by the term

F:=λx1…xm:(G(H1x1…xm)…(Hkx1…xm))

by inspection. □

Lemma 2.1.20. The class of λ-definable functions is closed under primitive recursion.

Proof. Suppose f:ℕm+1→ℕ is obtained from h:ℕm+2→ℕ and g:ℕm→ℕ by primitive recursion.

f(0,n¯):=g(n¯)f(k+1,n¯):=h(f(k,n¯),k,n¯)

and the λ-terms H and G define h and h respectively.

We need a λ-term to keep track of a pair that records the current state of computation: the value of k and the value of f at that stage.

So define

T:=λp.[S(pπ1),H(pπ2)(pπ1)x1…xn],

which acts on a pair [ck,cf(k,n¯] by updating the iteration data. Then f ought to be definable by

F:=λx.λx1…xm.xT[c0,Gx1…xm]π2.

Indeed,

Fckcn1…cnm≡βckT[c0,Gcn1…cnm]π2≡βTk[c0,cg(π)]π2

by definition of ck, and since

T[ck,cf(k,π)]≡β[Sck,Hcf(k,n¯)ckcn1,…,cnm]≡β[ck+1,ch(f(k,n¯),k,n¯)]

we have

Fckcn1…cnm≡βTk([c0,Gcn1…cnm])π2≡βcf(k,n¯)

as needed. □

Lemma 2.1.21. The λ-definable functions are closed under minimisation.

Proof. Suppose G λ-defines g:ℕm+1→ℕ, and that f:ℕm→ℕ is defined from g by minimisation: f(n¯)=μk.g(k,n¯)=0.

We can λ-define f by implementing an algorithm that searches for the least k in the following way:

First define a term that can check if a Church numeral is c0, for example

zero?⁡:=λx.x(λy.⊥)⊤⁡.

You can check that

zero?⁡cn≡β{⊤⁡if n=0⊥otherwise.

Now we want a term that, on input k, checks if g(k,n¯)=0 and returns k if so, else runs itself on k+1. If we can do this, running it on input k=0 will perform the search.

Let:

Search⁡:=λf.λg.λk.λx1…⁡λxm.(if zero?⁡(gkx1…⁡xm) then k else (f(g(Sk)x1…⁡xm))),

and set

F:=λx1…λxm.(YSearch⁡)Gc0x1…⁡xm.

Note that

(YSearch⁡)Gckcn1…⁡cnm≡βSearch⁡(YSearch⁡)Gckcn1…⁡cnm,

which is

if zero?⁡(Gckcn1…⁡cnm) then ck else ((YSearch⁡)Gck+1cn1…⁡cnm.

Thus

(YSearch⁡)Gckcn1…⁡cnm≡βck

if g(k,n¯)=0 and

(YSearch⁡)Gckcn1…⁡cnm≡β(YSearch⁡)Gck+1c1…⁡cm

otherwise, as g is λ-defined by G. Hence

Fcn1…cnm≡β(YSearch⁡)Gc0cn1…⁡cnm≡βcf(n¯)

if f is defined on n¯. So F λ-defines f. □

Lemma 2.1.22. Every partial recursive function is λ-definable.

Definition 2.1.23 (Godel numbering). Let L be a first-order language. A Gödel numbering is an injection L↪ℕ that is:

  • (1)
    Computable (assuming some notion of computability for strings of symbols over a finite alphabet);
  • (2)
    Its image is a recursive subset of ℕ;
  • (3)
    Its inverse (where defined) is also computable.

Notation. We will use ⌈φ⌉ to be the Gödel numbering of an element of L, for some fixed choice of Gödel numbering.

One way: assign a unique number ns to each symbol s in your finite alphabet σ. We can then define

⌈s0…sk⌉:=∑i=0k(nsi+1).

Remark. We can also encode proofs: add a symbol # to the alphabet and code a proof with lines φ0,…,φk as ⌈φ0#φ1#⋯#φk⌉.

Theorem 2.1.24. Assuming that:

Proof (sketch). Assign Gödel numbers ⌈τ⌉ to λ-terms τ. We can then consider a partial recursive function in N(t) that on input t checks if t is the Gödel numbering of a λ-term τ, and returns the Gödel numbering of its β-normal form if it exists (undefined otherwise).

We also have partial recursive functions that convert n to ⌈cn⌉ and vice-versa. Finally, say f is a partial function defined by a λ-term F. We can compute f(m¯) by first converting Church numerals to their Gödel numbers, then append the result to ⌈F⌉ in order to get ⌈Fcn1…cnk⌉, then apply N.

If f is defined on n¯, then Fcn1…cnk has a β-normal form, and what we get is ⌈cf(n¯)⌉. Otherwise N(⌈Fcn1…cnk⌉) is not defined.

We finish by going back from ⌈cf(n¯)⌉ to f(n¯). □

2.2 Decidability in Logic

Recall that a subset X⊆ℕ is recursive (or decidable) if its characteristic map is total recursive.

Definition 2.2.1 (Recursively enumerable). We say that X⊆ℕ is recursively enumerable if any of the following are true:

Note, if X and ℕ∖X are both recursively enumerable, then X is recursive. Note that the set of partial recursive function is countable, so we can fix an enumeration {f0,f1,…}.

Example 2.2.2. The subset W={(i,x):fi is defined on x}⊆ℕ2 is recursively enumerable, but not recursive.

Definition 2.2.3 (Recursive / decidable language). A language L is recursive if there is an algorithm that decides whether a string of symbols is an L-formula.

An L-theory T is recursive if membership in T is decidable (for L-sentences).

An L-theory T is decidable if there is an algorithm for deciding whether T⊨φ.

We will work with recursive from now on.

Theorem 2.2.4 (Craig). Assuming that:

Then T admits a recursive axiomatisation.

Proof. By hypothesis, there is a total recursive f such that the axioms of T are exactly {f(n):n∈ℕ}.

Idea: Replace f(n) with something equivalent, but with a shape that lets us retrieve n. Let

ψn=∧k=1n(f(n))

for each n and

T∗:={ψn:n∈ℕ}.

Then T∗ has the same deductive closure as T. As formulae have finite length, we can check in finite time whether some χ is f(0) or some ∧⁡k=1nAn. By appropriate use of brackets, we can make sure that such an n is “unique” if we are working with some ψn.

In the first case, we halt and say we have a member of T∗. In the second case, we check if A=f(n), saying we have a member of T∗ if so, and that we don’t otherwise.

We can do this because we can scan the list {f(n):n<ω} and check symbol by symbol whether f(n) matches A, which takes finite time.

If the input is not of the right shape, we halt and decide that it is ∉T∗. □

Lemma 2.2.5. The set of (Gödel numberings for) total recursive functions is not recursively enumerable.

Proof. Suppose otherwise, so there is a total recursive function whose image is the set of Gödel numberings of total recursive functions.

So for any total recursive r, there is n such that ⌈f(n)⌉=r. Define g:ℕ→ℕ by g(n)=⌈f(n)⌉(n)+1. This is certainly total recursive, but can’t be the function coded by f(m) for any m, contradiction. □

Definition 2.2.6 (Language of arithmetic). The language of arithmetic is the first-order language LPA with signature (0,1,+,⋅,<). The base theory of arithmetic is the LPA-theory PA− whose axioms express that:

  • (1)
    + and ⋅ are commutative and associative, with identity elements 0 and 1 respectively;
  • (2)
    ⋅ distributes over +;
  • (3)
    < is a linear ordering compatible with + and ⋅;
  • (4)
    ∀⁡x.∀⁡y.(x<y→∃⁡z.x+z=y);
  • (5)
    0<1∧∀⁡x.(x>0→x≥1);
  • (6)
    ∀⁡x.x≥0.

The (first-order) theory of Peano arithmetic PA is obtained from PA− by adding the scheme of induction: for each LPA-formula φ(x,y¯), the axiom

Iφ:=∀⁡y¯.(φ(0,y¯)∧∀⁡x.(φ(x,y¯)→φ(x+1,y¯))→∀⁡x.φ(x,y¯)).

Definition 2.2.7 (Delta0-formula, Sigma1-formula). A Δ0-formula of PA is one whose quantifiers are bounded, i.e. ∃⁡x<t.φ(x) or ∀⁡x<t.φ(x), where t is not free in φ and φ is quantifier free.

We say φ(x¯) is a Σ1-formula if there is a Δ0-formula ψ(x¯,y¯) such that

PA⁡⊢φ(x¯)↔∃⁡y¯.ψ(x¯,y¯).

It is a Π1-formula if there is a Δ0-formula ψ(x¯,y¯) such that

PA⁡⊢φ(x¯)⟺∀⁡y¯.ψ(x¯,y¯).

In Example Sheet 4, you will prove that the characteristic function of a Δ0-definable set is partial recursive. We will show that the Σ1-definable sets are precisely the recursively enumerable ones.

Recall that defining ⟨x,y⟩=(x+y)(x+y+1)2+y yields a total recursive bijection ℕ2→ℕ.

Applying this a bunch of times, we get total recursive bijections ℕk→ℕ by ⟨v,w¯⟩=⟨v,⟨w¯⟩⟩.

This is not good, as we have a different function for each k. We’d like a “pairing function” that lets us see a number as a code for a sequence of any length.

This can be done within any model of PA by using a single function β(x,y) (known as Gödel’s β-function) which is definable in PA.

We want an arithmetic procedure that can associate a code to sequences of any length, and such that the entries of the sequence can be recovered from the code.

We will do this by a clever application of the Chinese Remainder Theorem.

Suppose given a sequence x0,x1,…,xn−1 of natural numbers. We want numbers m+1,2m+1,…,nm+1 to serve as moduli, with xi<(i+1)m+1, and all of which are pairwise coprime. If we can find m such that these conditions hold, then there is a number a such that a≡xi(mod(i+1)m+1).

Taking m=max⁡(n,x0,…⁡,xm−1)! works.

We say that the pair (a,m) codes the sequence.

Definition 2.2.8 (beta indexing). The function β:ℕ2→ℕ is defined by β(x,i)=a%(m(i+1)+1), where a and m are the unique numbers such that x=⟨a,m⟩.

Remark. The forumula β(x,y)=z is given in PA by a Δ0-formula. We will use the notation (x)i for β(x,i); thus the decoding property is that (x)i=xi if x=⟨a,m⟩ codes x0,…,xn−1.

Lemma 2.2.9 (Godel’s Lemma). Assuming that:

  • M⊨PA⁡

  • n∈ℕ

  • x0,…,xn−1∈M

Then there is u∈M such that M⊨(u)i=xi for all i<n.

Theorem 2.2.10. Assuming that:

  • f:ℕk→ℕ a partial function

Then f is recursive if and only if there is a Σ1-formula 𝜃(x¯,y) such that y=f(x¯)⟺ℕ⊨𝜃(x¯,y).

Proof.

Corollary 2.2.11. A subset A⊆ℕk is recursively enumerable if and only if there is a Σ1-formula ψ(x1,…,xk) such that, given x¯∈ℕk, we have x¯∈A if and only if ℕ⊨ψ(x).

Proof.

Any model of PA− includes a copy of ℕ inside of it: consider the standard natural numbers

n̲=SSS…⁡S⏟n0.

In fact, ℕ embeds in any model PA− as an initial segment: essentially because

PA−⊢∀⁡x.(x≤k̲→x=0̲∧x=1̲∧⋯∧x=k̲).

In Example Sheet 4, you will see that ℕ is a Δ0-elementary substructure of any model of PA−: every Δ0-sentence φ(n̲) true in ℕ is also true in the model.

Definition 2.2.12 (Representation of a total function). Let f:ℕk→ℕ be total and T be any LPA⁡-theory extending PA−. We say that f is represented in T if there is an LPA− formula 𝜃(x1,…,xk,y) such that, for all n¯∈ℕk:

  • (a)
    T⊢∃⁡!y.𝜃(n¯,y)
  • (b)
    If k=f(n¯), then T⊢𝜃(n¯,k̲)

Lemma 2.2.13. Every total recursive function f:ℕk→ℕ is Σ1-represented in PA−.

Proof. The graph of f is given by a Σ1-formula by Theorem 2.2.10, say ∃⁡z¯.φ(x¯,y,z¯) where φ∈Δ0. Without loss of generality, we may assume that z¯ is a single variable (for example, rewrite ∃⁡z.∃⁡w¯<z.φ(x¯,y,w¯)).

Let ψ(x¯,y,z) be the Δ0-formula

φ(x¯,y,z)∧∀⁡u,v≤y+z.(u+v<y+z→¬⁡φ(x¯,u,v)).

Then the Σ1-formula 𝜃(x¯,y):=∃⁡z.ψ(x¯,y,z) represents f in PA−.

We show PA−⊢𝜃(n¯,k) first, where k=f(n¯). Note that k is the unique element of ℕ such that ℕ⊨∃⁡z.φ(n¯,k,z), as f is a function.

Take l to be the first natural number such that ℕ⊨φ(n¯,k,l). Then ℕ⊨ψ(n¯,k,l) too, whence ℕ⊨∃⁡z.ψ(n¯,k,z). But any Σ1-sentence true in ℕ is true in any model of PA−(c.f. Example Sheet 4), so PA−⊢∃⁡z.ψ(n¯,k,z), i.e. PA−⊢𝜃(n¯,k).

To see that PA−⊢∃⁡!y.𝜃(n¯,y), let l be the first number such that ℕ⊨φ(n¯,k,l), where k=f(n¯). Suppose a,b∈M⊨PA−, with M⊨ψ(n¯,a,b). We will show that a=k. Completeness settles the claim. Again, φ(n¯,k,l) is a Δ0-sentence true in ℕ, thus true in M.

Using the fact that < is a linear ordering in M, we have a,b≤k+l∈ℕ, so a,b∈ℕ (as ℕ is an initial segment of M). Now M⊨ψ(n¯,a,b)∈Δ0, hence ℕ⊨ψ(x¯,a,b) and thus ℕ⊨∃⁡z.φ(n¯,a,z). Thus a=k as needed. □

Corollary 2.2.14. Every recursive set A⊆ℕk is Σ1-representable in PA−.

Proof. The characteristic function χA of A is total recursive, so χA(x¯)=y is represented by some Σ1-formula 𝜃(x¯,y) in PA−. But then 𝜃(x¯,1) represents A in PA−. □

Lemma 2.2.15 (Diagonalisation Lemma). Assuming that:

Then there is an LPA⁡-sentence G such that
T⊢G↔𝜃(⌈G⌉).

Moreover, if 𝜃 is a Π1-formula, then we can take G to be a Π1-sentence.

Proof. Define a total recursive function diag⁡ this way: on input n∈ℕ, check if n=⌈σ(x)⌉ is the Gödel numbering of some LPA⁡-formula σ(x). If so, return ⌈∀⁡y.(y=n̲→σ(y))⌉, else return 0.

As diag⁡ is total recursive, it is Σ1-represented in T by some δ(x,y). Consider the formula

ψ(x):=∀⁡z.(δ(x,z)→𝜃(z)).

Let n=⌈ψ(x)⌉ and G:=∀⁡y.(y=n̲→ψ(y)). This makes G the sentence whose Gödel numbering is diag⁡(⌈ψ(x)⌉). It is obvious that T⊢G↔ψ(n̲), so we know that

T⊢G↔∀⁡z.(δ(n̲,z)→𝜃(z)).(α)

Now δ(x,y) represents diag⁡ in T, and diag⁡(n)=⌈G⌉ by construction, hence

T⊢∀⁡z.(δ(n̲,z)↔z=⌈G⌉).(β)

Combining (α) and (β), we get T⊢G↔𝜃(⌈G⌉) as needed.

Finally, note that if 𝜃∈Π1, then both ψ and G are equal to a Π1-formula. □

Theorem 2.2.16 (Crude Incompleteness). Assuming that:

  • T be a recursive set of (Gödel numberings of) LPA⁡-sentences

  • T is consistent (never includes both φ and ¬⁡φ)

  • T contains all the Σ1 and Π1 sentences provable in PA−

Then there is a Π1-sentence τ such that τ∉T and ¬⁡τ∉T.

Proof. Let 𝜃(x) be a Σ1-formula that represents T in PA−, so that

x∈T⟺PA−⊢𝜃(x)andx∉T⟺PA−⊢¬⁡𝜃(x).

This exists since T is recursive. By the Diagonalisation Lemma, there is a Π1-sentence τ such that PA−⊢τ↔¬⁡𝜃(⌈τ⌉).

If ⌈τ⌉∈T, then PA−⊢𝜃(⌈τ⌉), and thus PA−⊢¬⁡τ. But then ⌈¬⁡τ⌉∈T (as ¬⁡τ∈Σ1 and PA− proves it).

If ⌈¬⁡τ⌉∈T, then τ∉T, so PA−⊢¬⁡𝜃(⌈τ⌉), and thus PA−⊢τ. As τ∈Π1 and PA−⊢τ, we have ⌈τ⌉∈T.

Since T is consistent, we can’t have either of ⌈τ⌉ or ⌈¬⁡τ⌉ in T. □

Corollary 2.2.17 (Godel-Rosser Theorem). Let T be a consistent LPA⁡-theory extending PA− and admitting a recursively enumerable axiomatisation. Then T is Π1-incomplete: there is a Π1-sentence τ such that T⁄⊢τ and T⁄⊢¬⁡τ.

Proof. By Craig’s Theorem, we may assume that T is recursive. Suppose that T is Π1-complete, and consider the set S of (Gödel numberings of) all the Σ1 and Π1 sentences in LPA⁡ that T proves.

The set S is recursive: we can effectively decide if a given sentence is Σ1 or Π1, then check if ⌈σ⌉∈S by systematically searching through all proofs using the axioms in T, until we either find a proof of σ or a proof of ¬⁡σ. Since T is Π1-complete, there is always such a proof, and we’ll find it in finite time.

But then S satisfies the hypotheses of Theorem 2.2.16, so there is a Π1-sentence τ with ⌈τ⌉∉S and ⌈¬⁡τ⌉∉S, contradicting Π1-completeness of T. □

Definition 2.2.18 (Recursive structure). A (countable) LPA⁡-structure M is recursive if there are total recursive functions ⊕:ℕ2→ℕ, ⊗:ℕ2→ℕ, a binary recursive relation ≼⊆ℕ2, and natural numbers n0,n1∈ℕ such that M≅(ℕ,⊕,⊗,≼,n0,n1) as LPA⁡-structures.

We will show that the usual ℕ is the only recursive model of PA⁡ (up to ≅).

Strategy:

Note that there is a Σ1-formula pr⁡(x,y) that captures y being the x-th prime, and PA⁡⊢∀⁡x.∃⁡!y.pr⁡(x,y). So if ℕ thinks that k is the n-th prime, then any model of PA⁡ thinks so too. Write πn for the n-th prime.

Lemma 2.2.19 (Overspill). Assuming that:

  • M a non-standard model of PA⁡

  • φ(x) an LPA⁡-formula

  • M⊨φ(n) for all standard natural numbers n

Then there is a nonstandard natural number e such that M⊨φ(e).

Proof. Say M⊨φ(n) for all standard n, but only them. Then M⊨φ(0) and M⊨∀⁡n.(φ(n)→φ(n+1)) holds (if φ(n) holds, then n and hence n+1 are standard).

By Iφ (induction), we conclude that M⊨∀⁡n.φ(n). But M is non-standard, so there is non-standard e∈M with φ(e), contradiction. □

Fix some m∈ℕ, and a property φ(x) of the natural numbers.

Definition 2.2.20 (Canonically coded). A subset S⊆ℕ is canonically coded in a model M of PA⁡ if there is c∈M such that

S={n∈ℕ:∃⁡y.(πn̲×y=c)}

where n̲ denotes the standard number n in the model.

We could use other formulas to code subsets. Th subsets of ℕ coded in M are those S⊆ℕ for which there is a PA⁡-formula φ(x,y) and c∈M such that S={n∈ℕ:M⊨φ(n̲,c)}.

As it turns out, coding via Σ1-formulae gives nothing new:

Proposition 2.2.21. Assuming that:

  • C(u,x) be a Δ0-formula

  • M a non-standard model of PA⁡

Then given any b~∈M, there is c∈M such that, for any n∈ℕ:
M⊨∃⁡k<b~.C(k,n)↔∃⁡y.(πn̲×y)=c.

Proof (sketch*). The following formula holds in ℕ for any n:

∀⁡b.∃⁡a.∀⁡u<n.(∃⁡k<b.C(k,u)↔∃⁡y.(πu×y)=a).

This is by the reasoning we gave when introducing codes, which works due to the bound on k and u. This can be proved in PA⁡*.

Thus

M⊨∀⁡b.∃⁡a.∀⁡u<n̲.(∃⁡k<b.C(k,u)↔∃⁡y.(πu×y=a))

for any n∈ℕ. So by Lemma 2.2.19 there is a non-standard w∈M such that

M⊨∀⁡b.∀⁡a.∀⁡u<w.(∃⁡k<b.C(k,u)↔∃⁡y.(πu×y=a)).

So for any b~∈M, there must be c∈M such that

M⊨∀⁡u<w.(∃⁡k<b~.C(k,u)↔∃⁡y.(πu×y=c)).

Now w is non-standard, so M⊨n̲<w for all n∈ℕ. So for any b~∈M there is c∈M with

M⊨∃⁡k<b~.C(k,n)↔∃⁡y.(πn̲×y=c)

for all n∈ℕ. □

Definition 2.2.22 (Recursively inseparable). We say that subsets A,B⊂ℕ are recursively inseparable if they are disjoint and there is no recursive C⊆ℕ with B∩C=∅ and A⊆C.

Proposition 2.2.23. There are recursively enumerable subsets A,B⊆ℕ that are recursively inseparable.

Proof. Fix an effective enumeration {φn:n<ω} of the partial recursive functions. Define A={n∈ℕ:φn(n)=0} and B={n∈ℕ:φn(n)=1}, which are clearly disjoint and are clearly recursively enumerable.

Suppose there is a recursive C with A⊆C and B∩C=∅, and write χC for its (total recursive) characteristic function. There must be u∈ℕ such that χC=φu, as χC is total recursive.

Since χC(u)↓ and is either 0 or 1, we have either u∈A or u∈B.

If u∈A, then χC(u)=φu(u)=0, so u∉C, contradicting A⊆C; so u∈B. But then χC(u)=φu(u)=1, so u∈C, contradicting B∩C=∅. Thus A and B are recursively inseparable. □

Lemma 2.2.24. Assuming that:

  • M⊨PA⁡ non-standard

Then there is a non-recursive set S which is canonically coded in M.

Proof. Say A,B⊆ℕ are recursively enumerable and recursively inseparable. By Corollary 2.2.11, there are Σ1-formulae ∃⁡u.a(u,x) and ∃⁡u.b(u,x) defining A and B respectively (so a and b are Δ0-formulae).

Fix n∈ℕ. As the sets are disjoint, we have:

ℕ⊨∀⁡v<n.∀⁡w<n.∀⁡x<n.¬⁡(a(v,x)∧b(w,x)).

As this sentence is Δ0, it follows, for any non-standard M⊨PA⁡ and n̲∈M that:

M⊨∀⁡v<n̲.∀⁡w<n̲.∀⁡x<n̲.¬⁡(a(v,x)∧b(w,x)).

By Overspill, there is some non-standard c∈M such that

M⊨∀⁡v<c.∀⁡w<c.∀⁡x<x.¬⁡(a(v,x)∧b(w,x)).(∗)

Now define X:={n∈ℕ:∃⁡v<c.a(v,n̲)}. Note that:

As A and B are recursively inseparable, X can’t be recursive. This shows that M must encode a non-recursive set, which implies that it must canonically encode a non-recursive set by Proposition 2.2.21. □

Theorem 2.2.25 (Tennenbaum). Assuming that:

  • M=(M,⊕,⊗,≼,n0,n1) a countable non-standard model of PA⁡

Then ⊕ is not recursive.

Proof. As M is countable, we may as well assume that M=ℕ, n0=0, n1=1.

By Lemma 2.2.24, there is some c∈M that canonically codes a non-recursive subset X={n:M⊨∃⁡y.(πn̲×y=c)}⊆ℕ.

As PA⁡ proves that

πn̲×x=x+⋯+x⏟πn times,

we have that

πn̲×y=y+⋯+y⏟πn times

for all y∈M. So n∈X if and only if there is d∈M such that

c=d⊕⋯⊕d⏟πn times.

Suppose ⊕ is recursive. Then we can can through ℕ (which is M) and look for some d∈M that realises the disjunction of:

{c=x⊕⋯⊕x⏟πn x’sc=x⊕⋯⊕x⏟πn x’s⊕1⋯c=x⊕⋯⊕x⏟πn x’s⊕1⊕⋯⊕1⏟πn−1 ones

As ⊕ is recursive, we can decide whether the disjunction holds of a given d. Moreover, the search for such d always terminates:

Combining these, we get that division of c by πn̲ in M leaves a unique quotient d∈M, and remainder r≼πn̲, which is either 0 or 1 or 1⊕1 or …or 1⊕1⊕⋯⊕1 (πn−1 times); i.e. one of the disjunctions from before.

Now we see that X is recursive: if our search provides d such that

M⊨c=d⊕⋯⊕d⏟πn times,

then n∈X, and if the search gives d satisfying one of the other disjunctions, then n∉X.

This contradicts the choice of X, so ⊕ can’t be recursive. □

˙