Wie wird die vollständige Semantik von SOL und HOL spezifiziert?

In Bezug auf diese Frage nach dem "fundamentalen" Charakter möglicher logischer Systeme wurde mir klar, dass ich nur ein intuitives (und daher unzureichendes) Verständnis dafür hatte, wie Logiken, die höher als FOL sind, die Art von Semantik, die das Beabsichtigte ausmacht, eindeutig spezifizieren können Interpretation ihrer Formalismen innerhalb der Formalismen selbst . Dies ist eine durchaus bedeutsame Frage, da die Fähigkeit eines automatisierten Argumentationssystems auf der Ebene der Objektsprache nur erkennen kann, was auf dieser Ebene im Formalismus selbst kodiert ist; daher scheiden solche Ansätze, die von der Konstruktion eines Modells auf der Metaebene ausgehen, a priori in dem hier beschriebenen Sinne aus.

Woran ich denke, sind Computersysteme, die mit der Logik argumentieren, wie zum Beispiel die HOL-basierten Beweisassistenten, wie Isabelle .

Wie wird also die beabsichtigte Semantik von SOL und HOL in einem Computersystem spezifiziert?

PS : Ich habe festgestellt, dass dieses Thema auf dieser Seite nicht wirklich neu ist und in anderen Fragen wie dieser angesprochen wurde .

Siehe auch den schönen HOL-Übersichtsartikel "The Seven Virtues of Simple Type Theory" von. W. Farmer ( imps.mcmaster.ca/doc/seven-virtues.pdf )

Antworten (3)

Aus Sicht der Ableitbarkeit und Syntax gibt es keine Unterscheidung zwischen vollständiger Semantik höherer Ordnung und Semantik erster Ordnung (Henkin). Dies ist in gewisser Weise der Grund dafür, dass es keinen Vollständigkeitssatz für die vollständige Semantik gibt - weil der Vollständigkeitssatz die Ableitbarkeit mit der Henkin-Semantik abgleicht und daher jede wirklich unterschiedliche Semantik nicht mit der Ableitbarkeit übereinstimmt. Syntaktische Dinge wie Beweisassistenten, die sich nur um Ableitbarkeit kümmern, stehen semantischen Fragen eher gleichgültig gegenüber.

Ich glaube, dass der Hauptvorteil der Verwendung von Logik höherer Ordnung in Beweisassistenten darin besteht, dass es einfacher ist, Sätze zu formalisieren, die in der gewöhnlichen Mathematik bewiesen wurden. Selbst wenn diese Theoreme beispielsweise in der Peano-Arithmetik formalisiert werden könnten, indem völlig neue Beweise erstellt werden, ist es oft einfacher, den vorhandenen Beweis so zu modifizieren, dass er in der Logik höherer Ordnung funktioniert.

Ich glaube, Sie haben verstanden, was ich frage. Im Wesentlichen stört mich das gesamte Konzept der "vollständigen Semantik". Wie kann es als "wohldefinierter" Begriff angesehen werden, wenn Logiken höherer Ordnung, die Kategorizität erfüllen, eine FO-Metatheorie mit mengentheoretischem Geschmack benötigen, um die Kategorizität dessen zu beweisen, was "sie sagen", mit ihrer "aussagekräftigeren Kraft" ? Woher kommt die "Expressivität", wenn Sie eine nicht-kategorische Mengenlehre verwendet haben, um sie zu beweisen? Wenn ich es richtig verstehe, scheint es fast das gleiche Problem zu sein wie bei der Betrachtung des "Standarduniversums" der Mengenlehre. Es ist nur Intuition? Was ist daran "formal"?
Richtig, Logik höherer Ordnung mit vollständiger Semantik ist in diesem Sinne nicht "formal", und das Problem hängt stark mit dem Problem des "Standardmodells" der Mengenlehre zusammen.
Vielen Dank. Diese Frage hing mit einer anderen zusammen, die ich im ersten Absatz zitiere; Die Bedeutung des Wortes "fundamental", die ich dort verwendet habe, ist mehr oder weniger dieselbe, die wir hier unter dem Adjektiv "formal" besprochen haben, mit Ausnahme der zusätzlichen Bedeutung, andere Logiken aus mathematischer Sicht "simulieren" zu können (z. B. können Fuzzy-Logiken in einer mathematischen FO-Theorie formalisiert werden, die die reellen Zahlen unterstützt, und die "Fuzzy-Zugehörigkeit" als ein geordnetes Paar definieren).
Ich würde mich sehr freuen, wenn Sie dort eine Antwort hinterlassen könnten , da ich keine der aktuellen zufriedenstellend fand.

