Wie man '∃xP(x)' aus '¬∀x(P(x)→Q(x))' beweist

Wie würde ein formaler Fitch-Beweis dafür aussehen?

Ich habe ¬∀x(P(x)→Q(x)) und muss daraus ∃xP(x) ableiten.

Ich habe damit angefangen, aber ich weiß nicht, ob ich das Richtige tue und wie ich von dort aus weitermachen soll:

Geben Sie hier die Bildbeschreibung ein

EDIT: Tat es (siehe Antwort)

Bisher keine Antworten auf Englisch ausgeschrieben. Ist nicht der springende Punkt, dass, wenn es kein $x$ gäbe, so dass $P(x)$, dann $P(x)$ für alle $x$ falsch wäre und somit absolut alles implizieren würde?

Antworten (4)

Aufgelöst! Mir wurde klar, dass ich nirgendwohin führte, wenn ich das Gegenteil von dem annahm, was mir als Prämisse gegeben wurde ... Ich musste offensichtlich das Gegenteil von dem annehmen, was ich zu beweisen versuchte:

Geben Sie hier die Bildbeschreibung ein

In der Tat. Sie haben eine richtige Lösung. Sie können jetzt Ihre eigene Antwort akzeptieren, um diese Frage zu schließen.

1) ¬∀x(P(x) → Q(x)) --- Prämisse

2) ¬∃xP(x) --- angenommen [a]

3) P(x) --- angenommen [b]

4) ∃xP(x) --- von 3) durch ∃ -Einleitung

5) ⊥ --- Widerspruch : aus 2) und 4)

6) Q(x) --- aus 5) durch ⊥ -elim

7) P(x) → Q(x) --- aus 3) und 6) durch → -intro, Entladung [b]

8) ∀x(P(x) → Q(x)) --- von 7) durch ∀ -Intro

9) ⊥ --- Widerspruch : aus 1) und 8)

10) ∃xP(x) --- aus 2) durch doppelte Negation (oder ¬ -elim ), Entladen von [a].

Der folgende Beweis ist derselbe wie der von Mauro ALLEGRANZA, aber er verwendet Klements Beweisprüfer im Fitch-Stil. Beschreibungen der Regeln sind in forallx . Beide sind online verfügbar und unten aufgeführt. Sie können als ergänzendes Material zu dem, was Sie derzeit verwenden, hilfreich sein.

Möglicherweise müssen Sie in Ihrem Proof-Checker Widersprüche als Konjunktionen widersprüchlicher Aussagen darstellen. Dieser Beweisprüfer erfordert nur, den Widerspruch als "⊥" zu notieren und die widersprüchlichen Zeilen aufzulisten, wie ich es in den Zeilen 5 und 9 getan habe.

Geben Sie hier die Bildbeschreibung ein

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/

Ich habe es geschafft, aber mein Ergebnis unterscheidet sich geringfügig von Ihrem. Ich habe Ihren aus Neugier ausprobiert, und er funktioniert nicht in dem Fitch-Programm, das ich habe. Ich bin verblüfft über die Tatsache, dass Ihr Beweisprüfer Ihnen erlaubt hat, die vorübergehende Annahme 'a' außerhalb ihres Unterbeweises zu exportieren!
@ 35308 Sie könnten diesen Unterbeweis (Zeile 3-6) so betrachten, als würde er dasselbe sagen wie die bedingte Anweisung in Zeile 7 "Pa > Qa". Unter der Annahme Pa kann ich Qa mit dem ableiten, was verfügbar ist (nämlich Zeile 2). Der Unterbeweis zeigte nur, wie das gemacht wurde, und der Beweisprüfer verlangte, dass ich das zeige, bevor ich Zeile 7 verwende.
Das Problem ist, dass es Ihnen wirklich nicht erlaubt sein sollte, einen neuen freien Begriff „a“ einzuführen, ohne einen neuen Kontext zu schaffen, um ihn zu isolieren.

Pr. ~∀x(P(x)->Q(x))

2. ∃x~(P(x)->Q(x)) ~ Universal out Pr.

3. ~(P(a)->Q(a)) Existential out (x/a) 2

4. P(a)&~Q(a) ~ bedingtes Aus 3

5. P(a) Konjunktion aus 4

6. ∃xP(x) Existenziell in 5

Wie man '∃xP(x)' aus '¬∀x(P(x)→Q(x))' beweist
AntwortenHierDatenschutz-Bestimmungen1y, 0v