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 \mathbb{N}^M for the ω of M equipped with addition and multiplication, defined in the usual way as operations on finite ordinals. So \mathbb{N}^M is what he calls a T-standard model of PA.

If φ is a formula in the language of arithmetic, L(PA), then \varphi^\mathbb{N} 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 \varphi^\mathbb{N}. But (minor whiplash!) \text{Con}(T+\varphi^\mathbb{N}) 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 PAT 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 \varphi^\mathbb{N}. But that’s really just a grace note.

So we could list PAT by setting a program churning away, generating all the theorems of T, and harvesting the ones of the form \varphi^\mathbb{N}. Therefore PAT 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 \varphi^\mathbb{N} after it’s been running for 1000 steps, it prints \varphi^\mathbb{N}\wedge\ldots\wedge\varphi^\mathbb{N} instead, with 1000 repetitions of \varphi^\mathbb{N}. This garrulous version of PAT has exactly the same theorems as the laconic one. But if you ask “Does this statement belong to PAT?”, well, we know when to stop waiting for it to show up in the output. So PAT 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 PAT. 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 PAT is recursive: we can write a program that decides whethers formulas are in PAT 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 Xre with a recursive theory Xrec 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 \mathbb{N} via non-standard numbers? (For example, using the set of prime divisors.) Kaye shows in Lemma 11.1 that any recursive subset of \mathbb{N} is coded in all nonstandard models of PA, but in Lemma 11.2 he shows that any nonrecursive subset of \mathbb{N} 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 We is an r.e. set, then there’s a Σ1 formula φ(x) that represents We, in this sense: n belongs to We iff PA proves φ(n). What if We is recursive? Is there a Σ1 formula φ(x) that represents We in the sense that if n belongs to We then PA proves φ(n), and if n does not belong to We, then PA proves ¬φ(n)?

There is indeed, but it takes the Rosser trick to get it. Say Wf is the complement of We. So we have a Σ1 formula \exists t\zeta(x,t) representing We, and a Σ1 formula \exists t\eta(x,t) representing Wf. The φ(x) we want is

\exists t[\zeta(x,t)\wedge(\forall s\!<\!t)\neg\eta(x,s)]

Intuitively, we have a program spitting out elements of We, and another program spitting out elements of its complement Wf. 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


Filed under Conversations, Peano Arithmetic

2 responses to “Non-standard Models of Arithmetic 11

  1. Pingback: Nonstandard Models of Arithmetic | Azimuth

  2. Not that it matters, but if the “inefficiency” in Craig’s Trick bothers you, instead of emitting the conjunction of n copies of phi, I think you could emit “n = n and phi”. What matters is only that n is encoded somehow into the modified form of the axiom.

    On the one hand, this is not going to make the axiom lengths “small”, since not only n but log n might in general grow without bound compared to |phi|. On the other hand, once n gets large, they will at least be only O(log n) in length rather than O(n) or worse! So it makes an exponential difference in their size. (Not that anyone will care either way, in any application of this that I can guess.)

    (As usual — please correct me if I’m wrong about any of this.)

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.