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
Category Archives: Conversations
First-Order Categorical Logic 13
MW: It’s been a minute! Well, almost 60,000 minutes.
We left off with a question: does a natural transformation from a syntactic hyperdoctrine to a semantic hyperdoctrine automatically “respect quantifiers”? We saw that this amounts to a Beck–Chevalley condition. We wondered if we had to add that condition to our definition of a model, or if it came for free. Continue reading
Filed under Categories, Conversations, Logic
Nonstandard Models of Arithmetic 32
Prev TOC Next
Previous Paris-Harrington post
[Ed. note: This post was essentially ready two years ago, but I got distracted with other matters. If you’re seeing this for the first time, or want to refresh your memory, posts 8 and 9 introduced the Paris-Harrington theorem. Posts 21 through 24 continued the discussion, in a dialog with Bruce Smith. MW]
Filed under Conversations, Peano Arithmetic
First-Order Categorical Logic 12
MW: Last time we looked at the categorical rendition of “C is a model of B”:
- Functors B:FinSet→BoolAlg and C:FinSet→BoolAlg
- A natural transformation F:B→C
where B and C are hyperdoctrines, and
- B is syntactic: the elements of each B(n) are equivalence classes of formulas (which we agreed to call predicates);
- C is semantic: the elements of each C(n) are relations on a domain V.
(We’ve been saying that C(n) is the set of all n-ary relations on V, but I see no need to assume that.)
Filed under Categories, Conversations, Logic
First-Order Categorical Logic 11
MW: Last time we justified some equations and inequalities for our adjoints: they preserve some boolean operations, and “half-preserve” some others. And we incidentally made good use of the color palette!
Filed under Categories, Conversations, Logic
First-Order Categorical Logic 10
JB: Last time we saw how to get some laws of logic from two facts:
• right adjoint functors between boolean algebras preserve products (‘and’),
and
• left adjoint functors between boolean algebras preserve coproducts (‘or’).
Filed under Categories, Conversations, Logic
First-Order Categorical Logic 9
Filed under Categories, Conversations, Logic
First-Order Categorical Logic 8
MW: We’re reviewing hyperdoctrines, which are specially nice functors B: FinSet → BoolAlg. When we have such a functor, any map f of finite sets gives a homomorphism of boolean algebras, B(f). But we’ve seen this is a morphism and a functor. (“It’s a floor wax and a dessert topping!”) What do you think about the term “adjoint morphism”? It might help keep the two levels straight.
Filed under Categories, Conversations, Logic
First-Order Categorical Logic 7
MW: John, it’s been eons since we last discussed First-Order Categorical Logic: not since September 2019! (I read a lot of Russian novels during the break.) But New Year’s seems like a good time to resume the tale.
JB: Yes indeed! It’s been a long time, and it’s mostly my fault. Let’s see if we can get back up to speed.
Filed under Categories, Conversations, Logic
Nonstandard Models of Arithmetic 31
MW: Last time we learned about the “back-and-forth” condition for two countable structures M and N for a (countable) language L:
Filed under Conversations, Peano Arithmetic
Diagonal Argument 