Wurde der Kompaktheitssatz für FOL in Coq / Isabelle / etc formalisiert?
12
Ich habe nach einer Formalisierung des Kompaktheitssatzes für FOL gesucht, aber keine gefunden. Ist jemandem eine solche Entwicklung oder verwandte Arbeit bekannt?
Haben Sie versucht, auf den Coq- oder Isabelle-Mailinglisten nachzufragen?
Dave Clarke
2
Ich bin nicht sicher, ob dies für die Theorie geeignet ist, aber sehen Sie dies . Vollständigkeit ist da und Kompaktheit ist nicht weit davon entfernt.
Kaveh
Siehe auch den AFP-Eintrag für eine Version in Isabelle / HOL (ab 2004).
Makarius
Antworten:
16
Der Kompaktheitssatz für die klassische Logik erster Ordnung ist eine direkte Folge des Vollständigkeitssatzes, und tatsächlich kann man die Kompaktheit direkt durch das für die Vollständigkeit verwendete Argument im Henkin-Stil beweisen, ohne jemals die Ableitung zu erwähnen.
Der Vollständigkeitssatz für die klassische FOL in Bezug auf Standard-Tarski-Modelle wurde in Mizar formalisiert. Siehe die Artikelserie unter http://fm.mizar.org/2005-13/fm13-1.html
Ich sage "fast", weil es einen technischen Punkt gibt, der die Richtigkeit eines Sortieralgorithmus beweist, für dessen Fertigstellung ich noch keine Zeit hatte. Der Hauptbestandteil (konstruktiver Ultrafilter-Satz für zählbare Sprachen) ist jedoch formalisiert.
Man kann auch die Vollständigkeit und damit die Kompaktheit für einen nicht standardmäßigen Begriff der Gültigkeit betrachten und einen vollständigen und formalisierten konstruktiven Beweis erhalten.
Antworten:
Der Kompaktheitssatz für die klassische Logik erster Ordnung ist eine direkte Folge des Vollständigkeitssatzes, und tatsächlich kann man die Kompaktheit direkt durch das für die Vollständigkeit verwendete Argument im Henkin-Stil beweisen, ohne jemals die Ableitung zu erwähnen.
Der Vollständigkeitssatz für die klassische FOL in Bezug auf Standard-Tarski-Modelle wurde in Mizar formalisiert. Siehe die Artikelserie unter http://fm.mizar.org/2005-13/fm13-1.html
Der gleiche Vollständigkeitssatz, jedoch mit einem konstruktiven Beweis, wurde von mir im Coq-Beweisassistenten fast formalisiert (siehe Zip-Datei unter https://sites.google.com/site/dankoilik/publications/phd-thesis)
Ich sage "fast", weil es einen technischen Punkt gibt, der die Richtigkeit eines Sortieralgorithmus beweist, für dessen Fertigstellung ich noch keine Zeit hatte. Der Hauptbestandteil (konstruktiver Ultrafilter-Satz für zählbare Sprachen) ist jedoch formalisiert.
Man kann auch die Vollständigkeit und damit die Kompaktheit für einen nicht standardmäßigen Begriff der Gültigkeit betrachten und einen vollständigen und formalisierten konstruktiven Beweis erhalten.
quelle
Die Kompaktheit für FOL wurde in HOL von John Harrison durchgeführt und 1998 bei TPHOL berichtet. Siehe Formalisierung der grundlegenden Modelltheorie erster Ordnung .
quelle