Welches Paradigma der automatisierten Theoremprüfung ist für die Formalisierung nach Principia Mathematica geeignet?

Ich besitze ein Buch, das, inspiriert von Russells Principia Mathematica (PM) und dem logischen Positivismus, versucht, einen bestimmten Bereich zu formalisieren, indem es Axiome bestimmt und daraus Theoreme ableitet. Kurz gesagt, es wird versucht, für seine Domäne das zu tun, was PM für die Mathematik versucht hat. Wie PM wurde es geschrieben, bevor ein automatisierter Theorembeweis (ATP) möglich war.

Ich versuche, diese Axiome in einem modernen ATP-System darzustellen und Theoreme abzuleiten, zunächst die vom Autor (von Hand) abgeleiteten. Ich habe noch nie ein ATP-System verwendet und angesichts der Vielzahl von Optionen (HOL, Coq, Isabelle und viele mehr) mit ihren Stärken, Schwächen und beabsichtigten Anwendungen ist es schwierig zu entscheiden, welche für meine spezifischen geeignet sind Zweck.

Der Formalismus des Autors spiegelt PM sehr gut wider. Es gibt Klassen (Mengen?), Klassen von Klassen usw. mit bis zu 6 Hierarchieebenen. Es gibt eine Logik erster Ordnung und möglicherweise eine Logik höherer Ordnung. Angesichts der Verbindung zu PM habe ich zunächst Metamath untersucht, da andere Theoreme von PM in MetaMath von anderen Personen bewiesen wurden. Metamath ist jedoch natürlich ein Beweisprüfer und kein ATP-System.

Bei der Beschreibung verschiedener ATP-Systeme sehe ich verschiedene Merkmale, wie z. B. Implementierungen der Typentheorie der Kirche, konstruktive Typentheorien, intuitionistische Typentheorien, typisierte / untypisierte Mengenlehre, natürliche Deduktion, Arten von Lambda-Kalkülen, Polymorphismus, rekursive Funktionstheorie und die Existenz von Gleichheit (oder nicht). Kurz gesagt, jedes System scheint eine ganz andere Sprache zu implementieren und muss für die Formalisierung verschiedener Dinge geeignet sein. Ich gehe davon aus, dass vorhandene Bibliotheken zur Formalisierung der Mathematik für meinen Zweck nicht relevant sind.

Jeder Rat bezüglich der Eigenschaften, die ich bei der Auswahl eines ATP einholen sollte, oder jeder andere Rat, den Sie nach dem Lesen dieser Frage haben könnten, wäre sehr dankbar. Als Referenz finden Sie hier eine Beispielseite aus dem Buch. Leider ist es wie PM in Peano-Russell-Notation.

Das Buch -

"Die axiomatische Methode in der Biologie" (1937), JH Woodger, A. Tarski, WF Floyd

Die Axiome beginnen mit dem mereologischen. Beispielsweise,

1.1.2 ist die Summe von wenn in den Teilen von , und wenn ein Teil von gibt es immer ein das zu und Teile hat, die mit den Teilen von :$x$$\alpha$$\alpha$$x$$y$$x$$z$$\alpha$$y$

$$S{ = }_{ Df }\hat { x } \hat { \alpha } \{ \alpha \subset \vec { { P }^{ ‘ } } x:.(y):yPx.\supset .(\exists z).z\in \alpha .\vec { { P }^{ ‘ } } y\cap \vec { { P }^{ ‘ } } z\neq \Lambda \}$$

Beachten Sie erneut, dass dies die Peano-Russell-Notation (die Notation von Principia) ist.

Spätere Axiome haben biologischen Inhalt, wie z.

7.4.2 Wenn sich Gameten zweier Mitglieder einer Mendelschen Klasse paarweise zu Zygoten vereinigen, ist die Wahrscheinlichkeit, dass sich ein bestimmtes Paar vereinigt, gleich der des anderen Paares.

Soweit ich weiß, war dies ein Postulat der Mendelschen Genetik.

Ich lasse die Notation dafür weg, weil sie drei Zeilen lang ist und auf zuvor definierten Inhalten aufbaut.

Beispiel eines Satzes -

Dies hat anscheinend eine bedeutungsvolle Interpretation in der Mendelschen Genetik, die ich als Historiker der Biologie nicht verstehe. In dem Buch wurde es von Hand abgeleitet.

Vielen Dank!

