Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: FOL = and/exists + or/forall

Christian Williams (Feb 19 2024 at 21:17):

There's a great new paper called Diagrammatic Algebra of First Order Logic, where FOL is presented as a "union" of regular logic, i.e. the and/exists fragment of FOL, and its opposite, the fragment given by or/forall.

The or/forall fragment of FOL is rarely discussed, and yet it has a simple interpretation of defining "op-composition" of relations: $(R\bullet S)(x,z) = \forall y. R(x,y)\lor S(y,z)$, by considering a witness of a relation as an obstruction from one thing to another, rather than a connection.

Yesterday I realized that this or/forall fragment is the opposite fibration of regular logic. Given a regular fibration $R$, i.e. an "and/exists" cartesian bifibration, suppose that its opposite is also a regular fibration. This means that the fibers of $R$ are also cocartesian, giving "or", and substitution also has a right adjoint, giving "forall". Moreover, $R$ and $R^{op}$ are connected by "not", which forms a contravariant equivalence or "dual pair".
fol-dual-pair.png

Conjecture: A Boolean hyperdoctrine is equivalent to a dual pair in RegFib.

All thoughts welcome; thanks!

John Baez (Feb 19 2024 at 21:57):

The idea of treating first-order logic as a kind of "union" of and/$\exists$ and or/$\forall$ logic sounds really interesting!

John Baez (Feb 19 2024 at 22:00):

I'm not sure how you'd get the Boolean aspect of a Boolean hyperdoctrine out of a dual pair in RegFib: I would naively expect you'd get some more general type of hyperdoctrine, because I don't see how the principle of excluded middle would emerge "automatically" given a dual pair in RegFib. But I imagine a lot of category theorists would be happy to see some more general type of hyperdoctrine emerge here. So I don't see this as a problem so much as a possible refinement of your conjecture.

Mike Shulman (Feb 19 2024 at 22:04):

@John Baez, that was my first reaction as well, but then I realized Christian is saying something about $R$ and $R^{\rm op}$ being equivalent via a negation operator, which is a version of the double-negation law $\neg\neg p = p$. So it doesn't seem so far-fetched to me. But "dual pair" may not be the right name for this, maybe "self-dual object"?

John Baez (Feb 19 2024 at 22:10):

Oh, okay. So you're saying that in some context relevant to this "not" being an equivalence is enough to get $\neg \neg p = p$?

John Baez (Feb 19 2024 at 22:11):

Two other tricky aspects of the idea of hyperdoctrine are the Beck-Chevalley condition and Frobenius reciprocity. Do they both fall out automatically here?

Mike Shulman (Feb 19 2024 at 22:17):

John Baez said:

Oh, okay. So you're saying that in some context relevant to this "not" being an equivalence is enough to get $\neg \neg p = p$?

Well, that's what the conjecture is guessing. I'm not proposing a proof of the conjecture, just saying it doesn't seem as obviously false as I thought it was at first. (-:

Mike Shulman (Feb 19 2024 at 22:18):

I think the Beck-Chevalley condition for $\exists$ and Frobenius reciprocity are part of the definition of regular hyperdoctrine, so if I understand correctly they are built into what Christian is proposing.

John Baez (Feb 19 2024 at 22:25):

Do you mean part of the definition of regular fibration? He's assuming we have a regular fibration whose opposite is a regular fibration (and now is the time for me to admit that I don't know what a regular fibration is).

Mike Shulman (Feb 19 2024 at 22:28):

I guess I assumed he was talking about a [[regular hyperdoctrine]].

Mike Shulman (Feb 19 2024 at 22:29):

"regular fibration" doesn't seem to exist on the nLab, so if it's not the same as a regular hyperdoctrine, maybe I don't know what it is either.

Christian Williams (Feb 19 2024 at 22:41):

Yes, I mean that. It's called a regular fibration in Jacobs' Categorical Logic: reg-fib.png

and also in Finn Lawler's thesis Fibrations of predicates and bicategories of relations, though there it doesn't need to be preordered.

Christian Williams (Feb 19 2024 at 22:58):

