Wie beweist man "Möglicherweise P, wenn notwendigerweise P" in der Kripke-Modallogik?

Ich möchte innerhalb der Kripke-Modallogik Folgendes beweisen:

□P → ◇P

Das ist keine Hausaufgabe, sondern einfach das erste, was ich beweisen möchte. Ich konnte komplexere Theoreme wie □(P→Q)&◇P → ◇Q beweisen, aber ein direkter Beweis der Notwendigkeit, der die Möglichkeit impliziert, entzieht sich mir immer noch.

Auch ein Hinweis in die richtige Richtung wird sehr geschätzt.

Beachten Sie, dass wir in □(P→Q)&◇P → ◇Q wissen, dass P-Welten Q-Welten aus □(P→Q) sind, und ◇P die Existenz mindestens einer P-Welt garantiert, also die Der gesamte Vordersatz impliziert schließlich die Existenz einer Q-Welt (◇Q). (All dies ist natürlich relativ zu einem bestimmten Punkt in einem Modell.)

Antworten (3)

Zum Glück kann man es nicht beweisen. Es ist ungültig.

Gegenbeispiel. Betrachten Sie ein Modell M mit einer einzigen Welt w ∈ |M| so dass es keinen reflexiven Pfeil auf w gibt (dh ¬wRw). Das gibt uns die Tatsache, dass: (M, w) |= ▢ P, weil es vage wahr ist, dass für alle Welten v ∈ |M| zugänglich von w (wRv), haben wir (M, v) |= P. Daraus können wir schließen, dass (M, w) |= ▢ P. Aber es ist nicht so, dass es eine Welt v ∈ | gibt M| die von w zugänglich ist und so ist, dass (M, v) |= P (Sie wissen, dass es nur eine einzige Welt gibt und sie von sich selbst aus nicht zugänglich ist). Wir können also nicht schließen, dass (M, w) |= ♢P.

Die Begründung ist ähnlich wie bei den Quantoren ∀, ∃ üblich. Wenn Sie eine universell quantifizierte Formel φ (dh ∀φ) haben und diese in einem leeren Bereich interpretieren, ist sie erfüllt. Aber der existenzielle Wille nicht. Beachten Sie auch, dass selbst wenn Sie einen nicht leeren Diskursbereich haben, es immer noch der Fall sein kann, dass die Interpretation I von φ speziell leer ist, sodass die universellen Abschlüsse von φ möglicherweise immer noch leer als wahr bewertet werden, während die existentiellen nicht (vorausgesetzt, dass kein Objekt in die Erweiterung von φ unter dem I fällt).

Könnte man einfacher sagen, dass bei einem Modell mit genau null Welten für jedes P □P vage wahr, aber ◇P falsch ist?
Haha, naja, wenn das so einfach ist, kann man sogar sagen: In einem Modell ohne Welten ist jede Formel φ gültig, denn für jedes spitze Modell (M, w) gilt: (M, w) |= φ . Sicher!
Was ist die Motivation, dieses Verhalten hier zu wählen? Ich kann sehen, dass man Quantoren so definieren möchte, aber das bedeutet nicht, dass man ihre Definition zum Definieren von Modaloperatoren verwenden sollte. Gibt es schwerwiegende Folgen dieser Entscheidung? Warum kann die Definition von □ (und/oder ◇) in Bezug auf die möglichen Welten nicht geändert werden, damit die OPs-Aussage wahr ist?
Mit anderen Worten, wenn Sie sagen "Wenn Sie eine universell quantifizierte Formel φ (dh ∀φ) haben, wenn Sie sie in einem leeren Bereich interpretieren, wird sie erfüllt sein", warum ist diese Verdinglichung der möglichen Welten - sie als zu nehmen nicht realer als die Modaloperatoren, die das Hauptanliegen sind.
@Lucas Der Grund ist, dass die Quantoren ein wesentlicher Bestandteil der üblichen Semantik der Modaloperatoren sind. Nun, wie Shane im obigen Kommentar vorgeschlagen hat, können Sie einfach Einschränkungen für die Zugänglichkeitsbeziehung hinzufügen, um Ihre Intuitionen über die Beziehung zwischen Kästchen und Diamanten widerzuspiegeln. Wenn Sie zum Beispiel wollen, dass Notwendigkeit Möglichkeit impliziert, dann möchten Sie Axiom D zum Kern hinzufügen. Angenommen, Sie arbeiten mit Wissen (oder Beweisbarkeit), Sie übernehmen Axiom 4, um die Intuition zu erfassen, dass: Wenn Sie P kennen (oder bewiesen haben), dann wissen (oder bewiesen haben), dass Sie P kennen (oder bewiesen haben). Usw
Sagen Sie gerade "das sind die Axiome der Kripke-Semanitik"? Weil meine Frage ist, ob sie gute Axiome sind, insbesondere ob es "Kosten" gibt, es anders zu machen, obwohl ich verstehe, dass es nicht unbedingt eine Frage ist, die einfach zu beantworten ist.
Ich bin mir nicht sicher, was die Alternative ist. Die relationale Semantik der Modaloperatoren wird anhand der Quantoren erklärt. Ich kenne algebraische Ansätze, aber das Verbot von Variablen und die nur implizite Quantifizierung lenken nicht von der Tatsache ab, dass sie auf einer bestimmten Ebene benötigt werden. Ich vermute, dass ein technischer Vorschlag aus Ihren Sorgen extrahiert werden könnte, aber ich bin mir nicht sicher, wie ich das selbst machen soll. Denken Sie, dass die Kripke-Semantik zu liberal ist? Ich mag die Idee, dass es liberal ist und wir es durch die Axiome einschränken können. Dem müssen wir natürlich nicht zustimmen.

Noch ein Hinweis in die richtige Richtung: Es stimmt nicht, dass „die schwächste Logik, die diese Formel beweist, T ist“. Eher die schwächste Logik mit dieser Eigenschaft ist D, dessen Frames F = W, R (ich vermisse LaTex hier so sehr!) seriell sind , das heißt für jedes Mitglied w von W gibt es ein w' aus W, so dass wRw'. Tatsächlich charakterisiert die Formel des OP die Klasse der seriellen Frames: Ein Frame ist seriell, wenn die Formel in diesem Frame gültig ist (gültig in jedem Modell, das auf diesem Frame basiert). D ist eine echte Teillogik von T, da jeder T-Frame ein D-Frame ist, aber das T-Axiom nicht D-gültig ist.

Tatsächlich ist D das Minimum. In Bezug auf LaTeX, insbesondere für die Modallogik, würden einige Mittel zum Zeichnen von gerichteten Graphen die Dinge so viel einfacher zu erklären machen. Für die Logik im Allgemeinen schlage ich vor, dass Sie sich mit dem HTML-Zeichensatz vertraut machen. Auch die <sub><sup><kbd>-Tags sind praktisch. Viel Glück.
Danke @sequitur, dass du meinen Fehler erkannt hast. Jeder reflexive Rahmen ist seriell, aber nicht umgekehrt. Habe meinen fehlerhaften Kommentar oben gelöscht.

[]p -> <>p ist nur im seriellen Frame gültig.

nehmen wir an, dass x []p ist und x keinen Nachfolger hat.

dann hat x keinen Nachfolger bedeutet, dass <>p für x ungültig ist, weil x keinen Nachfolger hat

Nicht relevant, aber:

Serienmäßig gilt:

x[]p: Sei xRy wobei y Bewertet (p) ist und so Also: x<>p

Wie beweist man "Möglicherweise P, wenn notwendigerweise P" in der Kripke-Modallogik?
AntwortenHierDatenschutz-Bestimmungen1y, 0v