Ist First Order Logic (FOL) die einzige grundlegende Logik?

Ist First Order Logic (FOL) die einzige grundlegende Logik?

Kurze Antwort

Nein . Es ist nur die beliebteste Logik unter Mathematikern und Philosophen, hauptsächlich aus historischen und kulturellen Gründen.

Lange Antwort

Da Sie eine lange Frage geschrieben haben, hier ist eine lange Antwort :-)

Ursprünglich schlug Frege in seinen Grundlagen der Arithmetik (1884) eine Form der Logik zweiter Ordnung als Grundlage der Mathematik vor. Diese Grundlage kam aus der Mode, nachdem Russell bekanntermaßen einen Widerspruch in diesem System gefunden hatte (Sie können alles darüber auf SEP lesen ).

Seitdem haben nur sehr wenige Philosophen und Mathematiker die Wiederbelebung der Logik zweiter Ordnung als Grundlage der Mathematik argumentiert. Der einzige bekannte von dreien: Jouko Väänänen, Stewart Shapiro und George Boolos. Stewart Shapiro hat ein Buch darüber: Foundations without Foundationalism: A Case for Second-order Logic (2000) .

SOL ist aber hässlich. Es hat kein vollständiges Axiomensystem für seine Standardsemantik; die einzigen vollständigen Kalküle sind für Nicht-Standard-Modelle (siehe Henkin (1950) ). Außerdem versagt der Kompaktheitssatz für die übliche Semantik von SOL; Die Modelltheorie für FOL kann im Allgemeinen als verhaltener angesehen werden. Väänänen (2001) hat eine schöne Zusammenfassung der Eigenschaften der Logik zweiter Ordnung. Während das Löwenheim-Skolem-Theorem für die Standard-Semantik von SOL fehlschlägt, gilt es für Henkins Nicht-Standard-Semantik. Väänänen argumentiert: "Wenn die Logik zweiter Ordnung als unsere primitive Logik ausgelegt wird, kann man nicht sagen, ob sie eine vollständige Semantik oder eine Henkin-Semantik hat, und wir können auch nicht sinnvoll sagen, ob sie kategorisch ℕ und ℝ axiomatisiert."

Abraham Robinson stimmte in diesem Punkt wahrscheinlich mit Väänänen überein. In seinem Opus Nonstandard Analysis (1960), Kapitel 2, präsentiert er Henkins Semantik für Logik höherer Ordnung. Er fährt fort, Kompaktheit, Löwenheim-Skolem und den Satz von Łoś zu beweisen. Robinson schenkt der Klasse der Standardmodelle höherer Ordnung (die er als "Vollmodelle" bezeichnet) kaum Aufmerksamkeit. Dass Robinson Henkins nicht standardmäßige Semantik annehmen würde, macht natürlich Sinn. Der ganze Biss der Nichtstandardanalyse kommt von der Tatsache, dass ℝ nicht kategorisch ist und der Satz von Łoś funktioniert .

Abgesehen von Robinson (und vielleicht Väänänen) betrachtet niemand Henkins Semantik wirklich als Grundlage. Niemand, der an Grundlagen arbeitet, interessiert sich auch sonderlich für Systeme, die nicht axiomatisierbar sind. Der springende Punkt in Harvey Friedmans Forschungsprogramm zur Umkehrmathematik ist, dass wir verschiedene axiomatische Systeme haben und wir über ihre Beweiskraft argumentieren können.

Natürlich ist die Idee, dass es FOL vs. SOL für die Grundlagen der Mathematik gibt, sowieso eine falsche Dichotomie.

Warum also wird FOL ausnahmslos als zugrunde liegende Logik gewählt, auf deren Spitze die festgelegten theoretischen Axiome in jeder potenziell grundlegenden Formalisierung der Mathematik aufgestellt werden?

Es ist nicht ausnahmslos gewählt . Ihre Vorrangstellung in Mathematik und Philosophie verdankt sie ihrem frühen Erfolg und ihrer schnellen Entwicklung im Vergleich zur Konkurrenz.

Die mathematisch-philosophische Grundlagenforschung der Mathematik spaltete sich nach der Verwerfung von Freges Grundlagen in mehrere Richtungen . Sie können darüber in Heijenoorts Anthologie From Frege to Gödel: A Source Book in Mathematical Logic (1999) nachlesen :

