Demostración de la negación de la cuantificación universal

Cometió un error en el paso 6. Nr. 3 no es una cuantificación universal, es una negación (el ¬ está fuera del ∀). Por lo tanto, no puedes eliminar el ∀.

En cambio, lo que debe hacer es eliminar el ¬. Si quieres eliminar ¬ de ¬ p , asumes p y luego trabajas hacia una contradicción. Entonces obtienes:

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

Ahora puedes eliminar ∀ en x0:

7. ¬S(x0)

Esto en combinación con 5 nos da

8. R(x0)

Pero esto está en contradicción con 4. Por lo tanto, la suposición en 6 era incorrecta y, por lo tanto, debe cumplirse que ¬∀x(¬S(x)).

Considere el siguiente argumento

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

Mi estrategia es tratar de demostrar que ∀x(¬S(x)) es una contradicción y, por lo tanto, ¬∀x(¬S(x)) debe ser verdadera.

¡Buena estrategia! Una prueba por negación.

Mi solución hasta ahora

1. | ∀x(R(x) ∨ S(x)) Premisa

2. |_ ∃x(¬R(x)) Premisa

3. | |_ ¬∀x(¬S(x)) Suposición

¿Qué pasó con tu estrategia de asumir ∀x(¬S(x)) ? Aquí es donde debes hacerlo. También aquí es donde planteas la primera suposición. (Los dos primeros son premisas).

3. | |_ ∀x(¬S(x)) Suposición

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

No, no puedes eliminar el cuantificador universal en ¬∀x(¬S(x)) para obtener ¬¬S(x0). La negación tiene precedencia. Aparte de eso, ya que de todos modos, deberías haber asumido ∀x(¬S(x)) en la línea, solo corregiremos la línea 6, y realmente debería haber sido la suposición en el bloque: es el testigo del universal que buscamos. negar

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

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

Bueno. Está preparando las cosas para una eliminación de la disyunción. Solo déjalo en la línea ocho.

7. | | | |_ R(x0) Suposición
8. | | | | ⊥ :¬e 5, 7
9. | | | R(x0) → ⊥ :→i 7-8
10. | | | |_ S(x0) :Suposición
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

La pregunta es: "¿Cómo se trabajaría con negaciones de cuantificadores en escenarios como el anterior?"

Proporcionaré dos pruebas que pueden ayudar a responder la pregunta. La primera será una prueba indirecta similar al intento en el OP. El segundo será más directo.

Aquí está la primera prueba:

El local está en las dos primeras líneas. En la tercera línea asumo la negación de lo que quiero mostrar para obtener una contradicción. Llego a la contradicción deseada en la línea 9 que conduce a la finalización de la prueba en la línea 10.

En la línea 4 uso la segunda premisa. En la línea 5 uso la primera premisa. Estos generan rápidamente una contradicción.

La segunda prueba es más directa.

Las dos primeras líneas son la premisa. En la línea 3 empiezo el proceso para completar la eliminación existencial. Para hacer eso tengo que hacer una suposición que será descargada en la línea 15 permitiendo la eliminación existencial.

Usando la primera premisa considero los dos casos "Ra" y "Sa". Quiero que ambos casos me den (1) el mismo resultado y (2) un resultado que pueda usar. El resultado que quiero es "¬¬Sa". Tener esos dobles negativos me permite introducir un cuantificador existencial y luego, con una conversión de cuantificadores, mover una de esas negaciones al exterior de un cuantificador universal.

Para obtener más información sobre cómo funcionan estas reglas, asociadas con el comprobador de pruebas que utilicé, consulte forall x: Calgary Remix .

Referencias

Editor y comprobador de pruebas de deducción natural JavaScript/PHP estilo Fitch de Kevin Klement http://proofs.openlogicproject.org/

PD Magnus, Tim Button con adiciones de J. Robert Loftis remezcladas y revisadas por Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, invierno de 2018. http://forallx.openlogicproject.org/