Spezifische Wahl von Schlußregeln für den Prädikatenkalkül

Eine intuitive Antwort, in einer Welt aus Streichhölzern und Feuer und ohne Magie, dh aus nichts kann man kein Feuer machen.

Betrachten Sie eine Variable$x$ein Streichholz bedeuten. Lassen$A(x)$bedeutet „Stick$x$raucht" und$C$bedeutet "Es gibt Feuer".

Die Regel „wenn$A(x)\Rightarrow C$Dann$(\exists x A(x))\Rightarrow C$“ stellt das sehr Offensichtliche fest: „wenn Stock x raucht, dann gibt es Feuer“ bedeutet „wenn da etwas Stock ist$x$das raucht, dann ist da Feuer.“ Dieser Satz gilt in jedem Streichholzuniversum.

Betrachten Sie nun Ihre Regel "wenn$A(x)\Rightarrow C$Dann$(\forall x A(x))\Rightarrow C$". Darin heißt es: "Wenn Stock x raucht, dann gibt es Feuer" bedeutet auch, dass "wenn alle kleben$x$rauchen, dann gibt es Feuer". Diese Ableitung gilt nur in Modellen, die mindestens ein Objekt enthalten. Denn in einem leeren Universum, das keine Streichhölzer hat, rauchen alle Streichhölzer (die eigentlich keine sind). Es kann jedoch sein Kein Feuer ohne Streichhölzer!

Die zusätzlichen Regeln, die Sie angeben, sind tatsächlich gültig (auf nicht leeren Domänen). Der Grund dafür ist die Implikation$\forall x\, A(x) \Rightarrow \exists x\, A(x)$gilt (auf nicht-leeren Domains) - wenn ich mich richtig erinnere, wird dies manchmal als "existenzieller Import" bezeichnet.

Also wenn$A(x) \Rightarrow C$, dann haben wir beides$\forall x\, A(x)\Rightarrow \exists x\, A(x)$Und$\exists x\, A(x)\Rightarrow C$, So$\forall x\, A(x)\Rightarrow C$.

Und doppelt, wenn$C\Rightarrow A(x)$, dann haben wir beides$C\Rightarrow \forall x\, A(x)$Und$\forall x\, A(x)\Rightarrow \exists x\, A(x)$, So$C\Rightarrow \exists x\, A(x)$.

Aber davon bekommen wir das nicht$\exists$Und$\forall$"genauso handeln", weil die Regeln, die Sie in Ihrer Frage angegeben haben, die Bedeutung von nicht vollständig erfassen$\exists$Und$\forall$. Sie brauchen mehr Regeln.

Ich bin mir nicht sicher, welche Regeln Kleene verwendet, aber es gibt zwei gängige Ansätze:

1. Ein Ansatz besteht darin, auch die Umkehrungen Ihrer Regeln anzugeben: Wenn$\exists x\, A(x)\Rightarrow C$, Dann$A(x)\Rightarrow C$, und wenn$C\Rightarrow \forall x\, A(x)$, Dann$C\Rightarrow A(x)$(Wo$x$ist nicht frei$C$).

2. Ein anderer Ansatz besteht darin, die Axiome einzubeziehen$A(t)\Rightarrow \exists x\, A(x)$Und$\forall x\, A(x)\Rightarrow A(t)$, Wo$t$ist ein Begriff, der für ersetzt werden kann$x$.

Bei beiden Ansätzen werden Sie dies bemerken, wenn Sie versuchen, sie zu ersetzen$\exists$von$\forall$oder umgekehrt, die Regeln sind offensichtlich nicht solide.

Noch ein Kommentar: Der klassische Ansatz zur Logik erster Ordnung geht davon aus, dass jede Struktur einen nicht leeren Bereich hat. Aber diese Annahme ist nicht allgemeingültig. Wenn unsere Semantik für Logik erster Ordnung leere Domänen zulässt, dann scheitert der existenzielle Import: Wenn es keine gibt$x$s, dann$\forall x\, A(x)$ist vage wahr, während$\exists x\, A(x)$ist falsch.

Und ähnlich, wenn wir leere Domains zulassen, dann Ihre Versionen der Regeln, wo wir tauschen$\exists$Und$\forall$sind nicht mehr gültig. Frabalas Antwort gibt dafür ein sehr schönes intuitives Beispiel.