Principia Mathematica war eine weitgehend Antwort auf die verschiedenen Paradoxien, die um die Wende des 20. Jahrhunderts in der mathematischen Logik entdeckt wurden. Das Werk selbst, das oft schräg als „unlesbares Meisterwerk“ gelobt wurde, ist jedoch etwas ungeschickt und es wurden modernere Fundamente geschaffen. Um den größten Teil der Mathematik zu beschreiben, haben Sie mehrere Möglichkeiten: Die Kategorietheorie ist eine, die Typentheorie war in einigen Projekten als Erweiterung des Lambda-Kalküls beliebt, aber die am besten verstandene und grundlegendste ist wahrscheinlich die Mengenlehre.

Die Mengenlehre hat verschiedene Formulierungen; Die Mengenlehre von Zermelo Frankel mit dem Axiom der Wahl ist die orthodoxste, die von Enthusiasten der Mengenlehre liebevoll als wird. Die Tarski-Grothendiek-Mengenlehre ist eine andere, die der weitgehend ähnlich ist und Tarskis Axiom für die Argumentation über große Kategorien enthält. Diese sind interessant für die Kontrolle, aber etwas schwieriger für automatisiertes Theorem Proving weil das Ersetzungsaxiom eine unendliche Anzahl von Axiomen gibt , die eine Herausforderung für die Umsetzung darstellen. Während diese Grundlagen für Beweisverifizierungssysteme wie Mizar für Tarski-Grothendiek-Mengenlehre und Metamath für durchaus sinnvoll sind$\sf ZFC$$\sf\ ZFC$$\sf ZFC$Für ein tatsächliches Theorembeweisungssystem wäre eine endliche Axiomatisierung schön.

Die wahrscheinlich am besten geeignete Grundlage dafür ist die Von Neumann-Bernays-Gödel-Mengenlehre oder , die eine endliche Axiomatisierung zulässt, indem sie eine zweisortierte Theorie ist, die eine Ontologie geeigneter Klassen sowie Mengen aufweist. Ferner wurde bewiesen, dass eine konservative Erweiterung von , so dass jeder Satz von ein Satz vonN B G Z F C N B G Z F $\sf NBG$$\sf NBG$$\sf ZFC$$\sf NBG$$\sf ZFC$. Der Grund, warum diese Theorie meiner Meinung nach am besten für das automatisierte Denken geeignet ist, ist ihre Ausdrucksweise in der Logik erster Ordnung, die eine effektive, solide und vollständige Beweisrechnung zulässt, und eine endliche Axiomatisierung bedeutet, dass sie mit einer Auflösung erster Ordnung verwendet werden kann, die uns die gibt ordentliches Ergebnis: Wenn eine Aussage entscheidbar ist, wird schließlich ein Beweis gefunden.

Aussagenlogik ist nicht ausdrucksstark genug, und Logik höherer Ordnung lässt, obwohl sie viel ausdrucksvoller ist, keinen effektiven, soliden und vollständigen Beweiskalkül zu. Die Logik erster Ordnung mit der Mengenlehre ermöglicht es Ihnen, logische Theorien höherer Ordnung darzustellen und abzubilden. Für Grundlagen ist dies also der Sweet Spot ... mit Ausnahme der Möglichkeit unentscheidbarer Aussagen (dank Gödel), weshalb Theorien erster Ordnung einen ausreichenden Quantifiziererrang haben werden oft als halbentscheidbar beschrieben.

Art Quaife hat einige Arbeiten dazu durchgeführt in: Automatisierte Entwicklung grundlegender mathematischer Theorien, wo er in Logik erster Ordnung in klausaler Form implementierte , damit es von einem auflösungsbasierten Theorembeweiser (Otter) und einer hervorragenden Referenz für die Behandlung verwendet werden kann Die Grundlage für diese Art von Arbeit ist Elliott Mendelsons Einführung in die mathematische Logik.$\sf NBG$

Nun moderner Beweis Assistenten sind oft weniger mit Fundamenten aus dem Paradigma der Principia Mathematia und sind nützlich für Satz für die tägliche Arbeit zu beweisen, und so haben sie eine gewisse Unterstützung für Fragmente höherer Ordnung Logik, SAT / SMT Lösung, Typ Theorien und andere informellere und weniger grundlegende Ansätze. Wenn Sie jedoch versuchen, etwas wie Principia Mathematica zu tun, ist ein Auflösungssatzbeweiser erster Ordnung mit einer endlich axiomatisierbaren Mengenlehre erster Ordnung ideal.

Für einige Beispiele, wie automatisierte Theoremprüfer Probleme von diesen Grundlagen aus angreifen, weist die TPTP- Site (Thousands of Problems for Theorem Provers ) eine Reihe von Problemen auf, und Sie werden feststellen, dass viele der grundlegenden Probleme in der Zahlentheorie in Mengenlehre. Wenn Sie Zeit haben, lesen Sie NUM006-1.p auf ihrer Website: die Goldbach-Vermutung. Sie können versuchen, es auszuführen, und wenn es entscheidbar ist, wird schließlich ein Beweis gefunden.$\sf NBG$

