**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 Σ

_{1}formula φ(

*x*) that represents

*W*, in this sense:

_{e}*n*belongs to

*W*iff PA proves φ(

_{e}*n*). What if

*W*is recursive? Is there a Σ

_{e}_{1}formula φ(

*x*) that represents

*W*in the sense that if

_{e}*n*belongs to

*W*then PA proves φ(

_{e}*n*),

*and*if

*n*does

*not*belong to

*W*, then PA proves ¬φ(

_{e}*n*)?

There is indeed, but it takes the Rosser trick to get it. Say *W _{f}* is the complement of

*W*. So we have a Σ

_{e}_{1}formula representing

*W*, and a Σ

_{e}_{1}formula representing

*W*. The φ(

_{f}*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*. The formula ζ(

_{f}*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!

Pingback: Nonstandard Models of Arithmetic | Azimuth

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.)