• Die Logiker erster Ordnung : die frühe, große Mehrheit. Dazu gehören Guisseppe Peano, CS Pierce, David Hilbert, George Cantor, Richard Dedekind, Skolem, Löwenheim, Zermelo, Fraenkel, Herbrand, die Bourbaki-Jungs, Quine, Tarski, (früher) Wittgenstein usw.
• The Many Sorted Logicians : Russell, Whitehead und (manchmal) Gödel.
• Die Väter der Berechnung : Moses Schoenfinkle, Alonzo Church und seine Schüler.
• Die Konstruktivisten : Kronecker, Kolmogorov und Brouwer und seine Schüler.

Es sollte darauf hingewiesen werden, dass Peano, Pierce und Hilbert alle die Logik erster Ordnung ungefähr unabhängig voneinander entwickelt haben; dies verleiht der Idee Glaubwürdigkeit, dass FOL eine natürliche Grundlage für die Mathematik ist.

Während die anderen Ansätze nicht verschwunden sind, hatten sie alle anfänglich Schwierigkeiten.

Die Typentheorie war schlecht entwickelt: Jeder weiß, wie legendär die Principia Mathematica von Russell und Whitehead ist. Russell kämpfte lange, bevor er verzweigte Typen entwickelte , die herausfordernd und schwer zu handhaben waren. Letztlich zeigten Leon Chwistek und Frank Ramsey, dass das System vereinfacht werden kann, was in den 1920er Jahren zur Theorie der einfachen Typen führte. Tragischerweise starb Ramsey sehr jung, so dass alle Beiträge, die er möglicherweise geleistet hatte, gekürzt wurden. Darüber hinaus gab Russell die Logik auf, nachdem er die Principia geschrieben hatte, und sein Schüler Wittgenstein bemühte sich nicht, sie weiterzuentwickeln.

Auch die „Väter des Rechnens“ standen vor Herausforderungen, allerdings auch später als FOL und ZF-Mengenlehre. Nach der Veröffentlichung von On The Building Blocks of Mathematical Logic im Jahr 1924 fand sich Moses Schönfinkel hinter dem Eisernen Vorhang gefangen und nie wieder veröffentlicht. Seine Arbeit wurde später von Church aufgegriffen, die sie mit seinem λ-Kalkül verband. Der λ-Kalkül war zwar aussagekräftiger als FOL, aber nie wirklich als Grundlage für die Mathematik geeignet. Eine Reihe grundlegender Systeme, die auf dem λ-Kalkül aufbauen, wurden in den 30er Jahren von Church und anderen vorgeschlagen. Das populärste dieser Systeme erwies sich als widersprüchlich durch das, was heute als Curry-Paradoxon bekannt ist (siehe Curry (1941) ).

Schließlich hatten Konstruktivismus und Intuitionismus ihre eigenen Probleme. Der offensichtliche Fehler des Konstruktivismus ist zu restriktiv. Ein Mathematiker wird einen konstruktiven Beweis immer akzeptieren, aber es ist einfacher, einen nicht-konstruktiven Beweis zu finden, der auch allgemein akzeptabel ist. Ein weiteres Problem ist die Logik: Intuitionistische Logik und Arithmetik wurden erst Ende der 1920er Jahre durch Heyting axiomatisiert. Auch die adäquate Semantik der intuitionistischen Prädikatenlogik (IPK) blieb lange Zeit ein offenes Problem. Ein schwacher Vollständigkeitsbeweis wurde von Kreisel in den 1950er Jahren unter Verwendung von Brouwers beabsichtigter Semantik (dh Auswahlsequenzen ) geliefert. Kripke gab später einen starken Vollständigkeitsbeweisfür IPC in den 1960er Jahren unter Verwendung von Kripke-Strukturen. Die „Heilzeit“ der intuitionistischen Modelltheorie in den 50er und 60er Jahren kam 30 Jahre zu spät, um Auswirkungen auf die Grundlagen der Mathematik zu haben.

Während konkurrierende Stiftungen kämpften, gewann FOL/ZF schließlich die Herzen der Mainstream-Mathematiker und -Philosophen. Moderne Grundlagenmathematiker erforschen meist die Feinabstimmung der bestehenden Grundlage. Nachdem Paul Cohen die Unabhängigkeit der Kontinuumshypothese ( 1963 ) demonstriert hatte, begannen Mathematiker, die Unabhängigkeit verschiedener Aussagen in ZF und bestimmten Erweiterungen zu untersuchen. Eine wichtige axiomatische Erweiterung ist Grothendiecks Universumsaxiom , das der Existenz eines stark unzugänglichen Kardinals entspricht. Dieses Axiom ist in der algebraischen Geometrie weit verbreitet und wurde von Wiles in seinem Beweis von Fermats letztem Satz verwendet (obwohl hierHarvey Friedman argumentiert, dass die Verwendung des Axioms nicht wirklich wesentlich ist). Apropos Harvey Friedman, ein weiteres wichtiges Grundlagenforschungsprogramm ist die umgekehrte Mathematik , die die Beweiskraft von Systemen untersucht, die die Peano-Arithmetik erweitern, aber schwächer als ZF sind.