Soweit mir bekannt ist, kümmern sich Computerbeweissysteme überhaupt nicht um Semantik . Ihre Aufgabe ist es, formale Beweise zu konstruieren und zu überprüfen, die den syntaktischen Regeln folgen, was eine gültige Ableitung ausmacht, und es ist dann Sache des menschlichen Benutzers, sich davon zu überzeugen, dass das formale System seiner Intuition über Semantik entspricht.

(Nun, einige Beweisassistenten kümmern sich manchmal um Semantik, etwa wenn sie berechnungsbasierte Entscheidungsverfahren für bestimmte Theorien wie geordnete Körper oder Presburger-Arithmetik enthalten. Aber dann - je nach Grad der Paranoia, die bei der Entwicklung verwendet wurde -- die Rolle dieser semantischen Unterteile besteht normalerweise nur darin, einen syntaktischen Beweis vorzuschlagen , der unabhängig verifiziert werden kann).

Was mich verwirrt, ist, dass, selbst wenn Ihr Argument absolut solide ist (Computer folgen nur syntaktischen Regeln und kümmern sich nicht um Semantik), zu folgen scheint, dass jede Logik höherer Ordnung als FOL notwendigerweise so berechnet wird, als wäre sie a viele sortierte FOL (dh erkennt zum Beispiel nicht, dass sich Variablen zweiter Ordnung über Teilmengen derselben Menge erstrecken , über die sich Variablen erster Ordnung erstrecken). Ich vermute jedoch, dass ich hier etwas übersehe.
@Mono: Es stimmt, dass der syntaktische Charakter der Beweisprüfung für HOL derselbe ist wie für ein vielsortiertes FOL. Was HOL auszeichnet, ist, dass es normalerweise spezifische logische Axiome und/oder Schlussregeln gibt, die sich mit Variablen höherer Ordnung befassen und beispielsweise sicherstellen, dass alles, was in einer expliziten Formel definierbar ist, auch berücksichtigt wird, wenn wir eine Variable höherer Ordnung von quantifizieren eine entsprechende Unterschrift. ...(Fortsetzung)
... Es steht uns frei, diese Sonderregeln als Teil der eigentlichen Theorie statt als Teil der Logik zu betrachten, und das Ergebnis wäre eine Theorie erster Ordnung, die dasselbe beweisen könnte - im Wesentlichen die ursprüngliche höhere Ordnung Theorie in eine (möglicherweise schwache) Version der Mengenlehre erster Ordnung eingebettet wäre. Die Position, dass alle Logik höherer Ordnung nur eine Abkürzung für Mengenlehre ist, wurde von Quine vertreten und hat sich weitgehend durchgesetzt, bis das Aufkommen praktischer Computerbeweissysteme deutlich machte, wie umständlich es ist, alles die ganze Zeit explizit auf die erste Ordnung zu reduzieren.
Beachten Sie auch, dass die Tatsache, dass die logischen Axiome für Variablen höherer Ordnung immer gleich sind (im Gegensatz dazu, wenn sie nur zufällige Teile der Fachtheorie wären), es für Entwickler von Beweisassistenten praktischer macht, allgemeine Strategien für Sonderfälle bereitzustellen ihre Verwendung, die es Benutzern ermöglichen, allgemeine Argumentationsmuster einfach zu spezifizieren.
Nun, ich nehme an, dass die Art von logischen Axiomen, auf die Sie sich beziehen, zum Beispiel die Verständnis- und Auswahlaxiome in SOL sind. Wenn ich verstanden habe, was Sie gesagt haben, können sowohl SOL als auch HOL effektiv mit einem geeigneten MS-FOL abgeglichen werden; könnte man also argumentieren, dass der einzige Unterschied zwischen diesen in der Art und Weise liegt, wie Variablen "höherer Ordnung" formalisiert werden (in ersterem durch Verständnis und in letzterem durch die richtige Signatur des vielsortierten Modells, dh die Sortierung der Funktionen und Relationen)? Es ist nur so, dass die FO-Formalisierung umständlich ist , und sonst nichts?
Außerdem: ist dann absolute Kategorizität (dh das behauptete Ergebnis für Theorien wie die SO-Formalisierung der Realzahlen unter ihrer vollen Semantik) keine sinnvolle Eigenschaft für Theorien, die auf irgendeiner logischen Ordnung beruhen , wenn wir (zum Beispiel) eine zusätzliche FO benötigen mengentheoretische, nicht kategoriale Meta-Sprache, um dafür ein Modell zu produzieren, das gerade dann in Bezug auf seine Axiome als eindeutig bewiesen werden kann? Oder was auf die gleiche Schlussfolgerung hinausläuft: Ist dann nicht nur die relative Kategorisierung eine bedeutungsvolle Eigenschaft einer formalen Theorie unter jeglicher Logik?
@Mono: Mir ist unklar, warum Sie plötzlich von Kategorizität und Modellen sprechen - das sind semantische Eigenschaften, die Proof-Checker / -Assistenten nicht interessieren. Alles, was sie interessiert, ist die Existenz eines gültigen Beweises in einem formalen System; ob das formale System einem semantischen Modellbegriff entspricht, ist nicht ihr Problem.
@Mono: Wie Henning denke ich, dass das eine separate Frage ist. Aber Sie haben in der Tat einen entscheidenden Punkt über die vollständige Semantik zweiter Ordnung gefunden, nämlich dass sie das Problem der Kategorizität einfach von der Objekttheorie in die Metatheorie verlagert. Die Wirkung der vollständigen Semantik besteht einfach darin, viele der Modelle, die in der Logik erster Ordnung berücksichtigt werden, von der Betrachtung auszuschließen. Wenn wir genug von ihnen ausschließen, könnten Theorien, die früher viele Modelle hatten, am Ende kategorisch sein oder überhaupt keine Modelle mehr haben! Aber das liegt nicht daran, dass sich die Theorie geändert hat, sondern daran, dass wir zu viele mögliche Modelle eliminiert haben.
@HenningMakholm: Ich habe das Thema Kategorizität und Modelle angesprochen, nur weil ich das ursprünglich fragen wollte (über die vollständige Semantik von Logiken höher als FOL). Wenn die HOL-Syntax immer in eine FO-Mengentheorie-Syntax "übersetzbar" ist - sei es einfach sortiert wie ZFC oder viele sortiert, wie die zweisortige Axiomatisierung von NBG -, dann ist das einzige, was HOL tut, eine Formalisierung der Deduktion Systeme weniger umständlich sind (auf Kosten des "Verschiebens der Linie" dessen, was philosophisch als Grenze zwischen Logik und Mathematik bezeichnet werden kann), sollten Sie dies Ihrer Antwort hinzufügen.
@CarlMummert: Das ganze Problem ist, dass ich über die Formalisierung der Semantik einer darin enthaltenen Logik spreche , nur weil es mir scheint, dass dies der einzig sinnvolle Weg ist, Kategorizität zu behaupten (wenn es möglich ist). In FOL ist das keine Metaebene, weil ihre Vollständigkeit die Übereinstimmung zwischen Nachweisbarkeit und Zufriedenheit durch (mindestens) ein Modell garantiert. Aber in Logiken höherer Ordnung bedeutet das Fehlen von Vollständigkeit, dass ihre Semantik notwendigerweise von einer Metaebene aus betrachtet werden muss; Daher muss, wie Sie sagen, die Eliminierung möglicher Modelle auf dieser Ebene durchgeführt werden.
Dann kann ich nicht einsehen, warum der Satz " SOL kann die Realzahlen als das einzige vollständige archimedische Feld bis zur Isomorphie definieren " formal als bedeutungsvoll angesehen werden kann. Wenn wir eine SO-Theorie aufschreiben und dann ein FO-deduktives System hinzufügen, das um Verständnis- und Auswahlaxiome erweitert ist, stellt sich heraus, dass sie an Ausdruckskraft verliert (und nach Lindströms Theorem FOL entspricht) ; aber wenn wir diese Axiome nicht einbeziehen, dann "ist es kategorisch" und "ausdrucksstärker", aber nur , wenn ein Modell von einer Metaebene und nicht "von selbst" bereitgestellt wird.

