Warum können wir Schlußregeln nicht generell durch Axiome ersetzen?

Gibt es einen großen Unterschied darin, unzureichende Axiome und unzureichende Inferenzregeln / Beweisverfahren zu haben, um eine vollständige Theorie zu haben?

Es scheint, als hätte das Hinzufügen einer neuen Inferenzregel oder eines neuen Axioms in vielen Fällen den gleichen Effekt. Stellen Sie sich zum Beispiel eine Sprache mit 2-stelligen Konnektiven vor → , ∧ . Die Sprache hat auch eine Inferenzregel A → B , A ⟹ B .

Jetzt können wir ein neues Axiomenschema hinzufügen: A ∧ B → A Und A ∧ B → B für jede Formel A , B . Eine Alternative besteht darin, eine neue Inferenzregel hinzuzufügen: A ∧ B ⟹ A Und A ∧ B ⟹ B . In diesem Fall behaupte ich, dass die Theorien unabhängig von der Axiomatisierung gleichwertig sind.

Insbesondere würde ich denken, dass uns in der Logik zweiter Ordnung etwas daran hindert, Inferenzregeln durch Axiome zu ersetzen, egal wie viele Inferenzregeln definiert sind, da festgestellt wird, dass Beweiskalkül zweiter Ordnung immer unzureichend ist (für bestimmte Theorien). Sonst könnten wir immer denselben Beweiskalkül verwenden und lediglich Axiome hinzufügen und hätten so ein universelles Beweisprüfverfahren. Warum schlägt das Hinzufügen von Axiomen anstelle von Inferenzregeln fehl?

„Jetzt können wir ein neues Axiomenschema hinzufügen: a∧b→a und a∧b→b für jede Formel a,b. Eine Alternative besteht darin, neue Inferenzregeln hinzuzufügen: a∧b⟹a und a∧b⟹b. In diesem Fall behaupte ich, dass die Theorien unabhängig von der Axiomatisierung gleichwertig sind." Nein. Wenn Sie die Axiome ((a∧b)⟹a) und ((a∧b)⟹b) hinzufügen, dann sind die Schlussregeln (a∧b)⟹a und (a∧b)⟹b ableitbar wegen deine Distanzierungsregel. Aber aus der Distanzierungsregel folgt nicht, dass, wenn Sie die obigen Inferenzregeln hinzufügen, die obigen Formeln Theoreme sind. Folglich scheint diese Frage rückwärts. Es ist "Warum können wir Axiome nicht durch Regeln ersetzen?"
Ich verstehe nicht, was Ihrer Meinung nach das Ersetzen von Inferenzregeln durch Axiome mit der Vervollständigung der Logik zweiter Ordnung zu tun hat. Schlagen Sie gerade vor, für jede einzelne semantisch gültige Inferenz ein neues Axiom hinzuzufügen?

Antworten (1)

Axiome, Axiomschemata und Inferenzregeln sind 3 verschiedene Dinge.

Ein Axiom ist ein Datenelement. Es ist ein Satz, der ohne Beweis in eine Logik eingeführt wird.

Eine Rule of Inference (RoI) ist ein Programm. Man kann es sich als ein Programm vorstellen, um aus bestehenden Aussagen eine neue Aussage zu generieren (Aufzählung); man kann es sich als Entscheidungsverfahren vorstellen, um zu prüfen, ob aus bestehenden Aussagen eine neue Aussage folgt (Verifikation).

Ein Axiom-Schema ist ein RoI, das eine zählbar unendliche Anzahl von Aussagen einführt. Also die Beschreibung eines Axiomschemas als ( A ∧ B ) → A stellt vor ( X ∧ X ) → X , ( X > j ∧ j > z ) → ( X > z ) , etc, alles zur Theorie.

