Category Archives: Logic

Non-standard Models of Arithmetic 14

Prev TOC

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


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

Below is a diagrammatic description of PAT. 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 PAT. 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 PAT. 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

\{\text{``}T_n\vdash\varphi^\mathbb{N}\text{''}\rightarrow\varphi : \varphi\in\text{L(PA)},n\in\omega\}

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 \text{PA}^T\Rightarrow  \text{PA}+\Phi_T. We want to show that the formula \text{``}T_n\vdash\varphi^\mathbb{N}\text{''}\rightarrow\varphi “paints the oval blue”, i.e., holds in all models of T. Well, if T_n\vdash\varphi^\mathbb{N}, then “it stands to reason” that φ should hold in the \mathbb{N} 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 “T_n\vdash\varphi^\mathbb{N}inside the model \mathbb{N}. The proof of \varphi^\mathbb{N} 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, \text{PA}+\Phi_T\Rightarrow\text{PA}^T, takes less work, though there is one fine point. Suppose T yields \varphi^\mathbb{N}. Then some finite fragment does, say


In fact (this is the fine point),


Why? Well, if Tn 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 T_n\vdash\varphi^\mathbb{N}. Technically this is known as the Σ1-completeness of PA. Both “Tn proves φ” and “the Goldbach conjecture is false” are Σ1 statements, unlike “there are infinitely many prime pairs”, which is Π2. 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 \text{``}T_n\vdash\varphi^\mathbb{N}\text{''} and \text{``}T_n\vdash\varphi^\mathbb{N}\text{''}\rightarrow\varphi, for any φ in PAT. Modus ponens takes it from there!

Prev TOC Next

Leave a comment

Filed under Conversations, Peano arithmetic

Non-standard Models of Arithmetic 13

Prev TOC

MW: OK, back to the main plotline. Enayat asks for a “natural” axiomatization of PAT. Personally, I don’t find PAT 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

Leave a comment

Filed under Conversations, Peano arithmetic

First-Order Categorical Logic 6

Prev TOC

MW: An addendum to the last post. I do have an employment opportunity for one of those pathological scaffolds: the one where B(0) is the 2-element boolean algebra, and all the B(n)’s with n>0 are trivial. It’s perfect for the semantics of a structure with an empty domain.

The empty structure has a vexed history in model theory. Traditionally, authors excluded it from the get-go, but more recently some have rescued it from the outer darkness. (Two data points: Hodges’ A Shorter Model Theory allows it, but Marker’s Model Theory: An Introduction forbids it.)

Continue reading

Leave a comment

Filed under Categories, Conversations, Logic

First-Order Categorical Logic 5

Prev TOC Next

JB: Okay, let me try to sketch out a more categorical approach to Gödel’s completeness theorem for first-order theories. First, I’ll take it for granted that we can express this result as the model existence theorem: a theory in first-order logic has a model if it is consistent. From this we can easily get the usual formulation: if a sentence holds in all models of a theory, it is provable in that theory.

Continue reading

Leave a comment

Filed under Categories, Conversations, Logic

Non-standard Models of Arithmetic 12

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 PAT 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

Leave a comment

Filed under Conversations, Peano arithmetic

Algorithmic Information Theory

Back in the 60s, Kolmogorov and Chaitin independently found a way to connect information theory with computability theory. (They built on earlier work by Solomonoff.) Makes sense: flip a fair coin an infinite number of times, and compare the results with the output of a program. If you don’t get a 50% match, that’s pretty suspicious!

Three aspects of the theory strike me particularly. First, you can define an entropy function for finite bit strings, H(x), which shares many of the formal properties of the entropy functions of physics and communication theory. For example, there is a probability distribution P such that H(x)=−log P(x)+O(1). Next, you can give a precise definition for the concept “random infinite bit string”. In fact, you can give rather different looking definitions which turn out be equivalent; the equivalence seems “deep”. Finally, we have an analog of the halting problem: loosely speaking, what is the probability that a randomly chosen Turing machine halts? The binary expansion of this probability (denoted Ω by Chaitin) is random.

I wrote up my own notes on the theory, mostly to explain it to myself, but perhaps others might enjoy them.

Leave a comment

Filed under Logic

Review: Smullyan & Fitting, Set Theory and the Continuum Problem

The first sentence of Pollard’s review sums up my feelings perfectly: “This rewarding, exasperating book…” On balance, I found it more exasperating than rewarding. But it does have its charms.

I participated in a meetup group that went through the first two parts of S&F. My fellow participants possessed considerable mathematical knowledge and sophistication, but had only slight prior acquaintance with mathematical logic and none with axiomatic set theory. (The opinions here are strictly my own, but they reflect my experience in the meetup.) If I had just skimmed the book, glancing at familiar material, I would probably have a more positive impression.

I wrote an extensive set of notes for the meetup. This post is basically the last section of those notes.

I will begin with the book’s minuses, so as to end on a positive note.

Continue reading

Leave a comment

Filed under Logic, Reviews