Natürliche Abzugsbeweishilfe!

Eine frühere Version der Frage bestand aus fünf Teilen:

1. ∀x(Px ∨ Q) ⊢ (∀xPx ∨ Q)
2. ∀xPx → Q ⊢ ∃x(Px → Q)
3. ∀x∀y(Rxy → ¬x = y) ⊢ ¬∃xRxx
4. ∀x(∃yPxy → ∀yPyx) ⊢ ∃x∃yPxy → ∀x∀yPxy
5. ∃x∃y∀z(x = z ∨ y = z) ⊢ ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))

Was in der Frage bleibt, ist nur Teil 5.

---

Zu viele ...

Hinweis zu 1) :

1) ∀x(Px ∨ Q) --- Prämisse

2) Px ∨ Q --- bilden 1) durch ∀-elim

3) ¬Q --- angenommen [a]

4) ∃x¬Px --- angenommen [b]

5) Q --- angenommen [c] aus 2) für ∨-elim

6) ⊥ --- Widerspruch, aus 3) und 5)

7) ¬¬Q --- von 3) und 6) durch ¬-Intro, Entladung [a]

8) Q --- aus 7) durch ¬¬-elim

9) ∀xPx ∨ Q --- von 8) durch ∨-Intro

10) Px --- angenommen [d] aus 2) für ∨-elim

11) ¬Px --- angenommen [e] aus 4) für ∃-elim

12) ⊥ --- Widerspruch, aus 10) und 11) und Entladung [e] durch ∃-elim

13) ¬∃x¬Px --- aus 4) und 12) per ¬-Intro, Entladung [b]

14) ∀Px --- aus 13) mit der Unterableitung ¬∃x¬ ⊢∀x : nimm ¬Px an, und dann ∃x¬Px durch ∃-Intro. Mit Widerspruch und doppelter Negation leite Px ab, löse die Annahme auf und schließe mit ∀xPx durch ∀-Intro.

15) ∀Px ∨ Q --- aus 14) durch ∨-Intro

16) ∀Px ∨ Q --- aus 2) und 5)-9) und 10)-15) durch ∨-elim, Entladung von [c] und [d].

---

---

Hinweis zu 2) :

1) ∀xPx → Q --- Prämisse

2) Px --- angenommen [a]

3) ∃x¬Px --- angenommen [b]

4) ¬Px --- angenommen [c] aus 3) für ∃-elim

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

6) ⊥ --- aus 3), 4) und 5) durch ∃-elim, Entladung [c]

7) ¬∃x¬Px --- aus 3) und 6) durch ¬¬-elim, Entladung [b]

8) ∀Px --- aus 7) mit der Unterableitung ¬∃x¬ ⊢∀x

9) Q --- aus 1) und 8) durch →-elim

10) Px → Q$ --- aus 2) und 9) durch →-Intro, Entladung [a]

11) ∃x(Px → Q) --- aus 10) durch ∃-Intro.

---

---

Hinweis zu 3) :

1) ∀x∀y(Rxy → ¬x = y) --- Prämisse

2) Rxx --- angenommen [a]

3) Rxx → ¬ x = x --- von 1 durch ∀-elim

4) ¬ x = x --- aus 2) und 3) durch →-elim

5) x = x --- Axiom für Gleichheit

6) ¬Rxx --- aus 2) und Widerspruch, per ¬-Intro, Entladung [a]

7) ∀x¬Rxx --- von 6) durch ∀-Intro

Jetzt müssen wir noch die Unterableitung hinzufügen: ∀x¬ ⊢ ¬∃x.

---

---

Der letzte ist lang und langweilig, aber ziemlich einfach.

Hinweis zu 5) :

1) ∃x∃y∀z(x = z ∨ y = z) --- Prämisse

2) ¬∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) --- nimm die Negation der Konklusion an und suche nach einem Widerspruch: falls gefunden, folgt auf das Ergebnis ¬¬ -elim

3) ∀z(a = z ∨ b = z) --- angenommen aus 1) für ∃-elim zweimal

4) ∃x∃y ¬(¬x = y → ∀z(x = z ∨ y = z)) --- aus 2), wieder mit der Äquivalenz der Quantoren spielend

5) ¬(¬c = d → ∀z(c = z ∨ d = z)) --- angenommen aus 4) für ∃-elim zweimal