Die Modelltheorie erster Ordnung hat sich ebenfalls entwickelt. Ein alter Triumph der Modelltheorie ist Hrushovskis modelltheoretischer Beweis der Lang-Vermutung ( 1998 ). Trotz der Kategorisierung von ℕ und ℝ in SOL haben sich seit den 50er Jahren nur wenige Mathematiker mit Modelltheorie zweiter Ordnung beschäftigt. Auch in FOL gibt es Kategorizitätsergebnisse: Zum Beispiel ist (ℚ,<) in FOL ω-kategorisch.

Und in der Philosophie hat kein Philosoph FOL mehr evangelisiert als Quine. Ich würde sagen, Quines Überlegenheit ist wahrscheinlich der Grund, warum Philosophen nur FOL und ZF kennen und nichts anderes wissen.

Während Mainstream-Mathematiker und Philosophen sie ignorierten, konsolidierten sich die anderen Grundlagenforschungsprogramme und blühten schließlich auf.

Nachdem die Verwendung des λ-Kalküls als Grundlage gescheitert war, wandten sich Church und viele seiner Schüler der Verwendung einfacher Typen zu. Was dabei herauskam, kombinierte Russells Forschungsprogramm mit Churchs Programm.

Eine Weiterentwicklung war eine unerwartete, nicht niederländische Interpretation der intuitionistischen Logik: Die konstruierbaren Typen im einfach typisierten λ-Kalkül entsprechen genau der aussagenlogischen intuitionistischen Logik. Dies ist die sogenannte Curry-Howard-Korrespondenz .

Die Curry-Howard-Korrespondenz inspirierte schließlich Per Martin-Löf, Anfang der 70er Jahre die Intuitionistische Typentheorie als neuartige alternative Grundlage für die Mathematik zu erfinden. Die ursprüngliche Formulierung litt unter einem Defekt, der als Girards Paradoxon bekannt ist, obwohl das System zu retten war und Martin-Löf es nicht aufgab.

Studenten der Informatik ist allgemein bekannt, dass der λ-Kalkül John McCarthy und Steve Russell zur Erfindung inspirierte LISP. Ähnliches geschah Anfang der 70er Jahre mit dem einfach typisierten λ-Kalkül. Dana Scott, eine ehemalige Studentin der Alonzo-Kirche, erfand Ende der 60er Jahre The Logic for Computable Functions , um über die Denotationssemantik von typisierten funktionalen Programmen nachzudenken. 1973 implementierten Robin Milner und Co. LCFden ersten Computerbeweisassistenten. Dies geschah nach der Entwicklung der ersten einfach typisierten funktionalen Programmiersprache ML("MetaLanguage"), in der sie geschrieben wurde.

Seitdem arbeitet die Nicht-FOL/ZF-Grundlagenforschung weitgehend mit der Informatik-Community zusammen.

Ein Beispiel ist HOL oder „Higher Order Logic“, grob nach Churchs einfach typisiertem Lambda-Kalkül ( 1940 ) modelliert. Nach einer Reihe von Überarbeitungen veröffentlichte Mike Gordon HOL88, das für die Hardware-Verifizierung vorgesehen ist. Wie Gordon in seiner kurzen Geschichte zu diesem Thema zugibt, hackte sein Code Teile von LCF, wenn es praktisch war, und war eher ad hoc ( 1996 ). HOL wurde später von John Harrison und Konrad Slind zu HOL-Light geschliffen ; HOL-Light hat 9 elementare Regeln, die vage wie die Gleichungslogik aussehen , und drei Axiome (das Axiom der Unendlichkeit , das Axiom der Wahl unter Verwendung von Hilberts ε und das Leibniz-Gesetz ).

Eine weitere Erweiterung ist Isabelle/HOL , die das Typsystem von HOL konservativ um "context" erweitert. Noch ein weiteres System ist Homeiers HOL-Omega , das das Typensystem noch weiter konservativ erweitert.

