Category Archives: Conversations

Non-standard Models of Arithmetic 14

Prev TOC

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

\{\varphi\rightarrow\text{Con}(T_n+\varphi^\mathbb{N}):\varphi\in\text{L(PA)},n\in\omega\}

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.

Continue reading

Leave a comment

Filed under Conversations, Peano arithmetic

Non-standard Models of Arithmetic 13

Prev TOC Next

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

First-Order Categorical Logic 4

Prev TOC  Next

MW: I made up a little chart to help me keep all these adjoints straight:

Continue reading

Leave a comment

Filed under Categories, Conversations, Logic

First-Order Categorical Logic 3

Prev TOC Next

JB: Okay, let’s talk more about how to do first-order classical logic using some category theory. We’ve already got the scaffolding set up: we’re looking at functors

B \colon \textrm{FinSet} \to \textrm{BoolAlg}.

You can think of B(S) as a set of predicates whose free variables are chosen from the set S. The fact that B is a functor captures our ability to substitute variables, or in other words rename them.

But now we want to get existential and universal quantifiers into the game. And we do this using a great idea of Lawvere: quantifiers are adjoints to substitution.

Continue reading

Leave a comment

Filed under Categories, Conversations, Logic

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.

Continue reading

1 Comment

Filed under Conversations, Peano arithmetic

Non-Standard Models of Arithmetic 10

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

1 Comment

Filed under Conversations, Peano arithmetic

First-Order Categorical Logic 2

Prev TOC Next

MW: So let’s see. Last time we talked about the functor B from the category FinSet to the category BoolAlg of boolean algebras. Liberal infusions of coffee convinced you that B is covariant; I accidentally suggested it was contravariant. I think I’ve come round to your position, but I still have a couple of things I want to say on the matter. If it won’t be too confusing for our readers.

JB: Okay.  If we’re planning to talk more about the variance, it’s probably good to start out by getting the reader a bit confused.  I used to always be confused about it myself.  Then I finally felt I had it all straightened out.  Then you shocked me by arguing that it worked the opposite way.  Your argument was very sneaky.

Continue reading

Leave a comment

Filed under Categories, Conversations, Logic