MW: I’d like to chew a bit more on this matter of Trued versus True. This Janus-feature of the Tarski legacy fascinated me from the start, though I didn’t find it paradoxical. But now I’m getting an inkling of how it seems to you.
Category Archives: Conversations
Non-standard Models of Arithmetic 16
MW: Ok, let’s plunge into the construction of Trued(x). The bedrock level: True0(x), truth for (closed) atomic formulas. Continue reading
Filed under Conversations, Peano Arithmetic
Non-standard Models of Arithmetic 15
The Truth about Truth
MW: A little while back, I noted something delicious about the history of mathematical logic:
- Gödel’s two most famous results are the completeness theorem and the incompleteness theorem.
- Tarski’s two most famous results are the undefinability of truth and the definition of truth.
Filed under Conversations, Peano Arithmetic
Non-standard Models of Arithmetic 14
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.
Filed under Conversations, Peano Arithmetic
Non-standard Models of Arithmetic 13
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.)
Filed under Conversations, Peano Arithmetic
First-Order Categorical Logic 6
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.)
Filed under Categories, Conversations, Logic
First-Order Categorical Logic 5
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.
Filed under Categories, Conversations, Logic
Non-standard Models of Arithmetic 12
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?
Filed under Conversations, Peano Arithmetic
First-Order Categorical Logic 4
MW: I made up a little chart to help me keep all these adjoints straight:
Filed under Categories, Conversations, Logic
First-Order Categorical Logic 3
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
You can think of 
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.
Filed under Categories, Conversations, Logic
Diagonal Argument 