Ich habe mehrere Artikel über modale natürliche Deduktion gelesen, aber ich konnte nur eine klare Erklärung der []-Einführung finden ( []Awenn Aaus keinen Annahmen/Prämissen bewiesen werden kann). Aber es gab keine gesonderten Regeln für die <>-Einleitung. Stattdessen <>Awurde definiert als ~[]~A. Und es gab überhaupt keine Regeln für die Eliminierung von Quantoren.
Aus ästhetischen Gründen würde ich es vorziehen, in einer Logik zu arbeiten, in der alle Symbole primitiv definiert sind und ihre Entsprechungen Ergebnisse sind und in der wir Terme nicht im Rahmen eines Quantifizierers manipulieren können.
Gibt es eine solche Formalisierung der Modallogik? Was sind seine Einführungs- und Eliminierungsregeln? Gibt es Papiere dazu?
Aus Garsons Modallogik für Philosophen (Link in den Kommentaren oben):
Zuerst führen wir eine neue Art von Unterbeweis ein, einen geschachtelten Unterbeweis . Es enthält keine Annahmen und ist []am Anfang mit gekennzeichnet, wie in
| presmises
|---
| stuff
|| []
||---
|| other stuff
| more stuff
Sie können nicht in einen geschachtelten Unterbeweis wiederholen, daher ist Folgendes ungültig:
| Q
|---
|| []
||---
|| Q R (BAD! NO! DON'T!)
Das wäre offensichtlich ein Trugschluss – von „ist der Fall“ zu „notwendigerweise der Fall“ zu gehen.
Nun zu den Inferenzregeln. []-Einführung:
| []
|---
| .
| .
| .
| Q
------ []I
[]Q
Es gibt auch eine []-Eliminierungsregel. Es ist die Ausnahme von dem Nicht-Wiederholen-Ding und es geht so:
| []Q
|| []
||---
------ []E
|| Q
Beachten Sie, dass dies nicht wirklich eine Eliminierung ist, nicht in der normalen Art und Weise, wie wir darüber denken. Was Sie wirklich erwarten würden, ist so etwas wie []Q -> Q, aber dies ist eigentlich ein Axiom, das zu K hinzugefügt wird, um System T zu machen.
Jetzt definiert Garson <>Q := ~[]~Q, aber ich möchte in der Lage sein, es primitiv einzuführen und zu eliminieren. Garson liefert eine abgeleitete Regel für die <>-Eliminierung:
<>P
| []
|---
|| P
|| .
|| .
|| .
|| Q
------ <>E
<>Q
Was sich zusammenfassen lässt
<>P
[](P -> Q)
------ <>E
<>Q
Ich konnte keine Inferenzregel für <>-introduction finden. Mir scheint jetzt, dass eine solche Regel nicht möglich ist, weil es keine Möglichkeit gibt, a priori herauszufinden, ob eine formale Aussage nur möglich ist oder nicht. Dies steht im Gegensatz zur Notwendigkeit – wir wissen a priori, dass jede Aussage, die in der nichtmodalen Logik beweisbar ist, notwendig ist.
Konifold
Schlucht
Konifold
Mauro ALLEGRANZA
Mauro ALLEGRANZA
Mauro ALLEGRANZA