Mathematisches Logikbuch, das einen Beweisassistenten verwendet?

Ich suche ein Einführungsbuch in die mathematische Logik, das auch eine Implementierung seiner Logik in einem Beweisassistenten behandelt. Es scheint mir, dass dies eine großartige Möglichkeit wäre, mathematische Logik zu lernen, da viele Konzepte sehr klar und konkret werden würden, wenn sie in einem Computerprogramm implementiert würden. Aber so ein Buch habe ich noch nie gesehen.

Vorzugsweise führt das Buch die Sprache des Beweisassistenten ohne Vorkenntnisse ein und ermutigt den Leser, sie an verschiedenen Stellen zu verwenden.

BEARBEITEN

Ich mag die bisher geposteten Antworten und möchte dies noch eine Weile offen halten, um andere Empfehlungen an einem Ort zu sammeln. Nach dem Öffnen fand ich jedoch auch die folgenden hervorragenden Ressourcen, die in dieser Frage verlinkt sind, nämlich diese Ressourcenliste und dieses Buch / diese Zusammenstellung von Notizen von Jeremy Avigad. Diese Ressourcen scheinen die Art von Dingen zu sein, nach denen ich gesucht habe, und könnten für andere hilfreich sein, die über diesen Beitrag stolpern.

BEARBEITEN 2

Ein Feature, das ich wirklich gerne sehen würde, das ich bisher in den Vorschlägen nicht gesehen habe, ist ein Buch, das seine Metalogik auch innerhalb eines Beweisassistenten formalisiert. Zum Beispiel würde ich mich über ein Buch freuen, das (zum Beispiel) einen Korrektheitssatz beweist und zeigt, wie ein solcher Beweis mit einem Beweisassistenten implementiert werden könnte.

Andererseits wäre ich überrascht, wenn eine solche Ressource existiert, da keine mathematischen Logikbücher (die ich gesehen habe) auch nur die Idee der Formalisierung der Metalogik erwähnen.

Würden die Texte aus dem Open Logic Project zählen, wo sie ein handentwickeltes Webtool zur formalen Überprüfung von Beweisen in ihren Systemen haben? Oder fragen Sie mit einem Allzweck-Beweisassistenten gezielt nach etwas?
@DanielSchepler Ich bin mit jeder bestimmten Software einverstanden - solange sie neben einer Ressource zum Unterrichten mathematischer Logik für Lehrzwecke verwendet wird. Scheint, als wäre OLP eine großartige Ressource, obwohl ich das von Ihnen erwähnte Web-Tool zur Beweisüberprüfung nicht finden kann.
Um Ihre Füße nass zu machen, könnten Sie meine Proof-Checker-Freeware in Betracht ziehen, die von meiner Homepage unter dcproof.com mit begleitendem Tutorial heruntergeladen werden kann. Es wurde entwickelt, um Studenten in die grundlegenden Beweismethoden einzuführen. Es basiert auf einer vereinfachten Form der natürlichen Deduktion und der Mengenlehre, die implizit in den meisten mathematischen Lehrbüchern (nicht Standard-FOL oder ZFC) verwendet zu werden scheint.
Zu Ihrer zweiten Bearbeitung: In dem von mir verlinkten Entwurf wird am Ende des Kapitels über Natürliche Deduktion die Solidität und Vollständigkeit der klassischen Aussagenlogik gezeigt. Die Formalisierung der vollständigen Metalogik, die ein Buch verwendet, ist eine komplizierte Frage; das Buch muss dann explizit zwischen seiner Metalogik und der Objektlogik unterscheiden, die es untersuchen will. Üblicherweise wird der Beweisassistent (und seine Logik) als Metalogik verwendet, in der Ergebnisse diskutiert werden. Dann ist es wirklich eine ganz eigene Herausforderung, alle Feinheiten der Beweisassistentenlogik zu formalisieren (!).
Dans Website ist für eigentliche mathematische Arbeiten, wie etwa den wertlosen Beweis des Schroder-Bernstein-Theorems, nicht brauchbar .
Für diejenigen, die an Proof-Assistenten interessiert sind, gibt es eine neue vorgeschlagene SE-Site ProofAssistants

Antworten (3)

Ich würde John Harrisons Handbook of Practical Logic and Automated Reasoning wärmstens empfehlen . Die Programmierbeispiele haben eher mit der Implementierung von Beweisassistenten und Entscheidungsverfahren zu tun als mit der Verwendung eines Beweisassistenten, aber ich denke, sie erfüllen Ihren Wunsch nach Implementierungen, die die Schlüsselkonzepte verdeutlichen. Die Beispiele sind alle in der funktionalen Programmiersprache OCaml angegeben .

Zur zweiten Bearbeitung: Ich denke, in den meisten Texten zur mathematischen Logik ist implizit enthalten, dass das Thema in einem geeigneten Grundlagensystem wie ZF formalisiert werden kann. In der Literatur zur mathematischen Logik wird dies wichtig und explizit in Arbeiten zur Unabhängigkeit . In der Welt der Beweisassistenten ist die Selbstformalisierung im Hinblick auf mehr Sicherheit und Verständnis seit vielen Jahren von Interesse. Siehe z. B. dieses Papier zur Selbstverifizierung von HOL und die darin enthaltenen Referenzen. Ich denke, die allgemeinen Prinzipien einer formalisierten Metalogik sind wahrscheinlich aufschlussreicher als die feinen Details der Formalisierung.

Probieren Sie grundlegende Beweismethoden in der Informatik aus. Es verwendet Athena als Beweisassistent. Es lehrt sowohl Logik als auch Sprache.

Wenn Sie das komplex finden, hier ein einfaches - https://staff.washington.edu/jon/flip/www/userguide-nd.html Es funktioniert mit Python 2.7.

Bücher, die einen begleitenden Beweisassistenten für ihre Logik haben, sind eine Möglichkeit, es zu betrachten, aber es funktioniert auch umgekehrt: Die meisten Beweisassistenten implementieren eine bestimmte (normalerweise konstruktive) Logik und daher sind Bücher über den Beweisassistenten bereits Bücher über diese Logik .

Hier sind einige Ressourcen zu Coq :

Die Lean Community - Website hat eine Seite mit empfohlenen Lernressourcen .

Und vergessen wir nicht das HoTT-Zeug:

Mathematisches Logikbuch, das einen Beweisassistenten verwendet?
AntwortenHierDatenschutz-Bestimmungen1y, 0v