Gibt es natürliche Abzugsregeln für die S5-Modaloperatoren, die die Einführungs- und Eliminierungsregeln für Quantoren in der Prädikatenlogik widerspiegeln? Ich erinnere mich, irgendwo Regeln wie die folgenden gesehen zu haben:
Einführung in die Notwendigkeit: Wenn Sie einen strengen Unterbeweis von A (ohne Hypothese) haben, können Sie auf □A schließen
Notwendigkeitsbeseitigung: □A impliziert A
Möglichkeitseinleitung: A impliziert ◇A
Möglichkeitsausschluss: Wenn Sie einen strengen Unterbeweis von B aus Hypothese A haben, dann können Sie aus ◇A auf B schließen
Wo es für die Einführung von Notwendigkeiten und die Eliminierung von Möglichkeiten Einschränkungen für den modalen Geltungsbereich von A, B und die Aussagen gibt, die in die strengen Unterbeweise importiert werden können (wie die Einschränkungen für das Auftreten der freien Variablen in der universellen Verallgemeinerung und der existentiellen Instanziierung). .
Intuitiv scheint es, als sollten die Regeln lauten:
Einführung in die Notwendigkeit: Wenn Sie einen strengen Unterbeweis von A (ohne Hypothese) haben, können Sie auf □A schließen
Notwendigkeitsbeseitigung: □A impliziert A
Möglichkeitseinleitung: A impliziert ◇A
Möglichkeits-"Eliminierung": Wenn Sie einen strengen Unterbeweis von B aus Hypothese A haben, können Sie aus ◇A auf ◇B schließen (beachten Sie die Hinzufügung des Möglichkeitsoperators zu B)
Wo die Einschränkung nur darin besteht, dass Sie notwendige Anweisungen importieren können, indem Sie einen anfänglichen Notwendigkeitsoperator entfernen. Aber das gibt kein S5. Meine Frage ist, ob es eine strengere Version der Regeln gibt.
S5 := T + 5 und T := K + M, wobei Axiom 5 := ◇p → □◇p, M (Reflexivitätsaxiom) := □p → p, und K das einfachste normale Modalsystem ist, das eine Notwendigkeitsregel hat N und Verteilungsaxiom K.
Basierend auf der obigen Definition und den Axiomen in Bezug auf Ihre "Notwendigkeitseinführung" tut dies genau die Notwendigkeitsregel im System K, dh p → □p, was so interpretiert werden kann, als ob p ein Theorem ist, dann ist □p ebenfalls ein Theorem .
In Bezug auf Ihre „Notwendigkeitsbeseitigung“ ist dies genau das oben für S5 definierte Reflexivitätsaxiom M.
In Bezug auf Ihre "Möglichkeitseinführung" kann dies trivial bewiesen werden, indem Sie Brouwers Axiom B (p → □◇p) mit dem obigen Reflexivitätsaxiom M in S5 hinzufügen.
In Bezug auf Ihre "Möglichkeitsbeseitigung" können wir in System K beweisen, dass □(A→B) → (◇A→◇B) (bei Interesse können Sie hier eine detaillierte Herleitung im Kommentar einer früheren PSE-Frage sehen), aber wenn Sie wirklich wollen ( A→B) → (◇A→◇B), dann scheint es die einzige Möglichkeit zu sein, dass die Formel (A→B) ein tautologisches Theorem ist, dann können wir die obige Notwendigkeitsregel N im System K anwenden, dann können wir bei (A→B) → □(A→B) ankommen, dann Modus Ponens, wir können (A→B) → (◇A→◇B) haben.
Es ist möglich, S5 unter Verwendung natürlicher Deduktionsstilregeln anstelle von Axiomen auszudrücken. Es ist jedoch ein ganzes Stück komplexer als nur eine einzige Einführungs- und Eliminierungsregel für Box und Diamond. Es gibt hier einen Artikel, der einen Ansatz beschreibt:
https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093888133
Eine Alternative ist die Verwendung des Folgenkalküls, der ein schnittfreies und entscheidbares System liefern kann. Der folgende Artikel beschreibt, wie S5 mit Hilfe des Folgenkalküls dargestellt werden kann.
Ein schnittfreier einfacher Folgenkalkül für die Modallogik S5
Ich habe herausgefunden, wonach ich gesucht habe. Die folgenden Schlußregeln, die zu denen für den klassischen Aussagenkalkül hinzugefügt werden, ergeben die S5-Modallogik:
Definition: Eine im Wesentlichen modale Anweisung hat die Form □A, ~□A, ◇A oder ~◇A.
Einführung in die Notwendigkeit: Wenn Sie einen strengen Unterbeweis von A (ohne Hypothese) haben, können Sie auf □A schließen, wobei alle vorherigen Aussagen, die Sie in den strengen Unterbeweis einfügen, im Wesentlichen modal sein müssen .
Notwendigkeitsbeseitigung: □A impliziert A
Möglichkeitseinleitung: A impliziert ◇A
Möglichkeitsbeseitigung: Wenn Sie einen strengen Unterbeweis von B aus Hypothese A haben, können Sie aus ◇A auf B schließen, wobei sowohl die Schlussfolgerung B als auch alle vorherigen Aussagen, die Sie in den strengen Unterbeweis einfügen, im Wesentlichen modal sein müssen .
Mit diesen Schlußregeln können Sie alle üblichen Axiome für S5 sowie die dualen Beziehungen ◇A=~□~A und □A=~◇~A beweisen (damit sie nicht von Hand eingegeben werden müssen, und Möglichkeit und Notwendigkeit werden als gleich grundlegend behandelt).
Bearbeiten: Die Definition von im Wesentlichen modalen Anweisungen kann wie folgt erweitert werden, ohne die Logik zu ändern:
Matt Dickau
Doppelter Knoten
Hummel
Doppelter Knoten
Doppelter Knoten