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: deprecated: logic

Topic: All models of classical logic are posets

Max New (Jan 10 2023 at 13:36):

I know I've seen a there is a theorem that states that, unlike intuitionistic propositional logic (IPL) where any cartesian closed category gives a model, if you try to define the structure on a category to interpret classical propositional logic (CPL) then you can show that the only models are preorders. This gives a precise sense in which (CPL) cannot be given the same kind of constructive interpretation as IPL and we have to change something to get a computational interpretation of classical logic (linearity, evaluation order, etc).

But I'm not having any luck finding a reference. Does anyone have a good one?

The only precise formulation I can remember is that if something is a biCCC then it has a strict initial object (Any A -> 0 is an isomorphism) and so with classical logic the opposite category should also be a biCCC and so a model of classical logic would have a strict terminal object (Any 1 -> A is an isomorphism) which would for example make inl(): 1 + 1 and inr(): 1 + 1 equal.

Matt Earnshaw (Jan 10 2023 at 14:04):

try Lambek and Scott, Prop 8.3

vikraman (Jan 10 2023 at 14:50):

It was originally observed by Joyal, and is Thm 2.3 here: http://sro.sussex.ac.uk/id/eprint/1439/1/streicherreus1998.pdf, and also in Lambek & Scott

Max New (Jan 10 2023 at 15:36):

Thanks both, I think these were exactly the 2 theorems I had in mind. For posterity, it's Prop 8.3 in part I of Lambek & Scott (page 67 in my copy)

Max New (Jan 10 2023 at 15:42):

The lemma from Joyal is also mentioned on the nlab here: https://ncatlab.org/nlab/show/dualizing+object+in+a+closed+category

Max New (Jan 10 2023 at 16:37):

The Streicher-Reus paper is a bit confusing to me. It looks like the object they write as $\bot$ is only the initial object of $\mathcal N_R$ if $R$ is the domain with one element, in which case $\mathcal N_R$ is the terminal category? So it seems misleading of them to say that the only problem with interpreting classical logic as a category is that $\neg\neg A$ is only logically equivalent rather than isomorphic to $A$. And also I don't think there's coproducts on this category so it interprets only a fragment of classical propositional logic.

I wonder: are there any non-trivial biCCCs where $\neg\neg A$ and $A$ are logically equivalent for all $A$?

Max New (Jan 10 2023 at 16:45):

oh yes even Finite sets satisfy this

Max New (Jan 10 2023 at 16:54):

but the $\neg \neg A \to A$ is not natural hm

vikraman (Jan 10 2023 at 17:07):

They write $\bot$ for the initial object of $\mathcal N_R$ (def 2.3, for any $R$). Another way of thinking about this $\mathcal N_R$ is that it's isomorphic to the dual of the Kleisli category of the continuation monad $R^{R^{(-)}}$.

Max New (Jan 10 2023 at 17:58):

The definition of $\bot$ is $\{*\}$, and so a morphism out of $\bot$ is $\mathcal N_R(\bot, X) = \text{Cont}(R^{\{*\}}, R^X)$ which is equivalent to $\text{Cont}(X \times R, R)$. This is a weakly initial object because you always have the projection morphism, but it will only be unique if $R$ is the terminal domain $\{*\}$, in which case the category $\mathcal N_R$ is trivial.

vikraman (Jan 10 2023 at 21:25):

I see, but if you used $\mathcal N_R(X,Y) = C(R^{R^Y},X)$, you'd get a $\bot$. The $\bot$ is not really necessary though, since they could use $\neg A = R^A$ (remark 2.2).