Lógica ecuacional

La lógica ecuacional de primer orden consiste en términos sin cuantificadores de la lógica ordinaria de primer orden , con la igualdad como único símbolo de predicado . La teoría de modelos de esta lógica fue desarrollada en álgebra universal por Birkhoff , Grätzer y Cohn . Posteriormente , Lawvere la convirtió en una rama de la teoría de categorías ("teorías algebraicas"). ^{[ 1 ]}

Los términos de la lógica ecuacional se construyen a partir de variables y constantes utilizando símbolos de función (u operaciones).

Estas son las cuatro reglas de inferencia de la lógica.${\textstyle P[x:=E]}$denota la sustitución textual de la expresión${\textstyle E}$para variable${\textstyle x}$en expresión${\textstyle P}$. Próximo,${\textstyle b=c}$denota igualdad, para${\textstyle b}$y${\textstyle c}$del mismo tipo, mientras que${\textstyle b\equiv c}$, o equivalencia, se define únicamente para${\textstyle b}$y${\textstyle c}$de tipo booleano . Para${\textstyle b}$y${\textstyle c}$de tipo booleano,${\textstyle b=c}$y${\textstyle b\equiv c}$tienen el mismo significado.

^{[ 2 ]}

Explicamos cómo se utilizan las cuatro reglas de inferencia en las demostraciones, utilizando la demostración de${\textstyle \lnot p\equiv p\equiv \bot }$Los símbolos lógicos${\textstyle \top }$y${\textstyle \bot }$indican "verdadero" y "falso", respectivamente, y${\textstyle \lnot }$indica " no ". Los números de los teoremas se refieren a teoremas de Un enfoque lógico de las matemáticas discretas . ^{[ 2 ]}

$${\displaystyle {\begin{array}{lcl}(0)&&\lnot p\equiv p\equiv \bot \\(1)&=&\quad \left\langle \;(3.9),\;\lnot (p\equiv q)\equiv \lnot p\equiv q,\;{\text{con}}\ q:=p\;\right\rangle \\(2)&&\lnot (p\equiv p)\equiv \bot \\(3)&=&\quad \left\langle \;{\text{Identidad de}}\ \equiv (3.9),\;{\text{con}}\ q:=p\;\right\rangle \\(4)&&\lnot \top \equiv \bot &(3.8)\end{array}}}$$

Primero, líneas${\textstyle (0)}$–${\textstyle (2)}$mostrar un uso de la regla de inferencia de Leibniz:

$${\displaystyle (0)=(2)}$$

es la conclusión de Leibniz y su premisa${\textstyle \lnot (p\equiv p)\equiv \lnot p\equiv p}$se da en línea${\textstyle (1)}$. Del mismo modo, la igualdad en las líneas${\textstyle (2)}$–${\textstyle (4)}$se fundamentan utilizando a Leibniz.

La "pista" en línea${\textstyle (1)}$Se supone que debe dar una premisa de Leibniz, mostrando qué sustitución de iguales por iguales se está utilizando. Esta premisa es el teorema${\textstyle (3.9)}$con la sustitución${\textstyle p:=q}$, es decir

$${\displaystyle (\lnot (p\equiv q)\equiv \lnot p\equiv q)[p:=q]}$$

Esto muestra cómo se utiliza la regla de inferencia Sustitución dentro de las sugerencias.

De${\textstyle (0)=(2)}$y${\textstyle (2)=(4)}$, concluimos por regla de inferencia Transitividad que${\textstyle (0)=(4)}$Esto muestra cómo se utiliza la transitividad.

Finalmente, observe esa línea${\textstyle (4)}$,${\textstyle \lnot \top \equiv \bot }$, es un teorema, como lo indica la pista a su derecha. Por lo tanto, por la regla de inferencia de Ecuanimidad, concluimos que la línea${\textstyle (0)}$También es un teorema. Y${\textstyle (0)}$eso es lo que queríamos demostrar. ^{[ 2 ]}

• Teoría de la igualdad pura

• Sakharov, Alex. "Lógica ecuacional". De MathWorld, un recurso web de Wolfram, creado por Eric W. Weisstein.