Lógica ecuacional

La lógica ecuacional de primer orden consta de términos libres de cuantificadores de la lógica ordinaria de primer orden , con la igualdad como único símbolo de predicado . La teoría modelo de esta lógica fue desarrollada hasta convertirse en álgebra universal por Birkhoff , Grätzer y Cohn . Más tarde , 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).

Silogismo

Aquí están las cuatro reglas de inferencia de la lógica. denota sustitución textual de expresión por variable en expresión . A continuación, denota igualdad, para y del mismo tipo, mientras que , o equivalencia, se define solo para y de tipo booleano . For y de tipo booleano, y tienen el mismo significado. ${\textstyle P[x:=E]}$ ${\textstyle E}$ ${\textstyle x}$ ${\textstyle P}$ ${\textstyle b=c}$ ${\textstyle b}$ ${\textstyle c}$ ${\textstyle b\equiv c}$ ${\textstyle b}$ ${\textstyle c}$ ${\textstyle b}$ ${\textstyle c}$ ${\textstyle b=c}$ ${\textstyle b\equiv c}$

^[2]

Historia

La lógica ecuacional fue desarrollada a lo largo de los años (a principios de la década de 1980) por investigadores en el desarrollo formal de programas, que sentían la necesidad de un estilo eficaz de manipulación, de cálculo. Participaron personas como Roland Carl Backhouse , Edsger W. Dijkstra , Wim HJ Feijen, David Gries , Carel S. Scholten y Netty van Gasteren. Wim Feijen es responsable de detalles importantes del formato de prueba.

Los axiomas son similares a los utilizados por Dijkstra y Scholten en su monografía Cálculo de predicados y semántica de programas (Springer Verlag, 1990), pero nuestro orden de presentación es ligeramente diferente.

En su monografía, Dijkstra y Scholten utilizan las tres reglas de inferencia de Leibniz, Sustitución y Transitividad. Sin embargo, el sistema Dijkstra/Scholten no es una lógica, como usan la palabra los lógicos. Algunas de sus manipulaciones se basan en los significados de los términos involucrados y no en reglas de manipulación sintácticas claramente presentadas. El primer intento de convertirlo en una lógica real apareció en Un enfoque lógico de las matemáticas discretas , sin embargo, allí falta la regla de inferencia Ecuanimidad y la definición del teorema está distorsionada para explicarla. La introducción de Equanimity y su uso en el formato de prueba se debe a Gries y Schneider. Se utiliza, por ejemplo, en las pruebas de solidez y completitud, y aparece en la segunda edición de A Logical Approach to Discrete Math . ^[2]

Prueba

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

$${\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{with}}\ q:=p\;\right\rangle \\(2)&&\lnot (p\equiv p)\equiv \bot \\(3)&=&\quad \left\langle \;{\text{Identity of}}\ \equiv (3.9),\;{\text{with}}\ q:=p\;\right\rangle \\(4)&&\lnot \top \equiv \bot &(3.8)\end{array}}}$$

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

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

Es la conclusión de Leibniz, y su premisa se da en línea . De la misma manera, la igualdad en las rectas se fundamenta con Leibniz. ${\textstyle \lnot (p\equiv p)\equiv \lnot p\equiv p}$ ${\textstyle (1)}$ ${\textstyle (2)}$ ${\textstyle (4)}$

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

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

Esto muestra cómo se utiliza la regla de inferencia de sustitución en las sugerencias.

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

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

Ver también

• Teoría de la igualdad pura

Referencias

1. lógica ecuacional. (Dakota del Norte). Diccionario de informática gratuito en línea. Obtenido el 24 de octubre de 2011 del sitio web Dictionary.com: http://dictionary.reference.com/browse/equational+logic
2. Gries, D. (2010). Introducción a la lógica ecuacional. Obtenido de http://www.cs.cornell.edu/home/gries/Logic/Equational.html Archivado el 23 de septiembre de 2019 en Wayback Machine.

enlaces externos

• Sájarov, Alex. "Lógica Ecuacional". De MathWorld: un recurso web de Wolfram, creado por Eric W. Weisstein.