"Classical" bicartesian closed category?

130 Views Asked by At

Every Heyting algebra can be thought of as a bicartesian closed category through which is also a poset.

We may interpret classical logic in a Heyting algebra if we ask of their pseudocomplements to be complements, i.e: to be boolean.

Can we give a similar definition with bicartesian closed categories in general and not get a preorder? That is, a "boolean bicartesian closed category".

Intuitively I'd say you can't but who knows.

2

There are 2 best solutions below

0
On BEST ANSWER

We can define Boolean bicartesian closed categories : for each object $A$, the canonical morphism from A to its bidual is an isomorphism. Then we can prove that such categories are necessarily thin.

If you accept the product not to be Cartesian, then you can consider star-autonomous categories: there are such categories that are not thin.

0
On

No, not in the manner you suggest. The "collapse" starts to happen the moment you allow initial objects and the exponential (and the product) to come together. That's for Cartesian closed categories. It doesn't matter whether it's bi-Cartesian or not.

I showed, in some detail, where and how the cascade of collapses happen here Decidability of bi-cartesian closed categories.

All of the "negative" formulae - those expressible as $¬A$, a.k.a. "regular" formulae - fall into a boolean lattice, where negation is defined by $¬A = A ⊃ ⊥$, and $⊥$ corresponds to the initial object. More generally and more precisely, the unique morphism $f: A → ¬B$ that witnesses the conditional $A ⊃ ¬B$ is given by $f = ⋀{([]_{A∧B})}^{-1}$, using the notation in the linked reply. This is true regardless of whether $A$ is negative or not.

The linked reply shows that if $g: A∧B → ⊥$, then $g = ([]_{A∧B})^{-1}$, where $[]_{A∧B}: ⊥ → A∧B$ is the unique morphism that witnesses the conditinal $⊥ ⊃ A∧B$. Under the "Curry" operator $⋀$, this becomes $⋀g: A → B ⊃ ⊥$. Conversely, if $f: A → ¬B = B ⊃ ⊥$, then $⋁f: A∧B → ⊥$, where $⋁$ is the inverse of the Curry operator, and uniqueness then gives us $⋁f = ([]_{A∧B})^{-1}$.

Nothing in this makes any mention of a co-product or requires it.