JB: So, let’s think about how we can prove this generalization of Gödel’s completeness theorem. First, remember that a hyperdoctrine B is consistent iff B(0) has at least two elements, or in other words, ⊤ ≠ ⊥ in this boolean algebra. Second, let’s say a hyperdoctrine C is set-based if every C(n) is the power set of Vn for some fixed set V. We call V the universe. Third, let’s say a morphism of hyperdoctrines, say F: B → C, is a natural transformation whose components F(n): B(n) → C(n) are Boolean algebra homomorphisms obeying the Beck–Chevalley condition and maybe the Frobenius condition. (We’re a bit fuzzy about this and we’ll probably have to sharpen it up.) Continue reading
Author Archives: John Baez
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
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
B:FinSet→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.
Filed under Categories, Conversations, Logic
Non-Standard Models of Arithmetic 10
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.
Filed under Conversations, Peano Arithmetic
First-Order Categorical Logic 1
(A conversation between John Baez and Michael Weiss.)
JB: Okay, maybe it’s a good time for me to unleash some of my crazy thoughts about logic. They’ve been refined a lot recently, thanks to all the education I’ve been getting from you and folks on the n-Category Café. So, I can actually start with stuff that’s not crazy at all… although it may seem crazy if you’re not used to it.
I’ll start with some generalities about first-order classical logic. (I don’t want to get into higher-order logic or intuitionistic logic here!) The first idea is this. In the traditional approach, syntax and semantics start out living in different worlds. In categorical logic, we merge those worlds.
Filed under Categories, Conversations, Logic
Non-standard Models of Arithmetic 6
JB: It’s interesting to see how you deploy various philosophies of mathematics: Platonism, intuitionism, formalism, etc. For a long time I’ve been disgusted by how people set up battles between these, like Punch-and-Judy shows where little puppets whack each other, instead of trying to clarify what any of these philosophies might actually mean.
For example, some like to whack Platonism for its claim that numbers “really exist”, without investigating what it might mean for an abstraction—a Platonic form—to “really exist”. If you define “really exist” in such a way that abstractions don’t do this, that’s fine—but it doesn’t mean you’ve defeated Platonism, it merely means you’re committed to a different way of thinking and talking.
Filed under Conversations, Peano Arithmetic
Diagonal Argument 