Ich möchte etwas klarstellen: HOL ist nicht nur multisortiertes FOL

Der Hauptunterschied besteht in der Expressivität der beiden Systeme. FOL kann keine transitive Schließung ausdrücken. Hier ist eine nette Notiz, die erklärt, warum. Andererseits kann HOL einen transitiven Abschluss ausdrücken. Hier ist der Quellcode der Implementierung von Isabelle/HOL, falls Sie interessiert sind.

BEARBEITEN 1 : Beachten Sie die Einschränkung in den Kommentaren: FOL, erweitert mit ZF oder Maschinen aus der Arithmetik, kann den transitiven Abschluss ausdrücken. Dass kein erweiterter Kalkül dies leisten kann, ist jedoch nicht die Behauptung, die ich hier aufstelle.

EDIT 2 : Ebenso ist es unangemessen, die Intuition aus Henkins Semantik für seine Logik höherer Ordnung blind zu nutzen, da ihre Anwendung auf computerbasierte HOLs nicht einfach ist. Zum einen basieren Beweisassistenten auf Churchs HOL, das älter als Henkins Arbeit ist und seine eigenen Besonderheiten hat. Die Semantik für das HOL der Kirche kann unter Verwendung von Anwendungsstrukturen gemäß Harvey Friedman (1975) und nachfolgenden Artikeln angegeben werden.

