Dieser Wikipedia-Artikel über kombinatorische Logik besagt, dass kombinatorische Logik, Lambda-Logik und Turing-Maschinen rechnerisch gleichwertig sind, aber dass beide die Ausdruckskraft der Logik erster Ordnung übersteigen.
Inwiefern übersteigen sie die Ausdruckskraft der Logik erster Stufe?
Haben wir Vollständigkeits- und Korrektheitstheoreme für Lambda/kombinatorische Logik?
1: Inwiefern übersteigen sie die Ausdruckskraft der Logik erster Ordnung?
Ich weiß nicht, ob der untypisierte Lambda-Kalkül und die Logik erster Ordnung direkt verglichen werden können, aber die Simple Type Theory ist ein typisierter Lambda-Kalkül und gleichzeitig eine Formalisierung der Logik höherer Ordnung. Laut Wikipedia:
Der Lambda-Kalkül wurde in den 1930er Jahren vom Mathematiker Alonzo Church eingeführt [...]. Das ursprüngliche System erwies sich 1935 als logisch inkonsistent [...] 1936 isolierte und veröffentlichte Church nur den Teil, der für die Berechnung relevant ist, was heute als untypisierter Lambda-Kalkül bezeichnet wird. 1940 führte er auch ein rechnerisch schwächeres, aber logisch konsistentes System ein, das als einfach typisierter Lambda-Kalkül bekannt ist.
Wie ich aus "Die sieben Tugenden der einfachen Typentheorie" gelernt habe, ist das häufig verwendete Beweissystem für die einfache Typentheorie gleichbedeutend mit der Mac-Lane-Mengentheorie . Diese wiederum gilt als „gutes Modell“ der „prädikativen Mathematik“. Es gibt Gerüchte , dass Randall Holmes einen Beweis dafür hat, dass auch Quines New Foundations mit der Mengentheorie von Mac Lane übereinstimmen.
2: Haben wir Vollständigkeits- und Korrektheitstheoreme für Lambda/kombinatorische Logik?
Das Papier, das die Henkin-Semantik für die Logik höherer Ordnung einführte, behandelte explizit die einfache Typentheorie und enthielt das Theorem von Henkin. Vollständigkeit und Korrektheit ähneln also in gewissem Sinne der Logik erster Ordnung. Äquikonsistenz mit der Mac-Lane-Mengentheorie bedeutet jedoch, dass die Konsistenz der einfachen Typentheorie nicht im absoluten Sinne bewiesen werden kann.
Der Artikel sagt tatsächlich, dass sie "typischerweise" die Macht der Logik erster Ordnung übersteigen. Die Logik erster Ordnung über einer Sprache der Arithmetik, die Addition und Multiplikation beinhaltet, ist Turing vollständig, da Sie jede rekursive Funktion arithmetisch definieren können:
Eine andere Möglichkeit, den untypisierten Lambda-Kalkül und die Logik erster Ordnung zu vergleichen, besteht darin, zu überlegen, was Sie mit Funktionen erster Ordnung im Vergleich zu Funktionen höherer Ordnung im Vergleich zu Funktionen im untypisierten Lambda-Kalkül erstellen können, die im Wesentlichen unendlicher Ordnung sind.
Ich möchte hier keinen Anstoß erregen. Ich kann nur als Laie kommentieren, der nur ein Laienverständnis von Universitätsmathematik hat.
Es ist bemerkenswert, dass nicht jeder hier glaubt, dass die Logik erster Ordnung nicht Turing-vollständig ist. Eine Turing-Maschine ist eine endliche Zustandsmaschine mit einem unendlichen Band. Es ist nur eine elementare (dh machbare) Computercodierübung, dies zu implementieren.
Für ein Turing-Komplettsystem wird nur eine winzige Teilmenge von Dartmouth Basic oder Applesoft Basic benötigt. In den letzten Jahren hat Terry Tao (möglicherweise auf dieser Seite) gefragt, ob es eine Gruppe gibt, die komplett ist. Vielleicht könnten wir eine Übung zum Ankreuzen von Kästchen machen und feststellen, dass jedes der Objekte, denen wir im Mathematik-Einführungskurs an der Universität begegnen, alleine ausreicht, um ein vollständiges Turing-System zu bauen.
Der Wikipedia-Eintrag zur Logik erster Ordnung ist ziemlich detailliert (viele hundert Zeilen).
Darin heißt es: Die Logik erster Ordnung ist in der Lage, viele einfache Quantorenkonstruktionen in natürlicher Sprache zu formalisieren, wie zum Beispiel "jede Person, die in Perth lebt, lebt in Australien". Aber es gibt viele kompliziertere Merkmale natürlicher Sprache, die nicht in (einfach sortierter) Logik erster Ordnung ausgedrückt werden können. „Jedes logische System, das als Instrument zur Analyse natürlicher Sprache geeignet ist, benötigt eine viel reichhaltigere Struktur als die Prädikatenlogik erster Ordnung“ (Gamut 1991, S. 75).
Der Wikipedia-Artikel sagt auch:
Gewöhnliche Interpretationen erster Ordnung haben einen einzigen Diskursbereich, über den sich alle Quantifizierer erstrecken. Die vielsortierte Logik erster Ordnung ermöglicht es, dass Variablen unterschiedliche Sortierungen haben, die unterschiedliche Domänen haben. ... Wenn es in einer Theorie nur endlich viele Arten gibt, kann die vielsortierte Logik erster Ordnung auf die einfachsortierte Logik erster Ordnung reduziert werden. Man führt in die einfach sortierte Theorie ein unäres Prädikatssymbol für jede Sorte in der vielsortierten Theorie ein und fügt ein Axiom hinzu, das besagt, dass diese unären Prädikate den Bereich des Diskurses aufteilen.
Aus dem Obigen bin ich alles andere als überzeugt, dass die Logik erster Ordnung für eine vollständige Behandlung der natürlichen Sprache ungeeignet ist. Wenn wir der Turing-Doktrin folgen, sind wir nicht gezwungen zuzustimmen, dass wir eine vollständige Behandlung natürlicher Sprache mit jedem vollständigen Turing-System codieren können, das, wie ich aus dem Wikipedia-Artikel vermute, sicherlich Logik erster Ordnung enthält.
Ich werde den Gamut-Artikel weiterverfolgen, um Licht ins Dunkel zu bringen. Aber auf den ersten Blick ist der Gamut-Artikel falsch, weil er die Frage aufwirft - er besagt, dass Sie natürliche Sprache nicht in einem einfach sortierten Prädikatenkalkül ausdrücken können. Aber der Wikipedia-Artikel macht deutlich, dass dies keine Einschränkung sein muss - zumindest zeigt er, dass ein mehrfach sortierter Prädikatenkalkül in einem einfach sortierten Prädikatenkalkül codiert werden kann.
Kobold GEGANGEN
Trylks