Category Archives: Logic

Non-standard Models of Arithmetic 2

JB: The only books I know on models of Peano arithmetic are Kaye’s Models of Peano Arithmetic and Kossack and Schmerl’s more demanding The Structure of Models of Peano Arithmetic, and I’m trying to read both. But I have a certain dream which is being aided and abetted by this paper:

• Ali Enayat, Standard Models of Arithmetic.

Roughly, my dream is to show that “the” standard model is a much more nebulous notion than many seem to believe.

One first hint of this is the simple fact that for any sentence that’s not decidable in Peano Arithmetic, there are models where this sentence is satisfied and models where it’s not. In which camp does the standard model lie? We can only say: “one or the other”. And the same is true in any recursively enumerable consistent extension of PA. There are always undecidable sentences in any such extension, and there are always models—infinitely many, in fact—where the sentence is satisfied, and infinitely many where it is not!

So, choosing “the” standard model among all the pretenders—or even this lesser task: finding it up to elementary equivalence—is a herculean task, like finding ones way through an infinite labyrinth of branching paths, where at each branch deciding which way to go requires brand-new insights into mathematics, not captured by our existing axioms. I’m not convinced it makes sense to talk about the “right” decision in every case.

Another hint is the Overspill Lemma, used ubiquitously in the study of nonstandard models. Roughly:

Overspill Lemma: In a nonstandard model of Peano arithmetic, any predicate in the language of arithmetic that holds for infinitely many standard natural numbers also holds for infinitely many nonstandard ones.

Corollary: There is no way to write down a predicate in the language of arithmetic that singles out the standard natural numbers.

So, if our supposed “standard” model were actually nonstandard, we still couldn’t pick out the nonstandard numbers. The aliens could be among us, and we’d never know!

But you know all this stuff, and probably have different interpretations of what it means. I don’t mainly want to argue about that; I mainly want to learn more, so I can prove some interesting theorems.

So, thanks for your great introduction! I especially love the idea of types, which I just learned. Your explanation was great. Here’s more, in case anyone is reading:

Types (model theory), Wikipedia.

You didn’t quite get to “recursively saturated models”, so I pestered Joel David Hamkins (a logician I know, now at Oxford) and got this nice explanation, which fits nicely with yours:

Dear John,

Saturation is about realizing types. The type of an element a in a model M is the set of all formulas \varphi(x) such that M satisfies \varphi(a). You can allow parameters in a type. For example, if you consider the reals as an ordered field, then any two elements a and b have different types, since there is some rational p/q between them, and a, say, will realize the formula a<p/q, while b does not. This formula x<p/q is expressible in the language of fields.

Does \mathbb{R} realize all types that it could? No, because you can write down a collection of formulas \varphi_n(x) asserting that 0<x and x<1/n. This is expressible in that language, and it is consistent with the diagram of the reals, meaning that this type could be realized in some elementary extension of \mathbb{R}. The type asserts that x is a positive infinitesimal number. So the reals are not saturated.

Indeed, since that type was very easy to describe, the reals are not even recursively saturated (I usually call it computably saturated). To be recursively saturated, a model M must realize every computable type (the formulas, as a set, are a computable set of formulas) that is consistent with its diagram.

In general, saturated models are very thick—they have lots of points of all the types that one could in principle have in a model of that theory. Usually, countable models are not saturated (except when the language is trivial in some way).  To get around this, the idea of recursive saturation works very well with countable models, and this is what is going on in Kaye’s book.

Hope this helps, and let me know if I can explain anything more about it…

Kind regards,


It’s so much easier to learn stuff by talking with people than by fighting through a thicket of logic symbols! But it’s also good for me to keep reading the books.

Leave a comment

Filed under Conversations, Peano arithmetic

Non-standard Models of Arithmetic 1

This is the first in a series of posts, recording an e-conversation between John Baez (JB) and me (MW).

JB: I’ve lately been trying to learn about nonstandard models of Peano arithmetic. Do you know what a “recursively saturated” model is? They’re supposed to be important but I don’t get the idea yet.

MW: What books and/or papers are you reading? I used to know this stuff, indeed my thesis (1980) was on existentially complete models of arithmetic. When I looked at it a couple of years ago, I was amazed at how much I’d forgotten. Talk about depressing.

Anyway, I’ll toss out a few vague ideas, to see if they help. Maybe this will be the push I need to get back to Kaye’s book, or even Kossak & Schmerl. I picked them up a few months ago, hoping to revisit my youth, but I didn’t make it past the prefaces.

As Hodges puts it, model theory is “algebraic geometry minus fields”. If you have an algebraic number r in a extension field K/F, it’s natural to look at all the polynomials in F[x] which have r as a root. It turns out that this is a principal ideal, generated by the minimal polynomial.

Sort-of generalize to an arbitrary model M of a theory T. Let (r_1,\ldots,r_n) be an n-tuple of elements of M. Look at the set of all formulas \varphi(x_1,\ldots,x_n) such that M satisfies \varphi(x_1,\ldots,x_n). This is the complete n-type of (r_1,\ldots,r_n) with respect to M.

Unlike the case in field theory, complete n-types are not usually implied (“generated”) by a single formula, but when they are, they are called principal.