[Wie] ist die beabsichtigte Semantik von SOL und HOL in einem Computersystem spezifiziert?

Sie können die Semantik nicht wirklich angeben , wie andere angemerkt haben, aber es gibt verschiedene Möglichkeiten, dies zu tun X ∈ A wird in die Basissyntax geparst .

In Isabelle können Sie entweder Isabelle/ZF oder Isabelle/HOL laden. Je nachdem welches System Sie laden, X ∈ A wird unterschiedlich interpretiert.

Bei Isabelle/ZF ist es die Bedeutung, die Sie im Mengentheorieunterricht gelernt haben: ∈ ist eine binäre Relation in FOL und erfüllt die verschiedenen Axiome der Mengenlehre.

In Isabelle/HOL ist S :: 'x set(dh " Sist eine Menge von Objekten des Typs 'x") wirklich nur ein Wrapper für ein Objekt des Typs f :: 'x -> bool(dh " fist eine Indikatorfunktion , die 'xzu True/False führt"). Set Comprehension und Membership werden effektiv durch die Äquivalenz definiert A ∈ { X   |   P ( X ) } ⟺ P ( A ) . Du kannst darüber in der Quelle von Isabelle/HOL lesen, wenn du auf so etwas stehst.

Sowohl bei Isabelle/ZF als auch bei Isabelle/HOL die bekannte Syntax { X ∈ S   |   ϕ ( X ) } wird auch als syntaktischer Zucker interpretiert. In beiden Fällen ist der Parser dafür verantwortlich, die erweiterte Syntax in die Basissyntax zu kompilieren; und wie es gemacht wird, unterscheidet sich je nach Grundlage.

Obwohl Computerbeweisassistenten im Allgemeinen nicht daran gewöhnt sind, über ihre eigene Semantik nachzudenken, gibt es schließlich eine Ausnahme. John Harrison hat hier zwei relative Konsistenzbeweise von HOL-Light innerhalb von HOL-Light entwickelt .

Er demonstriert zunächst, wie man ein vollständiges Modell von HOL-Light ohne das Axiom der Unendlichkeit in HOL-Light konstruiert. Er zeigt dann, wie man ein vollständiges Modell von HOL-Light in HOL-Light erweitert mit einem stark unzugänglichen Kardinal konstruiert.

