¿Una conexión entre las operaciones del espacio vectorial y las conectivas intuicionistas?

Question

Mientras trabajaba en el libro de Steven Roman Álgebra lineal avanzada Me encontré con esto en el capítulo 11, ejercicio 1.

Dejemos que $U,W$ sean subespacios de un espacio vectorial métrico $V$ . Demostrar que
(a) $U\subseteq W \implies W^\bot\subseteq U^\bot$
(b) $U\subseteq U^{\bot\bot}$
(c) $U^\bot = U^{\bot\bot\bot}$

Además, $(U+W)^\bot = U^\bot \cap W^\bot$ y $U^\bot + W^\bot \subseteq (U\cap W)^\bot$ . Estoy teniendo algunos problemas con la inclusión inversa (al menos no es tan evidente como lo eran las otras).
Todas estas propiedades son sorprendentemente similares al comportamiento de las conectivas en la lógica intuicionista, por ejemplo $p\rightarrow q \vdash \neg q\rightarrow \neg p$ , $\vdash p \rightarrow \neg\neg p$ , $\vdash \neg p \leftrightarrow \neg\neg\neg p$ , $\vdash \neg(p \lor q) \leftrightarrow \neg p \land \neg q$ , $\vdash \neg p \lor \neg q \rightarrow \neg(p\land q)$ .
¿Hay alguna conexión aquí? Si es así, ¿cuál es?

Answer 1

He aquí una perspectiva que unifica todas las respuestas anteriores. Como es lógico, se basa en teoría de categorías .

El lógica interna de un categoría simétrica monoidalmente cerrada es lógica lineal intuicionista multiplicativa (MILL). Una categoría monoidal es aquella que tiene una noción adecuada de producto tensorial, $\otimes$ (con unidad $I$ ). Es simétrico si tenemos un isomorfismo natural, $\sigma_{AB}:A\otimes B\cong B\otimes A$ , de tal manera que $\sigma_{BA}\circ\sigma_{AB}=id_{A\otimes B}$ . Es monoidalmente cerrado si tenemos $\text{hom}$ objetos caracterizado por el tensor-homología adición . Voy a escribir $A\multimap B$ para $\text{hom}(A,B)$ .

Un ejemplo arquetípico de categoría simétrica monoidalmente cerrada es $\mathbf{Vect}_k$ la categoría de $k$ -espacios vectoriales para un campo $k$ . Volviendo a una categoría arbitraria, en el caso especial de que $\otimes = \times$ El producto categórico hablamos de una categoría monoidal cartesiana. Una categoría monoidal cartesiana cerrada se llama categoría cerrada cartesiana . En este caso, el hom interno es el objeto exponencial. Por ejemplo, $\mathbf{Set}$ es una categoría cerrada cartesiana con $X\multimap Y$ escrito $Y^X$ el conjunto de funciones de $X$ a $Y$ . La lógica interna de una categoría cerrada cartesiana arbitraria es (un fragmento de) la lógica proposicional intuicionista (o mejor lógica mínima ). $\mathbf{Vect}_k$ no es cartesiano cerrado sin embargo.

Las conexiones de Galois que menciona Stephen A. Meigs se generalizan directamente a las adjunciones en categorías simétricas monoidales cerradas. En primer lugar, tenemos la propia adjunción tensor-hom: $(-)\otimes B \dashv B\multimap(-)$ . Esto establece que $\mathsf{Hom}(A\otimes B,C)\cong\mathsf{Hom}(A,B\multimap C)$ natural en $A$ y $C$ (y de hecho también $B$ pero esto va más allá de lo que el adjunto inmediatamente estados). (También, $\mathsf{Hom}(A,B)$ es el hom- set de flechas de $A$ a $B$ No hay que confundirlo con el hogar interno, $\text{hom}$ que es un objeto de la propia categoría. Sin embargo, como su nombre indica, el hom interno "internaliza" muchos aspectos de los hom-sets). La simetría también nos da la siguiente adjunción $((-)\multimap C)^{op}\dashv (-)\multimap C$ o $\mathsf{Hom}(A,B\multimap C)\cong\mathsf{Hom}(B,A\multimap C)$ . Como ya se ha mencionado, y como sugiere la notación, estas adjunciones corresponden a las reglas lógicas para $\otimes$ y $\multimap$ en la lógica lineal, que, en el caso cartesiano, corresponden a $\land$ y $\to$ en lógica proposicional (no lineal) (mínima, intuicionista o clásica).