Die Theoreme in Ihrem Buch werden mit ziemlicher Sicherheit Theoreme von , da sie in der Sprache der Mengenlehre geschrieben sind. Die Axiome der Genetik in diesem Buch werden mit ziemlicher Sicherheit als Definitionen für festgelegte theoretische Prädikate dargestellt, ähnlich wie die Peano-Arithmetik in als Definitionen von Prädikaten dargestellt wird. Von dort aus folgen Sie dem Auflösungsverfahren in jedem ATP. Wählen Sie eine Aussage aus, die Sie beweisen möchten, negieren Sie sie, konvertieren Sie sie in die Skolem-Normalform und dann in die Klauselform und folgen Sie der Auflösung. Wenn Sie die leere Klausel finden, haben Sie einen Widerspruch gefunden, der die Aussage beweist.N B $\sf NBG$$\sf NBG$

Die Aufgabe, die Sie haben, wenn Sie versuchen möchten, die Theorie in Bezug auf die Mengenlehre zu definieren, besteht darin, die von der Mengenlehre getrennten relationalen Prädikatdefinitionen zu finden, mit denen Sie die Prädikate in Bezug auf die Mengenlehre erstellen können. Ein Beispiel dafür ist wiederum die Definition der Peano-Arithmetik in der Mengenlehre, die für sich genommen keine Definitionen von Zahlen, Addition, Multiplikation oder sogar Gleichheit enthält. Als Beispiel für eine festgelegte theoretische Definition einer Beziehung wie Gleichheit können wir sie in Bezug auf die Mitgliedschaft als solche definieren:

∀ & egr ; ↔ & egr ; $\forall$ xy ( z (z x z y) x = y)$\forall$$\in$$\leftrightarrow$$\in$$\leftrightarrow$

Ein bisschen Warnung: Die Lernkurve dafür ist in der Tat sehr steil. Wenn Sie beabsichtigen, dies zu verfolgen, werden Sie sich möglicherweise einige Jahre später wiederfinden, bevor Sie das gesamte Problem erfassen, wie es meine Erfahrung war. Vielleicht möchten Sie die Theorie von einem weniger grundlegenden Ansatz aus untersuchen, bevor Sie die enorme Aufgabe übernehmen, sie für alles in eine grundlegende Sprache einzubetten. Schließlich müssen Sie nicht unbedingt über unzählige Mischungen von Genen nachdenken.

Mehrere Punkte:

1. Soweit ich weiß, verwendet Principia Mathematica im Wesentlichen eine Formalisierung der Mengenlehre unter Verwendung einer typisierten Logik erster Ordnung. Es wäre daher verlockend, einen automatisierten Theorembeweiser erster Ordnung wie Prover 9 oder möglicherweise ACL2 zu verwenden, um Ihre Aussagen zu formalisieren. Ich sehe dort jedoch mehrere satztheoretische Konstruktionen (wie , ), die normalerweise mit ATP erster Ordnung nicht sehr gut spielen.∩ , $\in$$\cap, \subset$

2. Jeder moderne interaktive Proof-Assistent wird sicherlich die Ausdruckskraft haben, Ihre Aussagen zu formalisieren und zu beweisen, wie Andrej vorgeschlagen hat. In der Tat wäre es ratsam, ein System wie Isabelle , Coq oder HOL zu verwenden, das bereits umfangreiche Theorien zur Behandlung von arithmetischen Aussagen enthält , da es einige Aussagen einschließlich Arithmetik zu geben scheint . Meine Betonung auf Modern ist kein Zufall: Seit Automath wurden große Fortschritte bei der Benutzerfreundlichkeit erzielt, und ich glaube ehrlich, Sie würden sich selbst einen schlechten Dienst erweisen, wenn Sie etwas verwenden, das seit den 90er Jahren nicht mehr aktiv entwickelt wurde (wenn Sie überhaupt einen bekommen könnten arbeiten!)

3. Schließlich haben ITP und ATP ziemlich herausfordernde Lernkurven, und Sie sollten nicht erwarten können, dass Sie diese Theoreme in ein solches System eingeben können, als ob Sie einen Beweis schreiben würden . Erwarten Sie starke Frustration und Zeitverlust, insbesondere in den ersten Monaten (ja, Monaten). Sie müssen auf jeden Fall zuerst einige Tutorials durcharbeiten, bevor Sie zur Hauptformalisierung gelangen.$\LaTeX$