Pregunta de prueba de lógica del lenguaje: ¬∃x∀y[E(x,y) ↔ ¬E(y,y)]

Aquí hay una prueba usando un verificador de prueba de deducción natural estilo Fitch.

Para hacer oraciones bien formadas tuve que reescribir algunos de los nombres usados ​​en el ejemplo del OP. En lugar de "E", usé "P", ya que "E" es un símbolo del cuantificador existencial en este comprobador de pruebas. Además, la notación en este comprobador de pruebas es más compacta. Por ejemplo, "E(x,y)" se convirtió en "Pxy".

En lugar de comenzar con una negación de la conclusión, eliminé el signo de negación de la conclusión con la intención de introducir la negación al final, lo cual hice en la línea 12.

De la línea 2 a la línea 10 usé una subdemostración para iniciar el intento de eliminar el cuantificador existencial (∃E en la línea 11) tomando el nombre "a" para la variable "x". Usé el mismo nombre para eliminar el cuantificador universal (∀E) en la línea 3. Esto me permitió usar la ley del medio excluido (LEM) para llegar a una contradicción en la línea 10 descargando las suposiciones hechas en las líneas 4 y 7 al cerrar las subpruebas.

La línea 10 me permitió eliminar el cuantificador existencial en la línea 11 descargando la suposición en la línea 2. La contradicción en la línea 10 me permitió introducir una negación en la línea 12 y completar la prueba.

---

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

Yo mismo no he usado/enseñado LPL, así que no conozco el formato o los estándares para terminar una prueba RAA. Las líneas sangradas 1-4 son correctas; para la línea 2 sin sangría, está mal formada (¿Eaa si y solo si E?) o no entiendo cómo analizarla.

En mis cursos de lógica, probablemente aceptaría 4 como suficiente para mostrar que 1 conduce a una contradicción, QED.

Para demostrar ~P, comience asumiendo P con el objetivo de demostrar una contradicción. Por lo tanto, use "introducción de negación". (Nota: no asuma una doble negación si puede evitarla, especialmente si su primer movimiento es eliminarla).

Para obtener una contradicción a partir de ƎxⱯy Qxy, use las reglas de instanciación del cuantificador y demuestre que Qba es una contradicción para el testigo by a arbitrario (que posiblemente también sea b).

Para obtener una contradicción de Eba <-> ~Eaa, para el testigo b y la a arbitraria, bueno, tenga en cuenta que cuando a es b, tiene una contradicción. Entonces tu eliminación universal es para el testigo existencial.

Para resumir: Debemos asumir ƎxⱯy (Exy <-> ~Eyy), luego asumir un testigo [b] para el existencial, que es Ɐy (Eby <-> ~Eyy), entonces podemos eliminar ese universal al testigo, entonces Ebb <-> ~Ebb, y demostrar que esto es contradicción, permitiéndonos así descargar los supuestos y terminar con la introducción de la negación.

Demostrar que Ebb <-> ~Ebb es una contradicción es simplemente una cuestión de usar eliminación de negación y eliminaciones bicondicionales. Asumiendo que Ebb deriva una contradicción del bicondicional, introduciendo así una negación. ~Ebb también deriva la contradición necesaria del bicondicional.

 |_
 |  |_ Ǝx Ɐy (Exy <-> ~Eyy)
 |  |  |_ [b] Ɐy (Eby <-> ~Eyy)
 |  |  |  Ebb <-> ~Ebb
 |  |  |  |_ Ebb
 |  |  |  |  ~Ebb
 |  |  |  |  ┴
 |  |  |  ~Ebb
 |  |  |  Ebb
 |  |  |  ┴
 |  |  ┴
 |  ~Ǝx Ɐy (Exy <-> ~Eyy)

La declaración ¬∃x∀y[E(x,y)⟷¬E(y,y)] es equivalente, usando las propiedades de la negación para

∀x∃y{[E(x,y)∧¬¬E(y,y)]∨[¬E(y,y)∧¬E(x,y)]} .

La oración entre corchetes siempre es verdadera para y=x usando ¬¬E→E, y esto prueba la declaración. Esta prueba tiene la ventaja de evitar el uso de reductio ad absurdum , y por lo tanto la ley del tercero excluido; sin embargo, utiliza el hecho de que ¬¬E→E. Por lo tanto, esta prueba no sería aceptable en la lógica intuicionista . La declaración de OP es un teorema en la lógica clásica pero no en la lógica intuicionista más débil.