Beweis der Negation der universellen Quantifizierung

Sie haben in Schritt 6 einen Fehler gemacht. 3 ist keine universelle Quantifizierung, sondern eine Negation (das ¬ liegt außerhalb des ∀). Daher können Sie das ∀ nicht eliminieren.

Was Sie stattdessen tun müssen, ist, das ¬ zu eliminieren. Will man ¬ aus ¬ p eliminieren , nimmt man p an und arbeitet dann auf einen Widerspruch hin. Sie erhalten also:

6. Angenommen ∀x(¬S(x))

Jetzt können Sie ∀ auf x0 eliminieren:

7. ¬S(x0)

Dies in Kombination mit 5 ergibt uns

8. R(x0)

Dies steht aber im Widerspruch zu 4. Daher war die Annahme in 6 falsch, und daher muss ¬∀x(¬S(x)) gelten.

Betrachten Sie das folgende Argument

∀x(R(x) ∨ S(x)), ∃x(¬R(x)) ⊦ ¬∀x(¬S(x))

Meine Strategie besteht darin zu versuchen zu beweisen, dass ∀x(¬S(x)) ein Widerspruch ist und daher ¬∀x(¬S(x)) wahr sein muss.

Gute Strategie! Ein Beweis durch Negation.

Meine bisherige Lösung

1. | ∀x(R(x) ∨ S(x)) Prämisse

2. |_ ∃x(¬R(x)) Prämisse

3. | |_ ¬∀x(¬S(x)) Annahme

Was ist aus Ihrer Strategie geworden, ∀x(¬S(x)) anzunehmen? Hier sollten Sie dies tun. Auch hier erhebst du die erste Vermutung. (Die ersten beiden sind Prämissen.)

3. | |_ ∀x(¬S(x)) Annahme

4. | | |_ x0 ¬R(x0) ∃e 2
5. | | | R(x0) ∨ S(x0) ∀e 1
6. | | | ¬¬S(x0) ∀e 3

Nein, man kann den Universalquantor in ¬∀x(¬S(x)) nicht eliminieren, um ¬¬S(x0) zu erhalten. Verneinung hat Vorrang. Abgesehen davon, da Sie in Zeile sowieso ∀x(¬S(x)) hätten annehmen sollen, korrigieren wir nur Zeile 6, und es hätte wirklich die Annahme auf dem Block sein sollen: Es ist der Zeuge für das Universelle, das wir suchen zu negieren.

4. | | |_ [x0] ¬S(x0) ∀e 3
5. | | | ¬R(x0) ∃e 2
6. | | | R(x0) ∨ S(x0) ∀e 1

7. | | | |_ R(x0) Annahme
8. | | | | ⊥ ¬e 5, 7
9. | | | | ¬S(x) ⊥e 8

Okay. Sie richten Dinge für eine Disjunktionsbeseitigung ein. Belassen Sie es einfach bei Zeile acht.

7. | | | |_ R(x0) Annahme
8. | | | | ⊥ :¬e 5, 7
9. | | | R(x0) → ⊥ :→i 7-8
10. | | | |_ S(x0) : Annahme
11. | | | | ⊥ :¬e 4, 10
12. | | | S(x0) → ⊥ : →i 10-11
13. | | | ⊥ :∨e 6, 9, 12
14. | | ⊥ :[]e 4-13
15. | ¬∀x (¬S(x)) :¬i 3-14

Die Frage lautet: "Wie würde man in Szenarien wie dem obigen mit Negationen von Quantoren arbeiten?"

Ich werde zwei Beweise liefern, die bei der Beantwortung der Frage helfen können. Der erste wird ein indirekter Beweis sein, ähnlich dem Versuch im OP. Der zweite wird direkter sein.

Hier der erste Beweis:

Die Räumlichkeiten befinden sich in den ersten beiden Zeilen. In der dritten Zeile nehme ich die Negation dessen an, was ich zeigen möchte, um einen Widerspruch zu erhalten. In Zeile 9 erreiche ich den gewünschten Widerspruch, der zur Vervollständigung des Beweises in Zeile 10 führt.

In Zeile 4 verwende ich die zweite Prämisse. In Zeile 5 verwende ich die erste Prämisse. Diese erzeugen schnell einen Widerspruch.

Der zweite Beweis ist direkter.

Die ersten beiden Zeilen sind die Prämisse. In Zeile 3 beginne ich mit dem Prozess zur vollständigen existenziellen Eliminierung. Dazu muss ich eine Annahme treffen, die in Zeile 15 entladen wird, um eine existenzielle Eliminierung zu ermöglichen.

Unter Verwendung der ersten Prämisse betrachte ich die beiden Fälle "Ra" und "Sa". Ich möchte, dass beide Fälle mir (1) das gleiche Ergebnis und (2) ein Ergebnis liefern, das ich verwenden kann. Das gewünschte Ergebnis ist "¬¬Sa". Mit diesen doppelten Negativen kann ich einen existenziellen Quantor einführen und dann mit einer Umwandlung von Quantoren eine dieser Negationen aus einem universellen Quantor herausbewegen.

Weitere Informationen zur Funktionsweise dieser Regeln im Zusammenhang mit dem von mir verwendeten Proof Checker finden Sie unter forall x: Calgary Remix .

Verweise

Kevin Klements JavaScript/PHP-Beweiseditor und -prüfer im Fitch-Stil für natürliche Deduktion http://proofs.openlogicproject.org/

PD Magnus, Tim Button mit Ergänzungen von J. Robert Loftis, remixt und überarbeitet von Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/