Beweisassistent für das Schreiben von Mathematik

Ich möchte mathematische Beweise mit einem Proof-Assistenten schreiben. Alles wird unter Verwendung von Logik erster Ordnung (mit Gleichheit) und natürlichem Abzug geschrieben. Hintergrund ist die Mengenlehre (ZF). Wie könnte ich zum Beispiel den folgenden Beweis schreiben?

Axiom: $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$

Theorem: $\forall x\forall y(\forall z(z\notin x)\land\forall z(z\notin y)\rightarrow x=y)$

Das heißt, die leere Menge ist eindeutig.

Es ist für mich trivial, dies mit Papier und einem Stift zu bewerkstelligen, aber ich brauche wirklich eine Software, die mir hilft, den Beweis auf Richtigkeit zu überprüfen.

Vielen Dank.

Dies können sowohl Coq als auch Isabelle.

[Coq] In diesem Artikel wird erläutert, wie ZFC in CIC codiert wird, auf dem Coq basiert.

Benjamin Werner: Mengen in Typen, Typen in Mengen (1997). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709

[Isabelle] Es gibt eine Bibliothek für ZF.

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/index.html

Verschoben vom Kommentar auf Kavehs Vorschlag

Zuerst müssen Sie einen Proof-Assistenten auswählen. Coq ist das, was ich benutze, aber es gibt viele andere . Coq basiert auf einer Logik höherer Ordnung (der sogenannten Berechnung induktiver Konstruktionen). Andere Proof-Assistenten basieren auf der Logik erster Ordnung und können daher besser auf Ihre Bedürfnisse zugeschnitten sein (Modulo die obigen Kommentare).

Dann müssen Sie sich darauf festlegen, den Proof-Assistenten zu erlernen. Das verknüpfte Dokument ist ein Tutorial, mit dem Sie sich mit Coq vertraut machen können. Ein Coq-Experte zu werden, erfordert jahrelange Hingabe und Übung, aber einfache Sätze können an einem Nachmittag bewiesen werden. Der Schlüssel zum Erlernen von Coq oder eines anderen Proof-Assistenten besteht darin, Proofs zu erstellen, wie z. B. die im verlinkten Artikel. Nur das Lesen der Zeitung hilft wenig, da die gesamte Erfahrung der Interaktion mit dem Proof-Assistenten nicht gut auf Papier übertragen werden kann.

Innerhalb weniger Tage sollten Sie in der Lage sein, einfache Sätze wie den obigen zu kodieren und sie zu beweisen. Erwarten Sie nicht, dass wir das für Sie tun. So lernst du nichts.

Wenn es Ihnen gelingt, diese Theoreme zu beweisen, können Sie Ihre Antworten hier posten und vielleicht ein paar Kommentare zu Ihren Erfahrungen hinterlassen.

Bist du bereit für die Herausforderung?

Es gibt viele mathematische Artikel, die mit dem Proof-Assistenten Mizar geschrieben wurden: http://mizar.org/fm/

Dave Clarke schlägt Coq vor, aber Isabelle scheint eine viel bessere Idee zu sein, da es eine Bibliothek für ZF gibt . Isabelle ist auch sehr ausgereift und beinhaltet eine Vielzahl von Taktiken und Erweiterungen.

Ich habe Mizar nicht persönlich benutzt, aber es kann auch gut sein.

Wie könnte ich den folgenden Beweis schreiben?

In Isabelle / ZF kann man so etwas schreiben

theory csthquestion imports Main

begin

theorem empty_unique:
shows "\<forall> x.\<forall>y.(\<forall>z. (z\<notin>x)) \<and> (\<forall>z.(z\<notin>y)) \<longrightarrow> x=y"
    by auto

end

Wie Sie sehen, beweist Isabelle dies automatisch. Natürlich können Sie einen detaillierteren Beweis schreiben, wenn Sie es wirklich wollen.

Dieser Satz ist ein praktisches Beispiel (siehe Beispiel 11) in dem Tutorial, das in meiner DC Proof 2.0-Software enthalten ist. Laden Sie es kostenlos auf meiner Website http://www.dcproof.com herunter