Non-standard Models of Arithmetic 11

Prev TOC Next

MW: Time to start on Enayat’s paper in earnest. First let’s review his notation. M is a model of T, a recursively axiomatizable extension of ZF. He writes for the ω of M equipped with addition and multiplication, defined in the usual way as operations on finite ordinals. So is what he calls a T-standard model of PA.

If φ is a formula in the language of arithmetic, L(PA), then is the corresponding statement in the language of set theory, L(ZF). This is a pretty common dodge in model theory: in ZF, we’re interpreting the formulas of L(PA) as really saying things about certain rather odd-looking sets, like {Ø,{Ø},{Ø,{Ø}}} (i.e., von Neumann’s 3). So φ has to be translated into L(ZF), resulting in . But (minor whiplash!) is a formula in L(PA) again. That’s because it’s an assertion about formulas, and all this syntactical stuff gets coded in the language of arithmetic, à la Gödel.

Enayat defines PA^T to be all the closed formulas of L(PA) that hold in all T-standard models. This is a semantic definition, but Gödel’s completeness theorem tells us that the statements true in all models of a theory are precisely those you can prove with the theory. Now, that’s not quite the story of Remark 2—we’re not talking about all statements you can prove with T, just those of the form . But that’s really just a grace note.

So we could list PA^T by setting a program churning away, generating all the theorems of T, and harvesting the ones of the form . Therefore PA^T is recursively enumerable. Enayat invokes Craig’s trick to make it recursive. Here’s how that works. Modify the program so that as time goes by, it spits out longer and longer statements.

For example, if it finds after it’s been running for 1000 steps, it prints instead, with 1000 repetitions of . This garrulous version of PA^T has exactly the same theorems as the laconic one. But if you ask “Does this statement belong to PA^T?”, well, we know when to stop waiting for it to show up in the output. So PA^T is a recursive set of (Gödel numbers of) formulas.

JB: Whoa—wait a minute. You’re taking formulas in the language of arithmetic and translating into the language of set theory, by treating natural numbers as finite ordinals. I get that. Then you’re seeing which of those formulas—or least the ‘closed’ formulas, with no free variables—you can prove using some theory T that extends ZF. These closed formulas form the set you’re calling PA^T. It seems obvious that this set is recursively enumerable: you just write a program to crank out proofs using the axioms of T (which are themselves recursively enumerable, by assumption).

But now you seem to be telling me that PA^T is recursive: we can write a program that decides whethers formulas are in PA^T or not. I thought that would violate the undecidability of arithmetic! More precisely, I thought that for any consistent recursively axiomatizable extension X of PA, it’s impossible to write a program to decide which closed formulas are theorems of X.

For example, if you just start going through all possible proofs, there’s no recursive function that says “if you’ve waited this long for a proof of this formula to show up, and it still hasn’t, you can give up”.

Now you’re not exactly claiming to do that, but it seems darn close. So I don’t get what’s going on.

MW: Ah, that’s the cleverness of Craig’s trick! Plus another example of me writing nearly what I should have said, instead of something precise, correct, and readable. Second try.

I wrote, “Enayat invokes Craig’s trick to make it recursive.” Scratch that, and replace it with, “Enayat invokes Craig’s trick, which replaces a recursively enumerable theory X_re with a recursive theory X_rec that has exactly the same theorems.”

JB: Oh, I get it! If you take all the theorems of some interesting theory of arithmetic and turn them axioms, they won’t be recursive, just recursively enumerable (if the original axioms were). But by replacing each theorem by a clearly equivalent but longer theorem, whose length grows with how long it took you to find a proof, you’ll get an equivalent set of theorems that’s recursive, since you “know when to quit” when trying to decide if a given closed formula is in this set.

Tricky guy, that Craig! As the old song goes

If you’re gonna play the game, boy
You gotta learn to play it right
You’ve got to know when to hold ’em
Know when to fold ’em
Know when to walk away
And know when to run.

But I’m a follower of Lawvere’s ideas on “theories”, so to me the particular choice of axioms is less important than the whole set of theorems: that’s what we call the theory. You can’t make that recursive for most interesting theories of arithmetic… so I’m wondering what’s the actual use of Craig’s trick. How is having a recursive set of axioms better than a merely r.e. set of axioms?

MW: Good model-theoretic instincts. Much of the time, model theorists care more about the class of all models of a theory rather than its particular axioms. When that’s the case, we might as well work with the deductive closure of the theory.

(Though the language of the theory—specifically, its signature—matters. As Hodges says in his Shorter Model Theory,

A healthy general principle is that, other things being equal, signatures should be chosen so that the notions of homomorphism and substructure agree with the usual notions for the relevant branch of mathematics.

End parenthetical comment.)

Except… Remember coding subsets of via non-standard numbers? (For example, using the set of prime divisors.) Kaye shows in Lemma 11.1 that any recursive subset of is coded in all nonstandard models of PA, but in Lemma 11.2 he shows that any nonrecursive subset of fails to be coded in at least one nonstandard model.

Now, types are just theories, from one viewpoint. Recursively saturated models realize all their recursive types. In the second half of Kaye’s book, a lot of traffic goes on between types, coded subsets, and notions of truth. Kaye uses Craig’s trick to show that “recursively saturated” could have been defined equivalently using “r.e. type” instead of “recursive type” (p.150). I can’t say off-hand how the development would have gone without Craig’s lemma—if it’s just a “nice-to-have”, or if the equivalence steps in at some critical juncture.

As long as we’re here, let me mention Rosser’s trick. You know how Gödel formalized the sentence “I am unprovable” in PA, and how that sentence isn’t provable unless PA is inconsistent. Now, that doesn’t quite demonstrate that PA is either inconsistent or incomplete; conceivably, you could prove the negation of the Gödel sentence even in a consistent PA! (You’d have proven the existence of a proof of the Gödel sentence, even though there wasn’t one. So PA lied, but consistently.) Five years after Gödel’s 1931 paper, Rosser came up with a sentence that (roughly speaking) says:

If I am provable, then my negation has a shorter proof.

And you can show that if the Rosser sentence or its negation is provable in PA, then PA is inconsistent.

You can view the Rosser trick from a more natural perspective. If W_e is an r.e. set, then there’s a Σ₁ formula φ(x) that represents W_e, in this sense: n belongs to W_e iff PA proves φ(n). What if W_e is recursive? Is there a Σ₁ formula φ(x) that represents W_e in the sense that if n belongs to W_e then PA proves φ(n), and if n does not belong to W_e, then PA proves ¬φ(n)?

There is indeed, but it takes the Rosser trick to get it. Say W_f is the complement of W_e. So we have a Σ₁ formula representing W_e, and a Σ₁ formula representing W_f. The φ(x) we want is

Intuitively, we have a program spitting out elements of W_e, and another program spitting out elements of its complement W_f. The formula ζ(x,t) formalizes “x shows up in the output of the first program at time t”, likewise η(x,s) formalizes “x shows up in the output of the second program at time s”. To determine if x belongs to the recursive set or not, we just wait to see where it shows up first.

For me, Rosser’s trick and Craig’s trick have a similar tang. On the one hand, the distinction between recursive and recursively enumerable is the cornerstone of computability theory. On the other hand, lots of subtleties attend that divide.

JB: Wow, this really provides a lot to think about. I’m glad I spoke up. But I’ll ponder this on my own later. Let’s get back to the main story line. What does Enayat do next?

MW: Stay tuned!

Prev TOC Next