Category Archives: Peano arithmetic

Prev TOC

MW: Recap: we showed that PA^T implies Φ_T, where Φ_T is the set of all formulas

Now we have to show the converse, that PA+Φ_T  implies PA^T. But first let’s wave our hands, hopefully shaking off some intuition, like a dog shaking off water.

Below is a diagrammatic description of PA^T. The outer rectangle contains all models of PA, the inner oval contains all those that are (isomorphic to) ω’s of models of T. In other words, all models of PA^T. Now let’s say φ is a sentence that cannot be proved using only PA, but can be proved from T. So for T=ZF, φ could be the Paris-Harrington principle, or Goodstein’s theorem, or Con(PA). The blue region represents all the models where φ holds. So it includes the oval, but not all of the rectangle. The oval is the intersection of all such blue regions, as φ ranges over all of PA^T. If φ were provable from PA, then it would paint the entire rectangle blue.

Next I want to take a second look at Φ_T. I’m going to turn its formulas inside-out and upside-down. Start with

The contrapositive is

Basic results from proposition logic tells us that for any sentence φ and any theory T, ¬Con(T+φ) is equivalent to T⊢¬φ. (“Proof by contradiction”.) So we have

Since φ ranges over all sentences of the language of PA, we might as well replace ¬φ with φ. Upshot: Φ_T is equivalent to

Let me explain the quote marks. Provability is a syntactic property, an assertion about strings of symbols. Or maybe I should say strings of strings of symbols. We can code syntactic claims into PA; the quoted stuff stands for the formalization of that claim into the language of PA. Kind of like the corner brackets for Gödel numbers, but more general.

The sentences of Φ_T say “Trust T.” In other words, “If T proves it, then it’s true.”

Let’s take a second look at the implication . We want to show that the formula “paints the oval blue”, i.e., holds in all models of T. Well, if , then “it stands to reason” that φ should hold in the of a model of T. That’s the intuition, at least.

As before, some subtleties lurk, but not enough to derail the conclusion. We must interpret the assumption “” inside the model . The proof of could have non-standard length! The trick is to bring the whole intuitive argument inside the model of T, which we can do thanks to the items mentioned last time: the Reflection Principle of ZF, and the existence of a formal truth predicate for formulas with up to d quantifiers (for any given d).

The reverse implication, , takes less work, though there is one fine point. Suppose T yields . Then some finite fragment does, say

.

In fact (this is the fine point),

.

Why? Well, if T_n proves something, then PA can prove that it proves it. People often argue (correctly) that if the Goldbach conjecture is false, then it’s provably false in PA: if we have a counterexample, we can check that it is a counterexample with a finite calculation, which we can code into PA. The same holds for . Technically this is known as the Σ₁-completeness of PA. Both “T_n proves φ” and “the Goldbach conjecture is false” are Σ₁ statements, unlike “there are infinitely many prime pairs”, which is Π₂. It’s quite conceivable that the prime pair conjecture could go either way without PA having a proof.

As we saw earlier, Φ_T is equivalent to the collection of all statements of this form:

.

So in PA+Φ_T, we can prove both and , for any φ in PA^T. Modus ponens takes it from there!

Prev TOC Next

Prev TOC

MW: OK, back to the main plotline. Enayat asks for a “natural” axiomatization of PA^T. Personally, I don’t find PA^T all that “unnatural”, but he needs this for Theorem 7. (It’s been a while, so remember that Enayat’s T is a recursively axiomatizable extension of ZF.)

Continue reading →

Prev TOC Next

JB: It’s been a long time since Part 11, so let me remind myself what we’re talking about in Enayat’s paper Standard models of arithmetic.

We’ve got a theory T that’s a recursively axiomatizable extension of ZF. We can define the ‘standard model’ of PA in any model of T, and we call this a ‘T-standard model’ of PA. Then, we let PA^T to be all the closed formulas in the language of Peano arithmetic that hold in all T-standard models.

This is what Enayat wants to study: the stuff about arithmetic that’s true in all T-standard models of the natural numbers. So what does he do first?

Continue reading →

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.

Continue reading →

Prev TOC Next

JB: So, last time you sketched the proof of the Paris–Harrington theorem. Your description is packed with interesting ideas, which will take me a long time to absorb. Someday I should ask some questions about them. But for now I’d like to revert to an earlier theme: how questions about the universe of sets cast their shadows down on the world of Peano arithmetic.

Continue reading →

Prev TOC Next

MW: Time to talk about the Paris-Harrington theorem. Originally I thought I’d give a “broad strokes” proof, but then I remembered what you once wrote: keep it fun, not a textbook. Anyway, Katz and Reimann do a nice job for someone who wants to dive into the details, without signing up for a full-bore grad course in model theory. So I’ll say a bit about the “cast of characters” (i.e., central ideas), and why I think they merit our attention.

Continue reading →

Prev TOC Next

JB: So, you were going to tell me a bit how questions about the universe of sets cast their shadows down on the world of Peano arithmetic.

MW: Yup. There are few ways to approach this. Mainly I want to get to the Paris-Harrington theorem, which Enayat name-checks.

First though I should do some table setting of my own. There’s a really succinct way to compare ZF with PA: PA = ZF − infinity!

Continue reading →