¡Ayuda de prueba de deducción natural!

Una versión anterior de la pregunta tenía cinco partes:

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))

Lo que queda en la pregunta es solo la parte 5.

---

demasiados ...

Sugerencia para 1):

1) ∀x(Px ∨ Q) --- premisa

2) Px ∨ Q --- forma 1) por ∀-elim

3) ¬Q --- asumido [a]

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

5) Q --- asumido [c] de 2) para ∨-elim

6) ⊥ --- contradicción, de 3) y 5)

7) ¬¬Q --- de 3) y 6) por ¬-intro, descargando [a]

8) Q --- de 7) por ¬¬-elim

9) ∀xPx ∨ Q --- de 8) por ∨-introducción

10) Px --- asumido [d] de 2) para ∨-elim

11) ¬Px --- asumido [e] de 4) para ∃-elim

12) ⊥ --- contradicción, de 10) y 11) y descarga [e] por ∃-elim

13) ¬∃x¬Px --- de 4) y 12) por ¬-introducción, descargando [b]

14) ∀Px --- de 13) usando la subderivación ¬∃x¬ ⊢∀x : suponga ¬Px, y luego ∃x¬Px por ∃-intro. Con contradicción y doble negación, obtenga Px, descargando la suposición, y concluya con ∀xPx por ∀-intro.

15) ∀Px ∨ Q --- de 14) por ∨-introducción

16) ∀Px ∨ Q --- de 2) y 5)-9) y 10)-15) por ∨-elim, descargando [c] y [d].

---

---

Sugerencia para 2):

1) ∀xPx → Q --- premisa

2) Px --- asumido [a]

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

4) ¬Px --- asumido [c] de 3) para ∃-elim

5) ⊥ --- contradicción, de 2) y 4)

6) ⊥ --- de 3), 4) y 5) por ∃-elim, descargando [c]

7) ¬∃x¬Px --- de 3) y 6) por ¬¬-elim, descargando [b]

8) ∀Px --- de 7) usando la subderivación ¬∃x¬ ⊢∀x

9) Q --- de 1) y 8) por →-elim

10) Px → Q$ --- de 2) y 9) por →-intro, descargando [a]

11) ∃x(Px → Q) --- de 10) por ∃-intro.

---

---

Sugerencia para 3):

1) ∀x∀y(Rxy → ¬x = y) --- premisa

2) Rxx --- asumido [a]

3) Rxx → ¬ x = x --- de 1 por ∀-elim

4) ¬ x = x --- de 2) y 3) por →-elim

5) x = x --- axioma de igualdad

6) ¬Rxx --- de 2) y contradicción, por ¬-intro, descargando [a]

7) ∀x¬Rxx --- de 6) por ∀-intro

Ahora tenemos que sumar la subderivación: ∀x¬ ⊢ ¬∃x.

---

---

El último es largo y tedioso, pero bastante sencillo.

Sugerencia para 5):

1) ∃x∃y∀z(x = z ∨ y = z) --- premisa

2) ¬∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) --- asumir la negación de la conclusión y buscar una contradicción: si se encuentra, el resultado seguirá por ¬¬ -eliminar

3) ∀z(a = z ∨ b = z) --- asumido de 1) para ∃-elim dos veces

4) ∃x∃y ¬(¬x = y → ∀z(x = z ∨ y = z)) --- de 2), jugando de nuevo con la equivalencia de cuantificadores

5) ¬(¬c = d → ∀z(c = z ∨ d = z)) --- asumido de 4) para ∃-elim dos veces

6) ¬c = d ∧ ¬∀z(c = z ∨ d = z) --- de 6) por equivalencia tautológica

7) ¬c = d --- de 6) por ∧-elim

8) ¬∀z(c = z ∨ d = z) --- de 6) por ∧-elim

9) ∃z ¬(c = z ∨ d = z) --- de 9) de nuevo por equivalencia de cuantificadores

10) ¬(c = e ∨ d = e) --- asumido de 9) para ∃-elim

11) ¬c = e ∧ ¬d = e --- de 10) por equivalencia tautológica

12) ¬c = e --- de 11) por ∧-elim

13) ¬d = e --- de 11) por ∧-elim

Ahora tenemos que instanciar 3) ∀z(a = z ∨ b = z) tres veces, con c,d,e respectivamente, para obtener:

