Esto es en realidad en referencia a la pregunta planteada aquí https://stackoverflow.com/posts/66285948/edit pero es más apropiado como pregunta para ser planteada en un sitio no codificado.
Proporciono una respuesta parcial, pero no la respuesta completa, transmitiendo la pregunta completa aquí como una pregunta sin resolver. Quizás otros puedan tomar el testigo.
La pregunta es: ¿qué procedimientos de decisión existen para las categorías cerradas bicartesianas? (Una pregunta secundaria es: ¿qué estrategias de reducción de orden normal existen para ellas?)
Las siguientes observaciones ayudarán a ilustrar por qué se excluye el objeto inicial en la referencia citada en el enlace original. Las cosas empiezan a colapsarse cuando los objetos iniciales se combinan con exponenciales; o los objetos terminales con coexponenciales. Este colapso se completa cuando están presentes tanto los exponenciales como los co-exponenciales; en cuyo caso, el problema de decidibilidad se vuelve trivial, reduciéndose a la demostrabilidad en una lógica, mientras que el problema de reducción de la "forma normal" se vuelve más difícil - irónicamente.
En una categoría, un objeto inicial $0$ , objeto terminal $1$ , producto $A,B ↦ A×B$ , coproducto $A,B ↦ A+B$ , exponencial $A,B ↦ B^A$ y co-exponencial $A,B ↦ A_B$ (si se nos permite denotarlas así) corresponden respectivamente a las constantes y conectivas de la lógica $⊥$ (falso), $⊤$ (verdadero), $A,B ↦ A∧B$ (y), $A,B ↦ A∨B$ (o), $A,B ↦ A⊃B$ (sólo si) y $A,B ↦ A⊂B$ (a no ser que) (de nuevo: si se nos permite denotar así).
Esta correspondencia se precisa de la siguiente manera: si el pedido previo $A ≤ B ⇔ ∃f: A → B$ se define sobre objetos, y si los objetos se identifican hasta la equivalencia ( $A ≡ B$ si y sólo si $A ≤ B$ y $B ≤ A$ ), entonces $⊤$ , $⊥$ , $∧$ y $∨$ son la parte superior de la red, la parte inferior, el encuentro y la unión, respectivamente, mientras que $⊃$ y $⊂$ son, respectivamente, los operadores de implicación y de coimplicación de una red de Heyting y de coimplicación.
Si todo lo siguiente $\{ ∧, ⊃, ⊥ \}$ están presentes juntos entonces también lo está $⊤$ y entonces la categoría se reduce prácticamente a una lógica. Más precisamente: tiene una conectiva de negación, definida hasta la equivalencia por $¬A ≡ A ⊃ ⊥$ y la subcategoría completa de los objetos regulares (es decir, aquellos objetos $A$ para lo cual $A$ y $¬¬A$ son equivalentes) es un orden parcial y, de hecho, se reduce a un álgebra booleana (con lo que todas esas equivalencias son también isomorfismos).
Es decir, si $A$ , $B$ son objetos regulares y $f: A → B$ y $f': A → B$ entonces $f = f'$ y tal $f$ existe si y sólo si $A ≤ B$ . Desde $¬¬¬A$ y $¬A$ son isomorfos, entonces los objetos regulares comprenden todas las negaciones y los objetos negativos $¬A$ forman una subcategoría que es en realidad una lógica booleana.
Un álgebra categórica que incluye cualquiera de los conjuntos completos de conectivas $\{ ∧, ⊃, ⊥ \}$ o $\{ ∨, ⊂, ⊤ \}$ contiene, por tanto, un álgebra categórica para la propia álgebra de Boole, como subálgebra. Una de estas álgebras fue, de hecho, dada por Spencer-Brown en las "Leyes de la Forma", aunque no reconoció que se trataba de un álgebra categórica; ya que la teoría de categorías era prácticamente desconocida en aquella época y las álgebras categóricas probablemente ni siquiera se conocían en absoluto, en ese momento. Spencer-Brown definió en realidad un grupo de álgebras booleanas, no sólo una categoría, ya que sus flechas eran todas reversibles y eran en realidad isomorfismos.
Se puede describir de forma equivalente como una categoría monoidal trenzada, cuyos objetos son cadenas, con el operador producto $x,y ↦ xy$ se denota por yuxtaposición, el objeto terminal por la cadena vacía $λ$ . La categoría está dotada de un operador extra (denotado por un círculo en el operando) que podría ser denotado aquí $x ↦ ❨x❩$ . Los isomorfismos que definió fueron Posición $❨❨x❩x❩ ↔ λ$ Transposición $❨❨xz❩❨yz❩❩ ↔ ❨❨x❩❨y❩❩z$ y un isomorfismo implícito $xy ↔ yx$ para la conmutatividad, que ya forma parte de la definición de las categorías monoidales trenzadas. Es coherente (sólo un morfismo por flecha), y se dio un procedimiento de decisión sobre las leyes de forma de Spencer-Brown. El functor $x ↦ ❨x❩$ se denota más adecuadamente como un "antifunctor", ya que mapea la categoría a su inversa.
Si se sustituye la transposición por morfismos para Número $xx ↔ x$ , Orden $❨❨x❩❩ ↔ x$ y Ortho $❨xy❩❨y❩ ↔ ❨y❩$ entonces esto es suficiente para caracterizar los retículos ortocomplementados. No sé cómo se puede adaptar el procedimiento especificado por Spencer-Brown a esta generalización. Ni siquiera estoy seguro de que se pueda colapsar a una categoría coherente.
El "colapso" parcial puede verse directamente como sigue, donde consideraremos la combinación $\{ ∧, ⊃, ⊥ \}$ que combina exponenciales y objetos iniciales: Categorías cartesianas cerradas con objetos iniciales.
Cada conectivo puede definirse de forma equivalente como un functor sobre la categoría que viene equipado con una biyección natural que proporciona el álgebra categórica para el conectivo y las reglas de prueba para la lógica correspondiente.
Para lo que sigue, adopte las siguientes convenciones. Para una categoría $