Ahora MILL no contiene $(-)^\perp$ . Podemos, sin embargo, hacer lo que hacen en la lógica mínima que es definir la "negación" $\neg A$ (así $A^\perp$ para nosotros) como simplemente $A\to R$ ( $A\multimap R$ ) para alguna proposición arbitraria pero fija $R$ . Una opción natural es elegir $R=I$ la unidad del producto tensorial. (Una elección más natural en cuanto a negación se refiere es $R=0$ o $R=\bot$ pero no hemos asumido esa estructura). Todas las reglas que mencionas se generalizan en el álgebra lineal a partir de afirmaciones sobre $V^\perp$ a las declaraciones sobre $\text{hom}(V,W)$ es decir, vemos $V^\perp$ como $\text{hom}(V,k)$ (donde $k$ es el campo subyacente). $k$ es en realidad la unidad del tensor, es decir $k=I$ . Esto corresponde, para una categoría general simétrica monoidalmente cerrada, a definir $A^\perp\equiv A\multimap I$ . Puede verificar casi todas las leyes que menciona. Una forma de manejar $\lor$ es añadir coproductos categóricos de los cuales el suma directa de los espacios vectoriales, $\oplus$ es un ejemplo. (Obsérvese que la forma de tratar la disyunción es uno de los puntos en los que las perspectivas intuicionista y clásica empiezan a divergir significativamente). En este caso, tenemos $(A\oplus B)\multimap C \cong (A\multimap C)\times (B\multimap C)$ como un caso especial (algo disfrazado) del hecho muy general y muy útil de que las uniones derechas preservan los límites, en este caso llevando productos (en la categoría opuesta, por tanto coproductos) a productos. Podemos hacer estas afirmaciones sobre el subobjetos $A\cap B$ y $A\cup B$ (dado que tenemos la estructura adecuada para interpretarlos) que encaja un poco mejor.

Todo esto forma parte de un patrón más amplio conectando lógica, teoría de tipos, teoría de categorías y computación .

Answer 2

No conozco los detalles, pero siempre he pensado que algo así fue parte de la motivación de lógica lineal -- donde la negación se anota incluso $p^\bot$ en lugar de $\neg p$ y tenemos las conectivas $\otimes$ y $\oplus$ que parecen corresponder al producto tensorial y a la suma directa de espacios vectoriales de una forma agradable.

En particular, lógica lineal intuicionista parece estar más cerca del álgebra lineal que la lógica lineal clásica.

Answer 3

Esta es la conexión que veo (aunque no soy un experto, pero lo que has notado siempre me ha fascinado):

Consideremos el fragmento de la lógica proposicional intuicionista que no tiene $\to$ (pero tiene $\neg$ , que aquí es una primitiva así que no $\to \bot$ )

Entonces podemos interpretar cualquier fórmula de nuestro fragmento en un espacio pre-Hilbert (real o complejo), dada cualquier asignación de subespacios a variables proposicionales. $\neg$ se interpreta como $^\bot$ , $\land$ como $\cap$ y $\lor$ como $+$ .

Creo que si se añade $\to$ a su fragmento y realizar pruebas en (un reducido - ver más adelante por qué) cálculo secuencial y al final obtener $H\vdash A$ con $H,A$ que no contenga $\to$ entonces el subespacio asociado a $H$ estará contenido en el subespacio asociado a $A$ .

En particular, $\neg\neg\neg p\vdash \neg p$ para cada $p$ produce (c) y $p\vdash \neg\neg p$ produce (b) (si es que son demostrables a partir del cálculo secuencial reducido en cuestión, yo diría que lo son: de nuevo, véase más abajo. No estoy muy seguro en el caso de los espacios vectoriales, pero por analogía con los anillos diría que es el caso)

El problema es, por supuesto, que no podemos interpretar $\to$ lo cual es algo triste.

Permítanme dar otro ejemplo en el que, de hecho, se puede interpretar $\to$ pero no siempre obtenemos la lógica intuicionista (sin embargo un punto muy interesante es que vemos como la lógica lineal obtiene dos "y" diferentes)

Consideremos un anillo conmutativo (unital) $R$ . En realidad interpretaremos nuestra lógica en el conjunto de ideales de $R$ de la siguiente manera: asignamos un ideal a cada variable proposicional (denotado $[p]$ ), entonces $[\bot] = 0, [\top] = R$ y luego definir inductivamente $[A\to B] = ([B]: [A]) = \{x\in R\mid \forall y \in [A], xy\in [B]\}$ , $[A\land B] = [A] [B]$ (nótese que aquí podemos elegir entre el producto de los ideales y la intersección: así podemos ver de dónde saca la lógica lineal sus diferentes "y"), $[A\lor B] = [A]+[B]$ (No he dado una cláusula para $\neg$ porque aquí podemos definir $\neg A := (A\to \bot)$ )