14) un = do ∨ segundo = do

15) un = re ∨ segundo = re

16) un = mi ∨ segundo = mi

y finalmente obtener la contradicción deseada con 7), 12) y 13) (aplicación simple pero aburrida de ∨-elim).

Lo que obtenemos es:

20) ⊥

que cierra todos los ∃-elim anteriores, descargando los supuestos correspondientes.

21) ∀x∀y(¬x = y → ∀z(x = z ∨ y = z)) --- de 2) y 20) por ¬¬- elim.

Una versión anterior de la pregunta tenía cinco partes:

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))

Lo que queda en la pregunta es solo la parte 5.

---

Los detalles de su prueba dependerán de cómo exactamente el sistema de prueba con el que está trabajando haya definido las reglas.

Estas son las pruebas para 1), 2), 3) y 4) usando el sistema de prueba de Fitch como se define en Lenguaje, Prueba y Lógica (este es un libro y un paquete de software):

Para 5), ​​claramente necesita hacer un ∃ Elim en la premisa y un ∀ Intro para la conclusión. Para este problema, en realidad no importa en qué orden los hagas. Es decir, puede configurar esto de esta manera:

o así:

OK, vamos a trabajar con este último. Ahora, como estamos buscando otro ∀, haremos otro ∀ Intro:

Ahora, para obtener esa disyunción, haremos una prueba por contradicción. ¿Por qué? Porque si piensas conceptualmente en este problema: sabemos que todo objeto es igual a a o b (o ambos, ya que a y b pueden ser el mismo objeto). Entonces, sabemos que hay como máximo dos objetos en el dominio. Por lo tanto, la conclusión tiene sentido: si hay dos objetos diferentes c y d, entonces todo debe ser igual al uno o al otro. Bien, pero ¿cómo probar eso? Bueno, toma cualquier objeto e. Sabemos que e es igual a a o b o ambos. Ahora, por lo general, cuando pasa de una disyunción P v Q a una disyunción R v S, puede rastrear una de las disyuntivas que desea (R) hasta una de las disyuntivas que tiene (digamos, Q), mientras que la otra disyunción le querer (S) viene del otro que tienes (P). Entonces, puede hacer una prueba por casos (v Elim) para hacer esto. Pero aquí, esa estrategia no va a funcionar: si e = a, ¿podemos decir que e = c? No. Ni que e = d. Sí, definitivamente tiene que ser uno u otro, pero no podemos decir cuál. Bien, entonces una prueba directa por casos no va a funcionar. Bueno, en ese caso usa la otra estrategia común para probar la disyunción: Prueba por contradicción:

OK, y ahora debería ser bastante sencillo. Sabemos que c, d y e son todas a o b, y ahora solo es cuestión de pasar por todas esas disyunciones, probando una contradicción cada vez. Aquí está la configuración básica:

Y aquí está la mitad resuelta:

Tedioso, pero bastante sencillo. ¡Buena suerte!

La premisa ∃x∃y∀z(x = z ∨ y = z)dice que existen como máximo dos valores distintos en el dominio.

La conclusión ∀x∀y(¬x = y → ∀z(x = z ∨ y = z))dice que para cualesquiera dos valores distintos en el dominio, no existe un tercero.

Claramente necesitamos utilizar la eliminación existencial y la introducción universal.

∃-elim aquí será complicado.

El 'truco' es usar cinco términos supuestos. Dos términos como testigos para las eliminaciones existenciales ( a, b), y tres términos arbitrarios para las introducciones ( c, d, e).

Para probar la conclusión a partir de la premisa: tome el testigo por la premisa (suponga ay bdonde ∀z(a = z ∨ b = z), tome valores arbitrarios ( c, d, y e) y (usando eliminación universal para cada uno) muestre que cuando b, y cse suponen distintos, que se sigue que edeben ser uno u otro de ellos, a través de algunas eliminaciones de disyunción anidadas (y eliminaciones de igualdad).

En resumen: Dado que (a = c ∨ b = c), (a = d ∨ b = d)y (a = e ∨ b = e)por eliminación universal, por lo tanto(c = e ∨ d = e)

---

En largo: Es tedioso y repetitivo, pero...

    |_ ∃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