Unter welchen Bedingungen hat ein axiomatisches Beweissystem ein natürliches Deduktionsäquivalent?

Mit "axiomatischem System" meine ich ein Beweissystem im Hilbert-Stil mit Axiomen und (typischerweise wenigen) grundlegenden Inferenzregeln, bei denen jeder Satz aus den Axiomen und diesen wenigen Regeln beweisbar ist. Zum einfachen Vergleich ein Folgensystem im Gentzen-Stil, bei dem jeder Satz nur mit unbedingten Linien bewiesen werden kann (Folgen, bei denen links vom Drehkreuz nichts vorkommt).

Mit „natürlichem Deduktionssystem“ meine ich ein Beweissystem, das auf Einführungs- und Eliminierungsregeln beruht und eine relativ große Menge an Schlussfolgerungen liefert. Zum Beispiel ein Folgenkalkül im Gentzen-Stil mit einigen Beweisen, die notwendigerweise Zeilen mit einer nicht leeren Menge von Prämissen links vom Drehkreuz enthalten.

Meine Frage betrifft die Anforderungen für die Äquivalenz im Sinne des Beweises derselben Theoreme. Ich interessiere mich besonders dafür, was auf einer gewissen Ebene der Allgemeinheit gesagt werden kann, ohne mich auf eine bestimmte Logik wie Aussagenlogik oder Logik erster Ordnung zu beschränken. Was ich über einige besondere Fälle weiß:

  1. (Klassische) Aussagenlogik: um die Äquivalenz zu einem natürlichen Deduktionssystem mit a → -Intro-Regel muss der Deduktionssatz im Axiomensystem gelten.
  2. (Klassische) Logik erster Ordnung: um die Äquivalenz zu einem natürlichen Deduktionssystem mit a ∀ -Intro-Regel, universelle Verallgemeinerung muss im Axiomatiksystem gelten.

Aber kann etwas Interessantes und Allgemeineres über die Bedingungen für Äquivalenz gesagt werden, insbesondere in Bezug auf andere Logiken (z. B. Modallogiken und Logiken höherer Ordnung) und axiomatische Theorien in der Mathematik? (Insbesondere jene Logiken und mathematischen Theorien, die unvollständig sind?) Welche Bedingungen sind erforderlich, um sicherzustellen, dass es für ein axiomatisches Beweissystem ein natürliches Deduktionsäquivalent gibt (und umgekehrt )? Gibt es Eigenschaften eines axiomatischen oder natürlichen Deduktionssystems, die eine Äquivalenz definitiv blockieren?

Antworten (1)

Mit „natürlichem Deduktionssystem“ meine ich ein Beweissystem, das auf Einführungs- und Eliminierungsregeln beruht und eine relativ große Menge an Schlussfolgerungen liefert. Zum Beispiel ein Folgenkalkül im Gentzen-Stil mit einigen Beweisen, die notwendigerweise Zeilen mit einer nicht leeren Menge von Prämissen links vom Drehkreuz enthalten.

Erstens haben natürliche Deduktionssysteme mehr Regeln, weil sie mehr logische Verknüpfungen verwenden ... Sie könnten auch ein axiomatisches System für mehr Verknüpfungen erstellen, und es hätte ebenfalls mehr Axiome. Tatsächlich besteht der natürlichste Weg, ein axiomatisches System mit Regeln für alle üblichen Konnektoren zu erstellen, darin, diese Regeln zu Konditionalisierungen der typischen Elim- und Intro-Regeln zu machen, z. B. könnten Sie ein Axiom haben ( P → Q ) → ( ( Q → P ) → ( P ↔ Q ) ) als axiomatische Konditionierung eines Typischen ↔ Intro Regel, während so etwas wie ( P ↔ Q ) → ( P → Q ) wäre ein guter Kandidat, um das zu axiomatisieren ↔ Elim-Schlußregel.