Yeah, so because posets are thin, a self-duality $n:R(A)\simeq R(A)^{op}$ gives a contravariant involution, so I think it should be both necessary and sufficient for the law of excluded middle.

Christian Williams (Feb 19 2024 at 23:01):

Unless I'm missing something, it seems like the conjecture will follow just from abstract duality; mainly the fact that a fibration has sums iff its opposite has products.

Mike Shulman (Feb 19 2024 at 23:04):

Hmm... Thinking about it some more, I don't think the existence of a contravariant involution implies excluded middle unless you ensure in some other way that the involution is the Heyting negation. In particular, any $\ast$-autonomous lattice has a contravariant "linear" involution that isn't the Heyting negation. For instance, Lukaciewicz logic is the linearly ordered poset $[0,1]$, which is a lattice with a contravariant involution $x\mapsto 1-x$, but it isn't a Boolean algebra.

Christian Williams (Feb 19 2024 at 23:14):

Hm, okay... maybe it has to do with the compatibility of the duality with the adjoints.

Christian Williams (Feb 19 2024 at 23:57):

Okay, well it's possible that the theorem is actually:
A self-dual object in RegFib is equivalent to a "de Morgan hyperdoctrine", a Boolean HD without LEM.

That would be an interesting generalization; but it'd be nice if we had SelfDual(RegFib) ~ BoolHD. It's not yet clear whether $n(U)\lor U = 1$ might follow from the structure... I'll be thinking about it.

John Baez (Feb 20 2024 at 00:21):

Okay, now I see that Frobenis reciprocity is built into the definition of "regular fibration" - thanks, @Christian Williams. Where does Beck-Chevalley for your hyperdoctrine come from? Is it obvious for some reason? Or on the opposite extreme, maybe you're not hoping to get that?

Christian Williams (Feb 20 2024 at 00:23):

I'm thinking of a regular fibration as having both Frobenius and Beck-Chevalley
(BC for certain squares defined by cartesian structure):
https://ncatlab.org/nlab/show/regular%20hyperdoctrine
https://ncatlab.org/finnlawler/show/regular+fibration

Hyperdoctrines by Seely is a good source; see Section 3.

Evan Washington (Feb 20 2024 at 00:34):

What I'm not seeing is where implications might come in. It seems each fiber is bicartesian, but is each also cartesian closed (and so a bicartesian closed preorder = Heyting algebra)? A Heyting algebra satisfying double negation elimination is Boolean, so that might help. (So every Heyting algebra which is also a de Morgan algebra is Boolean)

John Baez (Feb 20 2024 at 00:39):

Christian Williams said:

I'm thinking of a regular fibration as having both Frobenius and Beck-Chevalley.

Okay. So is that different than Jacobs' definition of regular fibration which you just showed us?

.

Christian Williams (Feb 20 2024 at 00:39):

Thanks, yeah I think this is equivalent to the oversight I was making... what is DNE again?

Christian Williams (Feb 20 2024 at 00:40):

And no, it's equivalent. Jacobs' notion of fibered co/products includes Beck-Chevalley.

John Baez (Feb 20 2024 at 00:40):

Oh, okay. Thanks!

Valeria de Paiva (Feb 20 2024 at 00:43):

DNE is usually double negation elimination $\neg \neg p\to p$.

Christian Williams (Feb 20 2024 at 00:48):

I didn't know about all these intermediate structures, like de Morgan Heyting algebra.

Christian Williams (Feb 20 2024 at 00:50):

Is there a simple name for cartesian closed poset?

Valeria de Paiva (Feb 20 2024 at 00:54):

Is there a simple name for cartesian closed poset?

well, I call a symmetric monoidal closed poset a "lineale" because they're exactly what you need for the multiplicative connectives of ILL. (quantales have completeness, which is not necessary).

Christian Williams (Feb 20 2024 at 00:57):

Hm, okay thanks.

In the notion of regular fibration, I think if we replace "meet semilattice" with "closed meet semilattice", then by Evan's suggestion I think self-dual objects in there will be equivalent to Boolean hyperdoctrines.