6) ¬c = d ∧ ¬∀z(c = z ∨ d = z) --- aus 6) durch tautologische Äquivalenz

7) ¬c = d --- aus 6) durch ∧-elim

8) ¬∀z(c = z ∨ d = z) --- aus 6) durch ∧-elim

9) ∃z ¬(c = z ∨ d = z) --- aus 9) wieder durch Quantorenäquivalenz

10) ¬(c = e ∨ d = e) --- angenommen aus 9) für ∃-elim

11) ¬c = e ∧ ¬d = e --- aus 10) durch tautologische Äquivalenz

12) ¬c = e --- aus 11) durch ∧-elim

13) ¬d = e --- aus 11) durch ∧-elim

Jetzt müssen wir 3) ∀z(a = z ∨ b = z) drei Mal mit c,d,e instanziieren, um zu erhalten:

14) a = c ∨ b = c

15) a = d ∨ b = d

16) a = e ∨ b = e

und mit 7), 12) und 13) (einfache aber langweilige Anwendung von ∨-elim) den gewünschten Widerspruch erhalten.

Was wir bekommen ist:

20) ⊥

das schließt alle obigen ∃-elims und entlädt die entsprechenden Annahmen.

21) ∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) --- aus 2) und 20) durch ¬¬-elim.

Eine frühere Version der Frage bestand aus fünf Teilen:

1. ∀x(Px ∨ Q) ⊢ (∀xPx ∨ Q)
2. ∀xPx → Q ⊢ ∃x(Px → Q)
3. ∀x∀y(Rxy → ¬x = y) ⊢ ¬∃xRxx
4. ∀x(∃yPxy → ∀yPyx) ⊢ ∃x∃yPxy → ∀x∀yPxy
5. ∃x∃y∀z(x = z ∨ y = z) ⊢ ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))

Was in der Frage bleibt, ist nur Teil 5.

---

Die Einzelheiten Ihres Beweises hängen davon ab, wie genau das Beweissystem, mit dem Sie arbeiten, die Regeln definiert hat.

Hier sind die Beweise für 1), 2), 3) und 4) unter Verwendung des Fitch-Beweissystems, wie es in Sprache, Beweis und Logik definiert ist (dies ist ein Buch und ein Softwarepaket):

Für 5) müssen Sie eindeutig ein ∃ Elim für die Prämisse und ein ∀ Intro für die Schlussfolgerung machen. Für dieses Problem spielt es eigentlich keine Rolle, in welcher Reihenfolge Sie sie ausführen. Das heißt, Sie können dies entweder wie folgt einrichten:

oder so:

OK, lassen Sie uns einfach mit letzterem arbeiten. Da wir jetzt nach einem weiteren ∀ suchen, machen wir ein weiteres ∀-Intro:

Um diese Disjunktion zu erhalten, führen wir nun einen Widerspruchsbeweis durch. Warum? Denn wenn Sie konzeptionell über dieses Problem nachdenken: Wir wissen, dass jedes Objekt entweder gleich a oder b ist (oder beides, da a und b dasselbe Objekt sein können). Wir wissen also, dass es höchstens zwei Objekte in der Domäne gibt. Daher ist die Schlussfolgerung sinnvoll: Wenn es zwei verschiedene Objekte c und d gibt, muss alles entweder dem einen oder dem anderen entsprechen. Okay, aber wie kann man das beweisen? Nun, nehmen Sie irgendein Objekt, z. Wir wissen, dass e gleich a oder b oder beides ist. Wenn Sie nun von einer Disjunktion P v Q zu einer Disjunktion R v S gehen, können Sie normalerweise eine der gewünschten Disjunktionen (R) zu einer der Disjunkte, die Sie haben (z. B. Q), zurückverfolgen, während die andere Sie disjunkt will (S) kommt von dem anderen, den du hast (P). Sie können also einen Fallbeweis (v Elim) durchführen, um dies zu tun. Aber hier wird diese Strategie nicht funktionieren: wenn e = a, können wir sagen, dass e = c? Nein. Auch nicht, dass e = d. Ja, es muss definitiv das eine oder andere sein, aber wir können einfach nicht sagen, welches. OK, also wird ein direkter Proof by Cases nicht funktionieren. Verwenden Sie in diesem Fall die andere gängige Strategie, um die Disjunktion zu beweisen: Beweis durch Widerspruch:

