Gleichungslogik - Equational logic

Erster Ordnung equational Logik besteht aus quantifier -freien Bedingungen der gewöhnlichen Logik erster Ordnung , mit Gleichheit als einziges Prädikat Symbol . Die Modelltheorie dieser Logik wurde von Birkhoff , Grätzer und Cohn zur universellen Algebra entwickelt . Es wurde später von Lawvere ("algebraische Theorien") zu einem Zweig der Kategorietheorie gemacht .

Die Begriffe der Gleichungslogik werden aus Variablen und Konstanten unter Verwendung von Funktionssymbolen (oder Operationen) aufgebaut.

Syllogismus

Hier sind die vier Inferenzregeln der Logik. bezeichnet die Textsubstitution des Ausdrucks für eine Variable im Ausdruck . Als nächstes bezeichnet Gleichheit für und vom gleichen Typ, während oder Äquivalenz nur für und vom Typ Boolean definiert ist . Für und vom Typ boolean und haben die gleiche Bedeutung. ${\ 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}$

Auswechslung	Wenn es sich um einen Satz handelt, ist dies auch der Fall . ${\ textstyle P}$${\ textstyle P [x: = E]}$	$${\ displaystyle \ vdash P \ qquad \ rightarrow \ qquad \ vdash P [x: = E]}$$
Leibniz	Wenn es sich um einen Satz handelt, ist dies auch der Fall . ${\ textstyle P = Q}$${\ textstyle E [x: = P] = E [x: = Q]}$	$${\ displaystyle \ vdash P = Q \ qquad \ rightarrow \ qquad \ vdash E [x: = P] = E [x: = Q]}$$
Transitivität	Wenn und Theoreme sind, dann ist es so . ${\ textstyle P = Q}$${\ textstyle Q = R}$${\ textstyle P = R}$	$${\ displaystyle \ vdash P = Q, \; \ vdash Q = R \ qquad \ rightarrow \ qquad \ vdash P = R}$$
Gleichmut	Wenn und Theoreme sind, dann ist es so . ${\ textstyle P}$${\ textstyle P \ equiv Q}$${\ textstyle Q}$	$${\ displaystyle \ vdash P, \; \ vdash P \ equiv Q \ qquad \ rightarrow \ qquad \ vdash Q}$$

Geschichte

Die Gleichungslogik wurde im Laufe der Jahre (beginnend in den frühen 1980er Jahren) von Forschern in der formalen Entwicklung von Programmen entwickelt, die das Bedürfnis nach einem effektiven Manipulations- und Berechnungsstil verspürten. Beteiligt waren Personen wie Roland Carl Backhouse , Edsger W. Dijkstra , Wim HJ Feijen, David Gries , Carel S. Scholten und Netty van Gasteren. Wim Feijen ist für wichtige Details des Proofformats verantwortlich.

Die Axiome ähneln denen, die Dijkstra und Scholten in ihrer Monographie Prädikatenrechnung und Programmsemantik (Springer Verlag, 1990) verwenden, aber unsere Darstellungsreihenfolge unterscheidet sich geringfügig.

In ihrer Monographie verwenden Dijkstra und Scholten die drei Inferenzregeln Leibniz, Substitution und Transitivität. Das Dijkstra / Scholten-System ist jedoch keine Logik, da Logiker das Wort verwenden. Einige ihrer Manipulationen basieren auf der Bedeutung der beteiligten Begriffe und nicht auf klar dargestellten syntaktischen Manipulationsregeln. Der erste Versuch, daraus eine echte Logik zu machen, erschien in A Logical Approach to Discrete Math . Dort fehlt jedoch die Inferenzregel Gleichmut, und die Definition des Satzes ist verzerrt, um dies zu berücksichtigen. Die Einführung von Equanimity und seine Verwendung im Proof-Format ist Gries und Schneider zu verdanken. Es wird zum Beispiel in den Beweisen für Solidität und Vollständigkeit verwendet und wird in der zweiten Ausgabe von A Logical Approach to Discrete Math erscheinen .

Beweis

Wir erklären, wie die vier Inferenzregeln in Beweisen verwendet werden, indem wir den Beweis von verwenden . Die logischen Symbole und "wahr" bzw. "falsch" und "nicht". Die Theoremnummern beziehen sich auf Theoreme eines logischen Ansatzes zur diskreten Mathematik . ${\ textstyle \ lnot p \ equiv p \ equiv \ bot}$ ${\ textstyle \ top}$${\ textstyle \ bot}$${\ textstyle \ lnot}$

Erstens Linien - zeigen eine Verwendung der Inferenzregel Leibniz: ${\ textstyle (0)}$${\ textstyle (2)}$

ist die Schlussfolgerung von Leibniz, und seine Prämisse wird online gegeben . Ebenso wird die Gleichheit auf Linien - mit Leibniz begründet. ${\ textstyle \ lnot (p \ equiv p) \ equiv \ lnot p \ equiv p}$${\ textstyle (1)}$${\ textstyle (2)}$${\ textstyle (4)}$

Der "Hinweis" online soll eine Prämisse von Leibniz geben und zeigen, welche Substitution von Gleichheit für Gleichheit verwendet wird. Diese Prämisse ist Satz mit der Substitution , dh ${\ textstyle (1)}$${\ textstyle (3.9)}$${\ textstyle p: = q}$

Dies zeigt, wie die Inferenzregel Substitution innerhalb von Hinweisen verwendet wird.

Aus und schließen wir durch Inferenzregel Transitivität, dass . Dies zeigt, wie Transitivität verwendet wird. ${\ textstyle (0) = (2)}$${\ textstyle (2) = (4)}$${\ textstyle (0) = (4)}$

Schließlich ist zu beachten , dass Linie , ist ein Satz, wie sie durch den Hinweis auf den rechten angegeben. Aus der Inferenzregel Gleichmut schließen wir daher, dass die Linie auch ein Satz ist. Und das wollten wir beweisen. ${\ textstyle (4)}$${\ textstyle \ lnot \ top \ equiv \ bot}$${\ textstyle (0)}$${\ textstyle (0)}$

Verweise

Externe Links

• Sacharow, Alex. "Gleichungslogik." Aus MathWorld - Eine Wolfram-Webressource, erstellt von Eric W. Weisstein.