Die Behauptung "FOL kann keine transitive Schließung ausdrücken" ist etwas vage. ZFC kann sicherlich die transitive Schließung einer Beziehung definieren und ist eine Theorie erster Ordnung. Alles, was in HOL ausgedrückt werden kann , kann durch genau denselben Satz in FOL ausgedrückt werden. Der einzige Unterschied liegt in der Semantik – aber HOL hat mehrere Semantiken, von denen die schwächste die gleiche Stärke wie FOL hat. Alles, was Isabelle tut, ist mit dieser Semantik kompatibel; Isabelle kann nicht sagen, welche Semantik ich verwende, um die Ausgabe zu interpretieren. Wenn ich die Henkin-Semantik verwende, hat Isabelle die gleichen semantischen Einschränkungen wie FOL.
@Carl Mummert: Ich denke, ich sollte unterscheiden. Während Sie in ZF die transitive Schließung einer Beziehung zwischen Mengen ausdrücken können, kann es die Schließung logischer Beziehungen wie at nicht ausdrücken ∈ ; FOL kann das nicht. Auf der anderen Seite hat Isabelle/HOL dieses Problem nicht. Ebenso kodiert Isabelle/HOL nicht nur Henkins Kalkül höherer Ordnung; es enthält auch Erweiterungen wie das Axiom der Wahl. Isabelle/HOL kann in ZFC eingebettet werden, aber das ist nicht dasselbe wie in FOL-Vereinfacher (wie es Henkins Kalkül höherer Ordnung kann).
Henkins Methode arbeitet mit einer willkürlichen Auswahl und hinzugefügten Verständnisaxiomen; Tatsächlich werden diese typischerweise in der Logik zweiter Ordnung verwendet, sogar mit Henkin-Semantik. Darüber hinaus ist es sicherlich möglich, innerhalb von ZFC den transitiven Abschluss einer beliebigen Menge oder Klasse auszudrücken A unter dem ∈ Beziehung: eine Menge B ist in der transitiven Schließung von A genau dann, wenn es eine endliche Kette gibt B ∈ A N + 1 ∈ A N ∈ ⋯ ∈ A 1 Wo A 1 ∈ A . Das kann als ein einziger Satz von ZFC geschrieben werden.
(Das ist der transitive Abschluss im mengentheoretischen Sinne. Für den transitiven Abschluss im ordnungstheoretischen Sinne würden wir setzen B ∈ ∗ A wenn es eine endliche Kette gibt B ∈ A N + 1 ∈ ⋯ ∈ A 1 = A Wo A N + 1 , A N , … , A 1 sind alle drin A . Das ist wieder ein einziger Satz von ZFC. Im Allgemeinen, wenn wir den transitiven Abschluss einer Relation definieren können R dann können wir den transitiven Abschluss von definieren ∈ durch bloßes Ersetzen R mit ∈ in der Definition.)
@Carl Mummert: Okay, jetzt, wo ich ein bisschen aufgewacht bin, sehe ich deine Abschlussdefinition von ∈ ist richtig. Wie auch immer, HOL-Computerassistenten haben keine Verständnisaxiome. Außerdem haben sie Lambda-Terme; Sie sind eine andere Tradition als das Bleistift-und-Papier-Henkin-Zeug. Ich verstehe nicht wirklich, was der Algorithmus ist, um Computer-HOLs in mehrfach sortierte FOL einzubetten. kannst du vielleicht ein Zitat geben?
Ich denke, das Problem ist, dass FOL keine einzelne Logik ist. Es gibt viele Logiken "erster Ordnung" mit leicht unterschiedlicher Syntax. Sie sind alle erster Ordnung in dem Sinne, dass sie über effektive deduktive Systeme, eine Semantik mit gewöhnlichen Strukturen erster Ordnung und Vollständigkeitstheoreme verfügen. Das FOL, das die Leute normalerweise zuerst sehen, hat keine Typen, λ Terme oder Mengenquantifizierer, aber diese können leicht hinzugefügt werden, während die Vollständigkeit gewahrt bleibt. Normalerweise λ Terme werden nur in der Beweistheorie oder in Computerumgebungen gesehen, zum Beispiel in der Arithmetik höherer Ordnung, wie in Kohlenbachs angewandter Beweistheorie .
Rechts; HOL-Beweisassistenten basieren auf Churchs früherer Formulierung, die älter ist als Henkins. Es scheint, dass eine Einbettung von Churchs HOL in FOL die Einbettung der Term-Algebra von HOL erfordert, also müssten Sie eine polymorphe binäre Operation @darstellende Anwendung einführen. Sieht aus, als hätte Harvey Friedman das in den 70ern herausgefunden. Unnötig zu erwähnen, dass ich nicht glaube, dass die Intuition von Henkins HOL direkt auf computerbasierte HOLs anwendbar ist. Das meiste habe ich nach dem Überfliegen dieser Masterarbeit herausgefunden: ps.uni-saarland.de/theses/kaminski/mthesis/kaminski-mthesis.pdf
Wie wird die vollständige Semantik von SOL und HOL spezifiziert?
AntwortenHierDatenschutz-Bestimmungen1y, 0v