Warum gibt es mehrere Axiomensysteme für die Aussagenlogik?

Tatsächlich gibt es viele Darstellungen der klassischen Aussagenlogik ¹ .

Wenn Komplexität nur anhand der Anzahl von Axiomen gemessen würde, dann wäre Mendelsons Axiomensystem "sparsamer". Wir könnten mit Merediths System noch "sparsamer" sein:

$$((((A\to B)\to(\neg C\to\neg D))\to C)\to E)\to((E\to A)\to(D\to A))$$ Geht einfach von der Zunge. Während Minimalität oft ein Treiber ist, müssen die Menschen immer noch minimalere Systeme entdecken. (Tatsächlich ist das Obige nicht das minimalste System, wenn wir die Komplexität des Axioms und nicht nur die Zahl einbeziehen.) Es stellt sich auch die Frage, die Axiome zu akzeptieren. Idealerweise möchten wir, dass die Axiome "selbstverständlich" oder zumindest intuitiv leicht verständlich sind. Vielleicht liegt es nur an mir, aber Merediths Axiom springt mir nicht als etwas entgegen, das offensichtlich wahr sein sollte, geschweige denn ausreichend, um alle anderen klassischen Tautologien zu beweisen.

Minimalität ist jedoch nicht der "ganze Sinn" axiomatischer Systeme. Sie erwähnen einen weiteren Grund: Manchmal wollen Sie tatsächlich Dinge beweisen, an denen es besser ist, ein reichhaltigeres und intuitiveres Axiomatiksystem zu haben. Sie können argumentieren, dass wir einfach alle Theoreme, die wir verwenden möchten, von einer minimalen Basis ableiten und diese Basis dann vergessen können. Das ist wahr, aber unnötige Komplexität, wenn wir keinen anderen Grund haben, diese minimale Basis in Betracht zu ziehen. Wenn wir verschiedene Stile von Beweissystemen vergleichen (z. B. Hilbert vs. Sequent Calculus vs. Natural Deduktion), können Übersetzungen zwischen ihnen (insbesondere in Systeme im Hilbert-Stil) eine Menge mechanischer Komplexität beinhalten. Diese Komplexität kann manchmal durch eine sorgfältige Auswahl von Axiomen erheblich reduziert werden.

Für die Gesetze der ausgeschlossenen Mitte (LEM) und der Widerspruchsfreiheit müssen Sie als Erstes die Konnektoren definieren. Du kannst es nicht beweisen$\neg(P\land\neg P)$in einem System, das nicht hat$\land$. Gegeben$\neg$Und$\to$als Primitive, Standarddefinitionen von$\land$Und$\lor$Sind$P\land Q:\equiv \neg(P\to\neg Q)$Und$P\lor Q:\equiv\neg P\to Q$. Mit diesen Definitionen (oder anderen) können LEM und Widerspruchsfreiheit sowohl in den von Ihnen erwähnten Systemen als auch in jedem anderen Beweissystem für die klassische Aussagenlogik bewiesen werden. Ihr Anliegen hier ist ein Beispiel dafür, dass uns oft wichtig ist, welche Axiome wir haben, und nicht nur, dass sie kurz und effektiv sind.

Dies führt auch zu einem weiteren Grund, warum wir möglicherweise eine bestimmte Präsentation wünschen. Wir möchten vielleicht, dass diese Präsentation mit anderen verwandten Logiken übereinstimmt. Wie Sie allmählich erkennen, ist es schlecht definiert, so etwas wie "Intuitionistische Aussagenlogik (IPL) ist klassische Aussagenlogik (CPL) minus LEM" zu sagen. Wenn Leute solche Dinge sagen, sind sie schlampig. „CPL ist IPL plus LEM“ ist jedoch eindeutig. Jede Präsentation von IPL, zu der wir LEM hinzufügen, ist eine Präsentation von CPL. Für diese Präsentation ist es sinnvoll, über das Entfernen von LEM zu sprechen. Es macht keinen Sinn, über das Entfernen eines Axioms zu sprechen, ohne eine Präsentation von Axiomen, die dieses Axiom enthält. Es ist auch durchaus möglich, dass eine Präsentation von CPL mit LEM auftritt, die viel schwächer wird als IPL, wenn LEM entfernt wird. In der Tat, du' Ich würde dies erwarten, weil eine Präsentation von IPL mit hinzugefügtem LEM wahrscheinlich redundant ist, weil Dinge, die intuitiv unterschiedlich sind, identifizierbar werden, wenn LEM hinzugefügt wird. Die Geschichte ist die gleiche für parakonsistente Logiken.

Während es für Beweissysteme im Hilbert-Stil nicht so sehr ein Treiber ist, drängen die Bedenken der strukturellen Beweistheorie für natürliche Deduktion und Folgekalküle oft nach mehrAxiome (oder vielmehr Schlußregeln). Zum Beispiel mischen viele Axiome in einem Beweissystem im Hilbert-Stil Konnektoren, wie es zB Meredith oben tut. Das bedeutet, dass wir ein Bindewort nicht für sich selbst verstehen können, sondern nur dadurch, wie es mit anderen Bindewörtern interagiert. Eine treibende Kraft in typischen Strukturdarstellungen ist die Charakterisierung von Konnektiven durch Regeln, die auf keine anderen Konnektive verweisen. Dies zeigt die "wahre" Natur der Konnektoren besser und macht das System modularer. Es wird sinnvoll, über das Hinzufügen oder Entfernen eines einzelnen Bindeworts zu sprechen, mit dem Sie eine Logik à la carte aufbauen können. Tatsächlich motiviert die Strukturbeweistheorie viele Einschränkungen, wie ein Beweissystem aussehen sollte, wie z. B. logische Harmonie .

¹ Und dieser Link berücksichtigt nur Beweissysteme im Hilbert-Stil.