Esta estructura no satisface necesariamente la lógica intuicionista (es decir, podemos tener secuencias intuitivamente demostrables $H\vdash A$ tal que $[H]$ no está incluido $[A]$ ), pero satisface algunas reglas básicas, en particular satisface la "introducción de la implicación": si $p\land q \vdash r$ entonces $p\vdash q\to r$ es una regla válida (se supone que $IJ \subset K$ y elegir $x\in I$ , entonces dado $y\in J$ , $xy\in IJ \subset K$ así que $xy\in K$ así que $x\in (K:J)$ ); también satisface "si $p\vdash q$ entonces $r\land p\vdash r\land q$ (suponer $I\subset J$ . Entonces $KI\subset KJ$ ); y una forma débil de modus ponens : $p\land (p\to q) \vdash q$ (obvio por la definición de $[A\to B]$ ) - Lo llamo modus ponens débil porque es más débil que " $p\vdash r\to q$ y $p\vdash r$ implica $p\vdash q$ " (esto correspondería a la otra "y"); y finalmente " $p\land q$ y $q\land r$ implica $p\vdash r$ " (trivial)

En particular, a partir de esto se puede demostrar $\neg\neg\neg p \vdash \neg p$ de la siguiente manera : $p\land \neg p\vdash \bot$ (definición de $\neg$ y modus ponens débil) así $p\vdash \neg\neg p$ (introducción de la implicación), así $\neg\neg\neg p\land p \vdash \neg\neg\neg p \land \neg\neg p$ . Además $\neg\neg\neg p \land \neg\neg p\vdash \bot$ (definición de $\neg$ ) por lo que $\neg\neg\neg p\land p \vdash \bot$ (transitividad), lo que da como resultado $\neg\neg\neg p \vdash \neg p$ (introducción de la implicación)

Esto da lugar a la famosa ecuación : $\mathrm{Anh}^3 = \mathrm{Anh}$ ( $\mathrm{Anh}$ es el aniquilador de un ideal). Por supuesto, no ganamos prácticamente nada con la prueba anterior en comparación con la prueba teórica de anillos habitual, pero la cuestión es que si ya conocemos la lógica que satisfacen estos anillos y conocemos algunas de sus propiedades básicas (como $\neg\neg\neg p\vdash \neg p$ ) entonces se puede aplicar a los anillos y obtener esta ecuación: en otras palabras, esta ecuación se deduce de cosas formales (nótese que todas las reglas de deducción que he utilizado son derivables de la lógica intuicionista habitual)

Se pueden estudiar estas lógicas que surgen en los anillos: en particular se pueden dar caracterizaciones de cuando esta lógica contiene la lógica intuicionista, la lógica clásica. Un punto interesante es que tenemos la posibilidad de tener dos "y" lo que da la posibilidad de interpretar la lógica lineal (o de hecho la lógica afín)

Me he alejado un poco de los espacios vectoriales, pero la cuestión es que podemos estudiar interpretaciones de la lógica en estructuras algebraicas, y ver qué propiedades de dichas estructuras algebraicas son "puramente formales" en cierto sentido.

Answer 4

Desde $U \subset V^{\bot} \leftrightarrow V \subset U^{\bot}$ existe una conexión de Galois derecha (la terminología varía) entre $^\bot$ y a sí mismo. Del mismo modo, ya que $A \vdash B \rightarrow C$ si y sólo si $B \vdash A \rightarrow C$ existe una conexión de Galois correcta entre $\_ \rightarrow C$ y a sí mismo. En particular, existe una conexión de Galois correcta entre $\_ \rightarrow \bot$ y ella misma; es decir, existe una conexión de Galois correcta entre $\neg$ y a sí mismo. Obsérvese que esta conexión de Galois es decreciente (en otra terminología, de orden inverso o antitono). Más famosa en lógica es la conexión de Galois propia (creciente) entre $\_ \wedge B$ y $B \rightarrow \_$ . Obsérvese que en la lógica clásica también existe una conexión de Galois izquierda entre $\neg$ y a sí mismo. Es decir, en la lógica clásica, $\neg A \vdash B$ si y sólo si $\neg B \vdash A$ .

Las reglas que das se desprenden en su mayor parte de hechos sencillos sobre las conexiones de la derecha-Galois. La excepción es la primera regla que das para la negación. La regla que pareces buscar a partir de las reglas de Galois derecho es $p \vdash q$ implica $\neg q \vdash \neg p$ .