Christian Williams (Feb 20 2024 at 01:00):

Even if there isn't a standard simple name, I think cartesian closed posets are very natural in categorical logic; and I think there's an intermediate kind of hyperdoctrine that has yet to be named.

Christian Williams (Feb 20 2024 at 01:03):

And by phrasing the theorem in that way, it also highlights that a Boolean algebra is "cocartesian coclosed".

Valeria de Paiva (Feb 20 2024 at 01:05):

Even if there isn't a standard simple name, I think cartesian closed posets are very natural in categorical logic;

I agree!

Evan Washington (Feb 20 2024 at 01:10):

Christian Williams said:

I didn't know about all these intermediate structures, like de Morgan Heyting algebra.

What a confusing collection of names here! By DNE I just double negation elimination, that's right. And the hierarchy of intermediate logics (between intuitionistic logic and classical logic) is surprisingly rich (there are continuum-many; they organize in a lattice, in fact a Heyting algebra!)

Evan Washington (Feb 20 2024 at 01:23):

Christian Williams said:

Is there a simple name for cartesian closed poset?

I've heard them called relatively pseudocomplemented semilattices, implicative semilattices, or Brouwerian semilattices

Valeria de Paiva (Feb 20 2024 at 01:31):

And the hierarchy of intermediate logics (between intuitionistic logic and classical logic) is surprisingly rich

and it gets even worse if you remove structural rules, e.g. https://www.researchgate.net/publication/2505247_Lineales_Algebraic_Models_of_Linear_Logic_from_a_Categorical_Perspective

Christian Williams (Feb 20 2024 at 01:42):

So for the theorem, I think the question that remains is: what characterizes the negation operator? Heyting algebras can have other involutions, but somehow negation is special.

Valeria de Paiva (Feb 20 2024 at 01:53):

well, if negation is implication into falsum ($\neg A\cong A\to \bot$) then you need to have an (weak) initial object $\bot\to A$ for any $A$?

Christian Williams (Feb 20 2024 at 02:17):

Well, I'm looking for what characterizes the map $H(-,\bot):H^{op}\to H$. Like how do we recognize when an involution $i:H^{op}\to H$ is actually the negation operator.

Mike Shulman (Feb 20 2024 at 02:38):

One might argue that "cartesian closed poset" is a perfectly standard simple name, not to mention descriptive. After all, we don't object to "cartesian closed category".

Mike Shulman (Feb 20 2024 at 02:44):

Christian Williams said:

In the notion of regular fibration, I think if we replace "meet semilattice" with "closed meet semilattice", then by Evan's suggestion I think self-dual objects in there will be equivalent to Boolean hyperdoctrines.

I don't follow, how is this ensuring that the duality is the negation?

Mike Shulman (Feb 20 2024 at 02:45):

Christian Williams said:

Well, I'm looking for what characterizes the map $H(-,\bot):H^{op}\to H$. Like how do we recognize when an involution $i:H^{op}\to H$ is actually the negation operator.

Well, the universal property of $\neg$ in a cartesian closed poset with initial object $\bot$ is that $x \le \neg y$ iff $x\wedge y = \bot$.

Christian Williams (Feb 20 2024 at 17:44):

Okay, well whatever the exact characterization, the point is:
First order logic, historically modelled by hyperdoctrines involving triple adjoints, can be understood as a union of two simpler parts - regular logic and its opposite.

It's a beautiful idea, and I'm glad I was introduced to this (new!) paper, Diagrammatic Algebra of FOL.

Alessandro Di Giorgio (Feb 20 2024 at 18:37):

Hi @Christian Williams , I’m happy to hear you liked our paper! :)

What you say sounds really interesting and I wonder how it relates to A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine, where the authors also propose a graphical language reminiscent of Peirce’s EGs

Christian Williams (Feb 20 2024 at 19:56):

Oh thanks, this is great. Yes, these string diagrams certainly look related --
I think there is a 3D language of FOL in which the sequents of regular logic go inner to outer, and the sequents of its opposite go outer to inner.