Eine weitere Entwicklung ist NuPRL von der Cornell University, das die intuitionistische Typentheorie von Martin-Löf implementiert. Agda ist ähnlich. Ein verwandtes System aus INRIA ist Coq , das den Konstruktionskalkül von Thierry Coquand implementiert, der die intuitionistische Typentheorie erweitert.

Die Entwicklung neuer Systeme hat sich in den letzten zehn Jahren verlangsamt, aber sie hat nicht aufgehört. Die wenigen FOL/ZF-Systeme (nämlich Isabelle/ZF und Mizar ) sind vergleichsweise inaktiv.

Ich würde meine Position so zusammenfassen: Zu sagen, dass FOL immer als zugrunde liegende Logik gewählt wird, ist so, als würde man sagen, dass Windows immer als zugrunde liegende Plattform für PC-Spiele gewählt wird .

In beiden Fällen ist es eine kulturelle Sache.

Jemand sollte darauf hinweisen, dass die Semantik, die Mathematiker tatsächlich im Alltag verwenden, trotz aller Sorgen um die Grundlagen immer noch Logik zweiter Ordnung oder ein Äquivalent ist.

Wir erlauben im Allgemeinen eine Bezugsebene für Sätze von Sätzen und gehen implizit davon aus, dass „Currying“ dies völlig ausreichend macht. Und wir schwächen die Logik nicht, um den Widerspruch zu vermeiden, es sei denn, wir werden von einem Logiker oder einem Paradox in eine Ecke gefangen.

Selbst Menschen, die große Teile der Standardlogik der Mathematik ablehnen, indem sie ein gewisses Maß an „Konstruktivität“ fordern, reduzieren ihr Denken nicht auf Manipulationen erster Ordnung, sondern kontrollieren stattdessen den Zugang zu Negations- und Universalitätsansprüchen, die nicht auf einer bestimmten Perspektive beruhen.

Der Fokus auf die Logik erster Ordnung als Grundlage von allem scheint die Logik von der eigentlichen mathematischen Praxis abgelenkt zu haben und im Grunde die Suche nach einer verwendbaren Standardlogik innerhalb der Logik zweiter Ordnung gestoppt zu haben, mit der Annahme, dass sie alle zum Opfer fallen werden die erhöhte Version des Satzes von Gödel. Dies ist keine ausgemachte Sache.

Ich habe gelegentlich Arbeiten zu Definitionen von „Begründetheit“ (à la Kategorietheorie als alternative Mengenlehre) und andere Beschränkungen der Selbstreferenz als Grundlage für eine Form der Logik gesehen, die mehr auf der Grundlage von Konsistenz arbeitet, indem sie auflöst oder konvergiert Schleifen als auf einer positivistischen Basis, die eine absolute Grundlage erfordert, aber langsam voranzukommen scheint und nicht gelehrt wird.

Stiftungen hat Ziele:

1. Eine Herangehensweise an die Mathematik zu präsentieren, auf die wir uns verlassen können, ist konsequent
2. Sprache und Methodik zu präsentieren, mit der wir tatsächlich Mathematik machen können

Diese Ziele sind im Grunde diametral entgegengesetzt. Die einfachste Methode, um das erste Ziel zu erreichen, besteht im Grunde darin, einen sehr minimalen Satz von Werkzeugen zu haben, um es möglich zu machen, über ihre Korrektheit zu urteilen. Das zweite Ziel ermutigt uns jedoch nachdrücklich, viele, viele verschiedene Werkzeuge zum Konstruieren, Manipulieren und Beweisen von Dingen einzusetzen.

Eine sehr schöne Lösung für dieses Problem besteht darin, Fundamente einfach in zwei Schichten aufzuteilen: Die erste Schicht ist eine sehr minimale, von deren Richtigkeit wir überzeugt sind, und damit bauen wir die zweite Schicht auf, die alle praktischen Funktionen enthält, die wir verwenden möchten um Mathematik zu machen.

Das sehen Sie heute; Logik erster Ordnung ist eine übliche Wahl für die erste Schicht und dann eine Form der Mengenlehre als zweite Schicht.

Beachten Sie übrigens, dass die Logik höherer Ordnung selbst eine Form der Mengenlehre ist.

Beachten Sie übrigens, dass Sie, sobald Sie die Grundlagen geschaffen haben, immer noch eine Theorie der formalen Logik auf diesen Grundlagen entwickeln möchten; es ist diese Formulierung der Logik, nicht was auch immer an der Basis Ihrer Grundlagen erscheint, die am relevantesten für das tatsächliche Praktizieren von Mathematik ist.