¿Existe una interpretación lógica para igualador y coigualador?

Question

Conozco el equivalente lógico a varias construcciones universales. Por ejemplo, el producto $\times$ es $\land$ y coproducto $+$ es $\lor$ . Las flechas asociadas son la proyección y la inclusión. El ecualizador arrow es una construcción posiblemente más sencilla, ¿existe una interpretación lógica?

Para el coproducto Si lo sé, puedo decir "Si lo sé $C$ se desprende de $A$ y también $C$ se desprende de $B$ por qué no almacenar esta información en la declaración que $C$ se desprende de $A\lor B$ ." y me imagino el diagrama de la propiedad universal.

Ahora el ecualizador, con dos flechas paralelas, es un poco más complicado. Porque si la lógica sólo se preocupa por las pruebas, $C$ de $A$ dicen, entonces has ganado cuando sólo hay una flecha. Me imagino que la respuesta será que alguien tiene que hay una sub-suposición $A'$ que es suficiente para la prueba de $C$ .

Answer 1

Su "categoría lógica" es un preorden, ordenado por implicación: los objetos son proposiciones, y hay una flecha $A \to B$ si y sólo si $A$ implica $B$ . Por tanto, hay como máximo un morfismo entre dos objetos cualesquiera.

Los igualadores y coigualadores en las categorías de preordenadas son un poco aburridos, ya que cualquier diagrama de la forma $$A \overset{f}{\underset{g}{\rightrightarrows}} B$$ debe tener $f=g$ . (Ambos $f$ y $g$ son sólo la declaración " $A$ implica $B$ "!)

Por lo tanto, en cualquier categoría de preorden, y en particular en su categoría de proposición y desentrañamiento, tenemos $$\mathsf{eq}(A \rightrightarrows B) = A \qquad \mathsf{coeq}(A \rightrightarrows B) = B$$ como puede comprobar fácilmente.

Esto se extiende incluso al caso en que un morfismo $A \to B$ es una prueba de $B$ de $A$ por lo que puede haber más de un morfismo de $A$ a $B$ . La clave es que cualquier morfismo $C \to A$ conmuta automáticamente con el diagrama de igualación: basta con pegar las pruebas una tras otra.

Answer 2

Los igualadores y coigualadores desempeñan un papel esencial en la lógica de cuantificadores categóricos. (Véase Makkai y Reyes, Lógica categórica de primer orden .)

Los ecualizadores se utilizan para interpretar la relación de igualdad (en un lenguaje de primer orden). En particular, dejemos que $\{x:t\}$ denotan un término en contexto, lo que significa que $t$ es un término de tipo $A_1,...,A_n;B$ y $x$ denota una secuencia de variables, incluyendo las variables libres en $t$ . En una interpretación $M$ , $M(\{x:t\})$ será una función de $M(A_1)\times \cdots \times M(A_n)$ a $M(B)$ . Entonces $M(\{x:t=t'\})$ se define como el ecualizador de las funciones $M(\{x:t\})$ y $M(\{x:t'\})$ .

Del mismo modo, los coequivalentes se utilizan para interpretar los tipos de cociente. En particular, si $E$ es una relación de equivalencia definible en una clase $A$ y si $p,q:E\to A$ son las proyecciones, entonces el ecualizador $e:A\to A/E$ de $p$ y $q$ da la proyección sobre el tipo de cociente.