Next step is to free the notion of n-type from dependence on the model M. If we have a set of formulas \Phi=\{\varphi(x_1,\ldots,x_n)\} that is consistent with T, then it’s an n-type. (Sort of like a polynomial in F[x], looking for a root.) The type is realized in a model M if there is a n-tuple (r_1,\ldots,r_n) such that M satisfies all the \varphi(x_1,\ldots,x_n). It’s omitted if there is no such n-tuple in M.

The omitting types theorem says that any countable collection of non-principal n-types in a countable language can all be omitted by some model of T.

You can imagine that n-types tell us a lot about possible isomorphisms and automorphisms of models. The poster child: the theory DLO of dense linear orderings without endpoints. This is because there are essentially only very simple types. Pretty much the only thing you can say about (r_1,\ldots,r_n) is what permutation of the subscripts puts them in monotonically increasing order, and for which subscripts i and j we have ri=rj. Anything else about the n-tuple is implied by this. Especially significant is that no quantifiers need apply.

And of course, any two countable DLOs are isomorphic, and there are lots of automorphisms of a countable DLO. If you look at the back-and-forth argument, you’ll see it relies on the limited repetoire of types.

Also, to hammer the analogy with field theory, the polynomials r satisfies tells us all about the isomorphisms and automorphisms.

OK, now specialize to PA. Key thing here is the overspill lemma. This allows you to code info about subsets of the standard \mathbb{N} into single elements of a non-standard M. For example, the set of standard prime divisors of a non-standard r in M.

If the set you want to code is totally arbitrary, well, you can’t even express it in the language of PA, so we want to look at sets that are definable by a formula. Then we can apply the overspill lemma. Say φ(x) is the formula for the set. Consider the formula \psi(y)\equiv(\exists z)(\forall x<y)[\varphi(x)\leftrightarrow p_x|z]. Here px is the x-th prime. Since ψ(n) holds for arbitrarily large finite n‘s (indeed all finite n‘s), overspill says that it also holds for some non-standard n. So there is a z such that φ(x) is true iff px|z, for all x<n. In particular it holds for all finite x, and so z codes the set via its prime divisors.

More generally, it would be nice to look at sets of n-tuples defined by an n-type. But we need some way to describe the n-type in the language of PA—we can’t describe an arbitrary set of formulas in the language of PA. So we look at recursive n-types, i.e., sets of formulas whose Gödel’s numbers form a recursive set.

If we’re lucky, we’ll be able to import a lot of classical model theory, developed in ZF (or even naive set theory) into PA, because we can code it all in PA. And this approach will help us understand things like extensions of one model by another, automorphisms, etc.

A couple more notes. First, the prenex normal form hierarchy shows up all the time in logic. A variant especially adapted to PA (the arithmetic hierarchy) is to let \Delta_0 formulas allow arbitrary bounded quantifiers, like (\forall x<y). It turns out that a relation is recursively enumerable iff it is \Sigma_1. So that’s a nice bridge between the model theory of PA and computability theory.

It also turns out that, because of the MRDP theorem, you don’t even need to allow bounded quantifiers at the ground level. Well, that’s a bit sloppy. What I mean is that \Sigma_1 is the same as \exists_1, formulas you get from putting a string of existential quantifiers in front of a quantifier-free formula.

Leave a comment

Filed under Conversations, Peano arithmetic

The Lambda-Calculus and the Plotkin/Scott Model

I won’t define the (untyped) λ-calculus; you have the rest of the internet for that. But the basic formalism is remarkably simple. Instead of writing x\mapsto 2\cdot x, for example, we write λx.(2·x). The λ-term ( λx.(2·x))7 stands for the application of the doubling function to 7, and we say that ( λx.(2·x))7 reduces to 2·7=14. (This is called β-reduction or β-conversion.)

The λ-calculus gleefully flouts the notion that a function can’t be its own argument. For example, the identity function I is defined by λx.x, and II reduces to I. Try it: II written out is (λx.x)(λx.x). To β-reduce this, you take the right hand copy of  (λx.x) and use it to replace the x in the left hand copy. (Maybe it’s easier if we rewrite II as (λx.x)I. This β-reduces to I.)

For my money, this is one of the most charming features of the λ-calculus. Of course, it does make it hard to model the  λ-calculus via those earth-bound functions of conventional set theory. For the first few decades of its history, the untyped λ-calculus remained a computational formalism.

A λ-term is reduced if it can’t be reduced any further. So λx.x is reduced but (λx.x)(λx.x) isn’t. Not all λ-terms can be (fully) reduced. The self-application term provides the standard example: D = λx.xx. Now, D itself is reduced, but if we try to reduce DD, we end up in an infinite loop.

There is one natural model of the λ-calculus. Regard λ-terms as programs and not as functions. (Well of course!) Let Λ be the totality of all reduced λ-terms. With any reduced λ-term T, we associate the partial function from Λ to Λ that takes a reduced term W to the reduction of TW—that is, if it has a reduction. So you get a partial function.

It doesn’t seem like you could model the λ-calculus with total functions, but in the 1970s Dana Scott and Gordon Plotkin discovered (independently) that you can.  I gave a seminar on a preprint by Scott. I recently latexed up my old hand-written notes; here’s the result.

I should say a word or two about the typed λ-calculus—everything above refers to the untyped calculus. Self-application is fun in some contexts, and sometimes very useful, but other times it’s a nightmare. To a computer scientist, having just one type for everything is the 9th circle of hell. After Scott came up with his model, he scaffolded up a whole theory of types based on these ideas. All very significant in theoretical computer science, but just a little too humdrum for my taste.




Filed under Logic