OK, und jetzt sollte es ziemlich einfach sein. Wir wissen, dass c, d und e alle a oder b sind, und jetzt geht es nur noch darum, all diese Disjunktionen durchzugehen und jedes Mal einen Widerspruch zu beweisen. Hier die Grundeinstellung:

Und hier ist eine Hälfte ausgearbeitet:

Mühsam, aber ziemlich einfach. Viel Glück!

Die Prämisse ∃x∃y∀z(x = z ∨ y = z)besagt, dass es höchstens zwei unterschiedliche Werte in der Domäne gibt.

Die Schlussfolgerung ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))besagt, dass es für zwei verschiedene Werte in der Domäne keinen dritten gibt.

Natürlich müssen wir existentielle Eliminierung und universelle Einführung nutzen.

∃-elim wird hier schwierig.

Der „Trick“ besteht darin, fünf angenommene Begriffe zu verwenden. Zwei Terme als Zeugen für die existentiellen Eliminierungen ( a, b), und drei willkürliche Terme für die Einleitungen ( c, d, e).

Um die Schlussfolgerung aus der Prämisse zu beweisen: Nehmen Sie den Zeugen für die Prämisse (nehmen Sie an aund bwo ∀z(a = z ∨ b = z), nehmen Sie willkürliche Werte ( c, d, und e) und zeigen Sie (unter Verwendung der universellen Eliminierung von jedem), dass wenn b, und cunterschiedlich angenommen werden, dass folgt, dass esein muss das eine oder andere davon über einige verschachtelte Disjunktionsbeseitigungen (und Gleichheitsbeseitigungen).

Kurz gesagt: Seit (a = c ∨ b = c), (a = d ∨ b = d), und (a = e ∨ b = e)über universelle Eliminierung, also(c = e ∨ d = e)

---

Kurz gesagt: Es ist langweilig und repetitiv, aber ...

    |_ ∃x∃y∀z(x = z ∨ y = z)                P
    |  |_ [a,b] ∀z(a = z ∨ b = z)           H
    |  |  |_ [c,d]                          H
    |  |  |  a = c ∨ b = c                 ∀E
    |  |  |  a = d ∨ b = d                 ∀E
    |  |  |  |_ ¬c = d                      H
    |  |  |  |  |_ [e]                      H
    |  |  |  |  |  a = e ∨ b = e           ∀E
    |  |  |  |  |  |_ a = e                 H
    |  |  |  |  |  |  |_ a = c              H
    |  |  |  |  |  |  |  c = e             =E
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨I
    |  |  |  |  |  |  +
    |  |  |  |  |  |  |_ b = c              H
    |  |  |  |  |  |  |  |_ a = d           H
    |  |  |  |  |  |  |  |  d = e          =E
    |  |  |  |  |  |  |  |  c = e ∨ d = e  ∨I
    |  |  |  |  |  |  |  +
    |  |  |  |  |  |  |  |_ b = d           H
    |  |  |  |  |  |  |  |  c = d          =E
    |  |  |  |  |  |  |  |  #              ¬E
    |  |  |  |  |  |  |  |  c = e ∨ d = e   X
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨E
    |  |  |  |  |  |  c = e ∨ d = e        ∨E
    |  |  |  |  |  +
    |  |  |  |  |  |_ b = e                 H
    |  |  |  |  |  |  |_ a = c              H
    |  |  |  |  |  |  |  |_ a = d           H
    |  |  |  |  |  |  |  |  c = d          =E
    |  |  |  |  |  |  |  |  #              ¬E
    |  |  |  |  |  |  |  |  c = e ∨ d = e   X
    |  |  |  |  |  |  |  +
    |  |  |  |  |  |  |  |_ b = d           H
    |  |  |  |  |  |  |  |  d = e          =E
    |  |  |  |  |  |  |  |  c = e ∨ d = e  ∨I
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨E
    |  |  |  |  |  |  +
    |  |  |  |  |  |  |_ b = c              H
    |  |  |  |  |  |  |  c = e             =E
    |  |  |  |  |  |  |  c = e ∨ d = e     ∨I
    |  |  |  |  |  |  c = e ∨ d = e        ∨E
    |  |  |  |  |  c = e ∨ d = e           ∨E
    |  |  |  |  ∀z (c = z ∨ d = z)         ∀I
    |  |  |  ¬c = d → ∀z (c = z ∨ d = z)   →I
    |  |  ∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) ∀I 
    |  ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))    ∃E