Einige Logiken haben explizit einen RoI namens "Propositional Substition". Dies ist die Regel, dass, wenn Sie einen Aussagenausdruck bewiesen haben, jede Aussagevariable vollständig durch einen beliebigen Aussagenausdruck ersetzt werden kann. Also zum Beispiel, wenn Sie sich bewährt haben ( X → X ) , dann kannst du daraus schließen ( ( A ∨ B ) → ( A ∨ B ) ) . Jaśkowski machte diese Regel in seiner Logik deutlich.

In einer Logik mit propositionaler Substitution induzieren Axiome und Axiomschemata derselben Beschreibung dieselbe Theorie. Tatsächlich neigen solche Logiken dazu, sich nicht einmal um Axiom Schema zu kümmern. In einer Logik ohne propositionale Substitution können Axiome und Axiomschemata derselben Beschreibung unterschiedliche Theorien hervorrufen. Zum Beispiel aus dem Axiom X → X du konntest nicht schlussfolgern Y → Y ohne propositionale Substitution.

Das Eliminieren aller RoI (auch nur derjenigen, die kein Axiom-Schema sind) würde es unmöglich machen, neue Theoreme in die Theorie einzuführen, sodass Sie niemals etwas beweisen könnten, außer dem, was explizit angenommen wird.

In der modernen Logik neigt eine heiße Frage dazu, genau das Gegenteil zu sein: Wie können wir es schaffen, dass der Benutzer einer Logik neue gültige RoI einführen kann? Es gibt viele Entscheidungsprozeduren, die Vorschläge bewerten und ihre Richtigkeit viel schneller bestimmen können, als wenn sie auf Zusammensetzungen einiger festcodierter ROI beschränkt wären, und wenn formale Bibliotheken größer werden, wird dies zu einem Hauptengpass.

Ich verstehe die Frage nicht ganz (und ich glaube auch nicht, dass OP dies tut), aber ich bin mir ziemlich sicher, dass dies überhaupt keine Antwort darauf ist. Soweit ich das beurteilen kann, lautet die eigentliche Frage hier: "Was bedeutet es, dass die Logik zweiter Ordnung kein gutes Beweissystem hat?".
Er stellt 2 verschiedene Fragen, die erste Hälfte und die zweite Hälfte sind meiner Meinung nach ziemlich unabhängig. Die erste Hälfte ist das, was ich hier anspreche.
@EricWofsey Das bedeutet, dass es eine Formel gibt, die in allen Modellen zutrifft, aber nicht bewiesen werden kann. Das bedeutet, dass wir neue Wahrheiten entdecken können, indem wir Inferenzregeln hinzufügen. Aber warum sich nicht einfach auf einige Inferenzregeln festlegen und nach Bedarf Axiome hinzufügen? Dann gibt es ein universelles Beweisverifizierungsverfahren ... und die Logik zweiter Ordnung verhält sich eher wie die erste Ordnung, bei der nur die axiomatische Unvollständigkeit das Problem ist (da der Beweiskalkül für FO vollständig ist). Ich denke, es muss einen Grund geben, warum das Hinzufügen von (konsistenten) Axiomen das Hinzufügen von Inferenzregeln nicht ersetzen kann, und frage mich, warum?
@Dole: Das Hinzufügen von Axiomen ist vollständig austauschbar mit dem Hinzufügen von Inferenzregeln. Niemand kümmert sich um einen der beiden Ansätze, weil keiner das eigentliche Problem tatsächlich mit Beweisen in Logik zweiter Ordnung löst.
Ein "universelles Beweisverifizierungsverfahren" ist nutzlos, wenn Sie nicht einmal überprüfen können, was Ihre logischen Axiome sind.
@EricWofsey Das Hinzufügen von Axiomen kann mit dem Hinzufügen von Inferenzregeln austauschbar sein. Aber das hängt vom System ab, ob das gilt oder nicht.
Warum können wir Schlußregeln nicht generell durch Axiome ersetzen?
AntwortenHierDatenschutz-Bestimmungen1y, 0v