Ich weise darauf hin, weil Sie im obigen Absatz eine Verbindung zwischen der Anzahl der Regeln und der Tatsache herzustellen scheinen, dass ein natürliches Deduktionssystem Annahmen verwendet ... aber diese stehen in keinem Zusammenhang, da man mit genau diesen Regeln effektiv ein axiomatisches System erstellen kann (aber Konditionalisierungen davon). Der Kernunterschied zwischen axiomatischen Systemen und natürlichen Deduktionssystemen ist also tatsächlich nur die Tatsache, dass Sie Annahmen treffen können (dh „Unterbeweise“ beginnen) oder, wie Sie sagen, ein sequentielles System mit nicht leeren Unterstützungsmengen.

Diese mögliche Verbindung zwischen Regeln und Axiomen kann jedoch auch verwendet werden, um Ihre eigentliche Frage zu beantworten: Zumindest scheint es, dass Sie sicherstellen können, dass das axiomatische System dies kann, solange Sie die Elim- und Intro-Regeln auf die oben vorgeschlagene Weise konditionalisieren alles tun, was ein natürliches Abzugssystem tun kann. Und für den umgekehrten Weg ... nun, wenn die Axiome im axiomatischen System tatsächlich die konditionalisierten Versionen der Intro- und Elim-Regeln eines natürlichen Deduktionssystems sind, dann scheint das Deduktionstheorem zu genügen.

Wenn es natürlich keinen solchen systematischen Zusammenhang zwischen Axiomen und Inferenzregeln gibt, dann sind alle Wetten ungültig, und Sie müssten die Äquivalenz zwischen den verschiedenen Systemen eher ad hoc beweisen, ... mit anderen Worten, ich Ich kann Ihnen keine "allgemeinen Anforderungen für die Gleichwertigkeit" nennen ... außer natürlich, dass Sie nachweisen können, dass beide Systeme für sich vollständig sind.

Entschuldigung, ich wollte nicht andeuten, dass „mehr Regeln“ das bestimmende Merkmal von ND-Systemen ist – nur ein typisches Merkmal. Ich denke, die "allgemeineren Anforderungen", die ich im Sinn hatte, waren so etwas wie das, was Sie aus der Curry-Howard(-Lambek)-Korrespondenz erhalten, wo das Deduktionstheorem der Abstraktionseliminierung in der typisierten kombinatorischen Logik und entspricht → -intro entspricht der Funktionsabstraktion im Lambda-Kalkül....
... Es scheint also, dass eine Voraussetzung für die Äquivalenz Hilbert<->ND<->Folge darin besteht, dass der Abzugssatz für das Hilbert-System gilt, jede ND-Ableitung auf die Normalform reduzierbar ist und der Folgenkalkül eine Schnittelimination zulassen muss. Scheint so viel richtig zu sein? Wenn das stimmt, ist dann die "allgemeine Anforderung" (zumindest eine notwendige Bedingung), nach der ich suche (obwohl ich zugegebenermaßen nur bestenfalls herumstolpere), eine Übereinstimmung in dieser Art von Strukturregeln / Normalisierungseigenschaften?
@Dennis Hmm, vieles von dem, was du hier sagst, geht mir tatsächlich über den Kopf, sorry! Hoffentlich können Ihnen noch mehr erfahrene Logiker helfen ...
OK danke! Ich sollte dieses Zeug in die Frage aufnehmen. Nur um zu verdeutlichen, was ich Ihnen bedeutete, kam mir der Gedanke, nach diesen Zusammenhängen zu fragen. Ihre Antwort war also eine große Hilfe!
@Dennis Ah, okay! Ich schätze, manchmal braucht man einfach einen Resonanzboden. Ich bin froh, behilflich zu sein, ha ha! :) Aber ja, bearbeite deinen Beitrag und hoffentlich bekommst du ein paar andere Leute dazu, zu antworten!
Unter welchen Bedingungen hat ein axiomatisches Beweissystem ein natürliches Deduktionsäquivalent?
AntwortenHierDatenschutz-Bestimmungen1y, 0v