Sind Axiome und Schlußregeln austauschbar?

Es gibt eine Äquivalenz zwischen zellularen Automaten und formalen Systemen, man kann das eine in das andere kodieren und umgekehrt. Aber in den zellularen Automaten (CA) sind die Schlußregeln festgelegt und ziemlich einfach (zum Beispiel die universelle Zwei-Nachbar-Zwei-Zustand-Regel 110). Daher müssen alle Regeln des formalen Systems, das in eine Regel 110 CA (ebenfalls ein formales System) codiert wird, hauptsächlich in der Eingabe codiert werden. Und umgekehrt, wenn Sie ein formales System haben, das Regel 110 ähnelt, können Sie Ihre Axiome in Inferenzregeln in einem anderen formalen System kodieren.

Ist das richtig? Hat diese Austauschbarkeit zwischen Axiomen und Regeln eine Bedeutung für die Grundlagen der Logik und/oder Mathematik?

Antworten (2)

In axiomatischen und natürlichen Deduktionsbeweissystemen sind Axiomenschemata und Inferenzregeln größtenteils austauschbar. In einem System mit Modus Ponens und einem Konditional → , zum Beispiel jede Folgerungsregel der Form

Λ / Γ
könnte durch das Axiomschema ersetzt werden
Λ → Γ
Im ersten Fall, wenn Sie haben Λ , dann können Sie durch die Inferenzregel folgern Γ . Im zweiten Fall ggf Λ , instanziieren Sie dann das Axiomschema, um zu ergeben Λ → Γ und verwenden Sie Modus Ponens, um zu schließen Γ . Ich denke, das zeigt, wie Inferenzregeln durch Axiomschemata ersetzt werden können (solange Sie Modus Ponens oder ein Äquivalent haben).

Das Ersetzen von Axiomschemata durch Inferenzregeln ist etwas einfacher, obwohl es sich wie ein bisschen Hack anfühlen kann. Wenn Sie das Axiomschema haben

Λ
Ersetzen Sie es einfach durch eine Inferenzregel ohne Vorbedingungen
/ Λ

Dieser Ansatz sollte unabhängig von den Besonderheiten Ihrer Axiomenschemata und Inferenzregeln funktionieren, da die Überprüfung, ob ein Schritt in einer Ableitung eine gültige Anwendung einer Inferenzregel auf der Grundlage einer Reihe von Prämissen ist, nicht mehr oder weniger schwierig sein sollte als die Überprüfung, ob a Formel ist eine Instanz eines Axiomenschemas.

In der ersten Hälfte gibt es ein kleines Problem. Die Inferenzregel A ⊢ B gilt nur, wenn man ableiten kann A , während das Axiom A → B muss in jedem Modell stimmen. Also wenn A nicht ableitbar ist, kann es sein, dass ein Modell nicht erfüllt A → B obwohl diese wahren Sätze unter der Inferenzregel geschlossen sind A ⊢ B . Dieses Phänomen tritt in bestimmten formalen Systemen auf, die in der mathematischen Logik vorkommen, obwohl es so dunkel ist, dass es in einführenden Texten normalerweise nicht erwähnt wird.
@CarlMummert, das ist ein sehr interessanter Punkt. Auf Anhieb sind mir solche Systeme nicht bekannt, aber ich wäre sehr daran interessiert, einige Beispiele zu hören. Stimmt meine Intuition, dass solche Systeme kein Deduktionstheorem haben (denn wenn ja, könnte man annehmen A , ableiten B , und dann, nach dem Abzugssatz, Schlussfolgerung A → B )?
Genau - diese Systeme haben kein Deduktionstheorem.
Mein anderer Kommentar, den ich gelöscht habe, war schlecht formuliert. Lassen A Sei C = 0 Und B Sei D = 1 in der Sprache der Arithmetik mit neuen konstanten Symbolen C , D . Lassen M sei das Standardmodell der Arithmetik, mit C Interpretiert als 0 Und D Interpretiert als 0 . Lassen T die Schließung sein P A nach den üblichen Schlußregeln. Dann T ist auch unter der Regel geschlossen C = 0 ⊢ D = 1 , Weil P A kann nicht beweisen C = 0 nach den üblichen Schlußregeln. Somit M ist ein Modell von T . Aber M ist kein Modell von P A plus das zusätzliche Axiom C = 0 → D = 1 .
(Ich konnte dem ersten Beispiel folgen, aber die Umschreibung ist auch in Ordnung.) Also würde ein solches System im Allgemeinen keine Deduktionstheoreme haben. Es scheint, als ob dieses System auch keinen semantisch orientierten Korrektheitsbeweis haben kann, da es Modelle dafür gibt C = 0 / D = 1 führt falsche Sätze ein. (Zumindest wird die Solidität dieser Regel nicht gezeigt, indem dies für jeden Satz von Formeln demonstriert wird Φ , Φ ⊨ C = 0 impliziert Φ ⊨ D = 1 .) Aber, wie Sie betonen, da C = 0 wird nicht beweisbar sein , wird es auch nicht D = 1 . Gilt hier eine andere Art von Solidität?
Im Allgemeinen erfordert der Beweis eines Korrektheitssatzes mit zusätzlichen Inferenzregeln, dass der Satz "zulässiger" Modelle eingeschränkt wird, um nur Modelle einzuschließen, bei denen die wahren Sätze unter den neuen Inferenzregeln geschlossen sind. Dies ist automatisch für den üblichen Satz von Inferenzregeln - jedes Modell funktioniert für diese nach dem üblichen Vollständigkeitssatz. Aber zusätzliche Inferenzregeln sind, wie Sie betonen, möglicherweise nicht für die Menge aller Modelle geeignet. Das Beispiel, das ich gegeben habe, ist ein Beispiel für eine neue Inferenzregel, die nicht korrekt ist, wobei die übliche Form des Korrektheitssatzes, der über alle Modelle quantifiziert, falsch wäre.
Modallogik ist ein Beispiel, bei dem das Deduktionstheorem nicht gilt (Beantwortung einer obigen Frage. Siehe zum Beispiel TLA+2 research.microsoft.com/en-us/um/people/lamport/tla/…

Zellulare Automaten werden als Teilmenge der formalen Systeme betrachtet, daher ist es richtig, was Sie über Axiome und Regeln sagen, die relativ sind. Ich erinnere mich tatsächlich, dass ich vor langer Zeit etwas darüber in einem Buch über das automatische Beweisen von Theoremen gelesen habe, aber ich kann mich nicht an die Details erinnern. In Bezug auf die philosophische Bedeutung davon bin ich der Ansicht, dass dies nur zeigt, wie viele Optionen Sie haben, wenn Sie ein formales System zum Codieren Ihres interessierenden Modells auswählen.

Sind Axiome und Schlußregeln austauschbar?
AntwortenHierDatenschutz-Bestimmungen1y, 0v