**Competencia finalizada:** ¿Cuál es la prueba más corta de $\exists x \forall y (D(x) \to D(y))$?

Question

La competencia ha finalizado el 6 de junio de 2014 a las 22:00 GMT. El ganador es Bryan.

¡Bien hecho!

---

Cuando estaba releyendo la prueba de la paradoja de los bebedores (ver Prueba de la paradoja de los bebedores), me di cuenta de que $\exists x \forall y (D(x) \to D(y))$ también es un teorema.

Logré demostrarlo en 21 líneas (ver abajo), pero no estoy seguro si esta es la prueba más corta posible. Y me gustaría saber si hay versiones más cortas.

Esa es la razón de esta competencia (ver también abajo)

Reglas de la competencia

• Esta es una competencia pequeña, daré a la persona que presente la prueba más corta (más corta que la prueba de abajo) una recompensa de 200 puntos de reputación (no marcados). (Solo puedo agregar una recompensa en un par de días a partir de ahora, pero ya puedes empezar a pensar en cómo demostrarlo y ya puedes publicar tu respuesta.

• La longitud de una prueba se mide por la cantidad de líneas numeradas en la prueba (ver la prueba de abajo como ejemplo, la primera fórmula está en la línea número 2 y las líneas de fin de prueba no se cuentan)

• Si hay más de una persona con la respuesta más corta, la recompensa se otorga al primer que la publique (medido con la última edición sustancial de la prueba)

• La respuesta debe estar en forma de una deducción natural en estilo Fitch completa escrita en un cuadro de respuesta como abajo. Las pruebas formateadas en $\LaTeX$ son aún mejores, pero simplemente no sé cómo hacerlo.

• El sistema de prueba es el sistema de deducción natural en estilo Fitch descrito en "Language proof and Logic" de Barwise cs, (LPL, http://ggweb.stanford.edu/lpl/ ), excepto que la regla General Conditional Proof no está permitida. (Simplemente no me gusta la regla, y no estoy seguro si usar esta regla acortaría la prueba tampoco)

• Tal vez dé un premio adicional por la respuesta más hermosa, o la prueba más corta en otro estilo/método de deducción natural. Depende un poco de las respuestas que reciba, otros también pueden establecer y dar recompensas como les parezca.

• Puedes proporcionar más de una respuesta, respuestas en más de un método de prueba, etc., pero publícalas como respuestas separadas y ten en cuenta que solo la prueba que utiliza el método Fitch descrito arriba está compitiendo, y otros participantes pueden echar un vistazo a tus respuestas.

• • BUENA SUERTE, y que gane el mejor.

Sistema de prueba:

Para los participantes que no tienen el libro LPL, las únicas reglas de inferencia permitidas son las reglas que usé en la prueba:

• las reglas de introducción y eliminación de $\bot$ (falso, contradicción)
• la regla de eliminación de $\lnot \lnot$
• las reglas de introducción de $\lnot$, $\to$, $\exists$ y $\forall

(ver también la prueba de abajo para ejemplos de cómo usarlas.)

También son permitidas las siguientes reglas:

• las reglas de introducción y eliminación de $\land$, $\lor$ y $\leftrightarrow
• las reglas de eliminación de $\to$, $\exists$ y $\forall
• la regla de reiteración

(Esto es solo por completitud, no creo que sean útiles en esta prueba)

Aviso:

• la línea 1 está vacía (en el software Fitch que acompaña al libro, la línea 1 es solo para premisas y no hay premisas en esta prueba)

• las líneas de fin de subprueba no tienen número de línea. (y no cuentan en la cantidad total de líneas)

• la regla General Conditional Proof no está permitida

• no hay regla de eliminación de $\lnot$ (solo una regla de eliminación de doble negación)

Mi prueba: (y ejemplo de cómo usar las reglas, y cómo debería estar formateada tu respuesta)

1  |
.  |----------------- 
2  | |____________  ~Ex Vy (D(x) -> D(y))    Nueva Subprueba para ~ Introducción
3  | | |_________a                           variable para Introducción Universal
4  | | | |________  D(b)                     Nueva Subprueba para -> Introducción
5  | | | | |______  ~D(a)                    Nueva Subprueba para ~ Introducción 
6  | | | | | |___c                           variable para Introducción Universal
7  | | | | | | |__  D(a)                     Nueva Subprueba para -> Introducción
8  | | | | | | |    _|_                      5,7 introducción _|_
9  | | | | | | |    D(c)                     8 Eliminación _|_
.. | | | | | | <-------------------------   fin de subprueba
10 | | | | | |      D(a) -> D(c)             7-9 Introducción ->
.. | | | | | <---------------------------   fin de subprueba
11 | | | | |        Vy(D(a) -> D(y))         6-10 Introducción Universal
12 | | | | |        Ex Vy (D(x) -> D(y))     11 Introducción Existencial
13 | | | | |        _|_                      2,12 Introducción _|_
.. | | | | <-----------------------------   fin de subprueba
14 | | | |          ~~D(a)                   5-13 Introducción ~
15 | | | |          D(a)                     14 Eliminación ~~
.. | | | <-------------------------------   fin de subprueba   
16 | | |            D(b) -> D(a)             4-15 Introducción ->
.. | | <---------------------------------   fin de subprueba   
17 | |              Vy(D(b) -> D(y))         3-16 Introducción Universal
18 | |              ExVy(D(x) -> D(y))       17 Introducción Existencial
19 | |              _|_                      2,18 Introducción _|_
.. | <-----------------------------------   fin de subprueba
20 |                ~~Ex Vy (D(x) -> D(y))   2-19 Introducción ~
21 |                Ex Vy (D(x) -> D(y))     20 Eliminación ~~

Preguntas permitidas y otras cosas meta

Pregunté en http://meta.math.stackexchange.com/questions/13855/are-small-competitions-allowed si esta era una pregunta permitida, todavía no he recibido una respuesta (28 de mayo de 2014) de que tales preguntas no eran permitidas, estaban fuera del alcance de este foro o cualquier otro comentario negativo, no me han comentado que esta es una pregunta inapropiada o bajo qué circunstancias se permiten tales competencias.

(el comentario más negativo fue que deberían ser puntos de reputación no marcados. :) ¡y ese comentario fue eliminado más tarde...

Si no estás de acuerdo con esto, por favor agrégalo como respuesta a la pregunta en el sitio de meta de math stackexchange. (o vota una respuesta así)

Por otro lado, si te gustan las competencias, muestra también tu apoyo en el sitio de meta, (añadiéndolo como respuesta o votando una respuesta así)

PD: no pienses que toda la lógica es simple, no haré una prueba más corta en poco tiempo, la pregunta es bastante difícil y complicada, ¡pero prueba que estoy equivocado! :)

Answer 1

Bueno, aquí está mi solución aunque he usado 4 reglas 'no permitidas'.

1. $\neg\exists x\forall y(Dx\implies Dy)\quad$ suposición para introducción de $\neg$
2. $\forall x\neg\forall y(Dx\implies Dy)\quad$ DeMorgan para cuantificadores
3. $\forall x\exists y \neg(Dx\implies Dy)\quad$ DeMorgan para cuantificadores
4. $\forall x\exists y\neg(\neg Dx\vee Dy)\quad$ Intercambio condicional
5. $\forall x\exists y(\neg\neg Dx\wedge \neg Dy)\quad$ DeMorgan
6. $\forall x \exists y(Dx\wedge\neg Dy)\quad$ Doble negación
7. $\exists y(Da\wedge\neg Dy)\quad$ Instantación universal
8. $Da\wedge \neg Db\quad$ Instantación existencial (marca $b$)
9. $\neg Db\quad$ Simplificación
10. $\exists y(Db\wedge \neg Dy)\quad$ Instantación universal
11. $Db\wedge \neg Dc\quad$ Instantación existencial (marca $c$)
12. $Db\quad$ Simplificación
13. $\bot\quad$ Contradicción 9, 12
14. $\neg\neg\exists x\forall y(Dx\implies Dy)\quad$ Prueba por contradicción 1-13
15. $\exists x\forall y(Dx\implies Dy)\quad$ Doble negación

Supongo que hay 16 líneas en total si incluimos la línea de premisa vacía. Sin embargo, tengo un par de comentarios.

En primer lugar, dudo mucho que esta prueba se pueda obtener con la última regla aplicada siendo Generalización Existencial. Esta afirmación es una verdad lógica precisamente porque podemos cambiar nuestro $x$ dependiendo de si el dominio tiene o no un miembro tal que $Dx$ sea verdadero. Si $D$ es verdadero para todos los miembros del dominio, cualquier elección de $x$ hará que la afirmación sea verdadera. Si $D$ no es verdadero para algún miembro del dominio, elegir eso como nuestro $x$ hará que la afirmación sea verdadera. Decir que podemos llegar a la conclusión con un uso final de G.E. significa que el miembro $b$ que aparece en el antecedente de alguna manera manejó ambos casos mientras que lo único que se supone que sabemos sobre $b$ es que es un miembro del dominio. Todavía no sabemos nada del dominio.

Dicho esto, después de obtener una copia de tu libro y leer las reglas, parece que la única manera de llegar a la conclusión es mediante la aplicación de la doble negación. Y la única forma de llegar allí es mediante una prueba por contradicción. Por lo tanto, creo que tus líneas 1, 2, 19, 20 y 21 pertenecen a la solución mínima. Hasta ahora, no he encontrado nada más sencillo para el medio.

Answer 2

Aunque esté fuera del alcance de lo que se pide, quizás sea divertido notar que una demostración en un sistema de tableau es notablemente más corta y se escribe sola (sin siquiera tener que dividir el árbol y considerar casos):

$$\neg\exists x\forall y(Dx\implies Dy)$$ $$\forall x\neg\forall y(Dx\implies Dy)$$ $$\neg\forall y(Da\implies Dy)$$ $$\exists y\neg(Da\implies Dy)$$ $$\neg(Da\implies Db)$$ $$\neg Db$$ $$\neg\forall y(Db\implies Dy)$$ $$\exists y\neg(Db\implies Dy)$$ $$\neg(Db\implies Dc)$$ $$Db$$ $$\bigstar$$

Answer 3

Esto no es exactamente una respuesta, ya que se trata de la paradoja del bebedor, y no de la versión ligeramente diferente aquí, pero puede ayudar a desarrollar una prueba más breve de la variante aquí. Sin embargo, el recuento de líneas puede no ser aceptable, porque utiliza Taut Con, pero solo para obtener $A$ y $\lnot B$ a partir de $\lnot (A \to B)$, no para ningún intercambio de cuantificadores ni nada por el estilo. La respuesta aceptada utiliza DeMorgan's con cuantificadores, así que creo que esto podría estar dentro de los límites.

Usando el software Fitch que se distribuye con el libro LPL, puedes reducir la Paradoja del Bebedor a 14 líneas, debido a la forma en que se permite que la introducción de $\forall$ cite cualquier resultado intermedio en la prueba, no solo el último.

Nota: La imagen dice "pájaro" porque cuando escuché esto por primera vez, se formuló como "hay algo tal que si es un pájaro, entonces todo es un pájaro." Hice esta prueba en 2009 y ya no tengo acceso a los archivos originales, así que lamento la calidad de la imagen.

Tal vez esto pueda ayudar a acortar una prueba de la variante.

Answer 4

Usando mi confiable Lema de Hokus Ponens:

Answer 5

Me gusta esta (FO Con está aplicando algunas equivalencias básicas, no muy diferente al comienzo de la prueba de Bryan):