Unterschied zwischen logischen Axiomen und Schlußregeln

Ein logisches Axiom kann als Folgerungsregel betrachtet werden, die zufällig keine Vorläufer hat.

Jedes interessante Beweissystem muss mindestens ein Axiom und eine Schlussregel mit Prämissen haben. Wenn es keine Axiome gibt, dann gibt es keine Möglichkeit, einen Beweis in der leeren Theorie zu beginnen, und ohne Schlußregeln könnten nur die Axiome selbst bewiesen werden.

Beweissysteme im Hilbert-Stil haben im Allgemeinen viele Axiome und wenige richtige Inferenzregeln. Im Gegensatz dazu haben Kalküle im Gentzen-Stil ( Folgenkalkül und natürlicher Abzug ) eine minimale Anzahl von Axiomen und viele Inferenzregeln.

In beiden Fällen kann man jede Instanz eines Axioms und/oder einer Folgerungsregel als Zeichenkette in einer bestimmten formalen Sprache ausdrücken.

Eine Theorie besteht aus Axiomen, die man zu den logischen Axiomen hinzufügt , die aus der Logik stammen. Theorien enthalten keine eigenen Schlußregeln.

Es ist im Wesentlichen eine Frage des Standpunkts.

Die Idee logischer Axiome lässt sich auf Freges Begriffsschrift (1879) zurückführen . Logik ist für Frege eine Wissenschaft, insbesondere der Wissenszweig, der sich mit der Wahrheit befasst. Daher ist es wichtig, eine Reihe von Gesetzen zu haben, die den Gegenstand regeln, nämlich den Begriff der Wahrheit. Das sind die Dinge, die wir als logische Axiome kennen.

Es scheint natürlich, die komplexeren dieser Urteile [des reinen Denkens] aus einfacheren abzuleiten, nicht um sie sicherer zu machen, was in den meisten Fällen unnötig wäre, sondern um die Beziehungen der Urteile zu einem deutlich zu machen andere. Nur die Gesetze zu kennen, ist offensichtlich nicht dasselbe wie sie zu kennen, zusammen mit den Verbindungen, die einige zu anderen haben. Auf diese Weise gelangen wir zu einer kleinen Zahl von Gesetzen, in denen, wenn wir die in den Regeln enthaltenen hinzufügen, der Inhalt aller Gesetze enthalten ist, wenn auch in einem unausgereiften Zustand. (Frege 1879, §13)

Es ist auch wichtig zu erwähnen, dass es für Frege (und Russell) keinen klaren Unterschied zwischen Logik und Mathematik gab, also die moderne Praxis, die in Mengentheorien wie ZFC veranschaulicht wird, logische Prinzipien als Schlussfolgerungsregeln und fachspezifisch zu integrieren mathematische Tatsachen als Axiome waren undenkbar.

Gentzens Untersuchungen über das logische Schließen (1934/1935) markierten den Wendepunkt von dieser frühen axiomatischen zur modernen schlussfolgernden Auffassung von Logik. Im Grunde bestand Gentzens Idee darin, einen Begriff des formalen Beweises zu entwickeln, der dem tatsächlichen mathematischen Denken besser entspricht:

Mein Ausgangspunkt war folgender: Die Formalisierung der logischen Deduktion, insbesondere wie sie von Frege, Russell und Hilbert entwickelt wurde, ist ziemlich weit entfernt von den in der Praxis verwendeten Formen der Deduktion bei mathematischen Beweisen. Dafür werden erhebliche formale Vorteile erzielt. Im Gegensatz dazu wollte ich zunächst ein formales System aufstellen, das dem tatsächlichen Denken so nahe wie möglich kommt. Das Ergebnis war ein „ Kalkül des natürlichen Abzugs “. (Gentzen, 1934/1935)

Tatsächlich ist es nicht sehr angenehm, mit Hilbert-Kalkülen zu arbeiten, da formale Beweise einfacher Tautologien in diesen Systemen oft auf extrem künstlichen Argumenten beruhen. Erwähnenswert ist vielleicht, dass Frege selbst nicht bemerkt hat, dass seine sechs Axiome für den Aussagenkalkül nicht unabhängig sind:

1. $A \rightarrow (B \rightarrow A)$
2. $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$
3. $(A \rightarrow (B \rightarrow C)) \rightarrow (B \rightarrow (A \rightarrow C))$
4. $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$
5. $\neg \neg A \rightarrow A$
6. $A \rightarrow \neg \neg A$

Das heißt, Axiom 3 kann aus modus ponens und den Axiomen 1 und 2 erhalten werden. Dieses Ergebnis wurde erstmals 1929 von Łukasicwicz festgestellt. Darüber hinaus können die Axiome 3, 4 und 5 alle auf ein einziges Axiom reduziert werden:

Auch dies blieb von Frege unbemerkt.

Kalküle im Gentzen-Stil rücken Schlußregeln stärker in den Vordergrund, die den Prozeß des Denkens mit logischen Konnektoren darstellen, indem sie erklären, wie sie erhalten werden können (Einführungsregeln) und was wir mit ihnen machen können (Eliminationsregeln). Typischerweise verlassen sie sich nur auf wenige Axiome, wie zum Beispiel das Axiom der Reflexion:

aber selbst dies kann als eine Schlußregel ohne Annahmen angesehen werden!