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

Bien, suficiente diversión. Realmente no creo que la prueba de Willemien pueda ser acortada si nos atenemos a las reglas. Aquí está la prueba de Willemien en Fitch:

Answer 2

El Generador de Pruebas de Árbol proporciona una prueba corta:

https://www.umsu.de/trees/#~7x~6y(Dx~5Dy)

Answer 3

Usando equvalencias:

$\top \equiv \forall y D(y) \rightarrow \forall y D(y) \equiv \forall x D(x) \rightarrow \forall y D(y) \equiv \exists x (D(x) \rightarrow \forall y D(y)) \equiv \exists x \forall y (D(x) \rightarrow D(y)) $

Answer 4

Aquí hay otra prueba. Primero proporcionaré el argumento informal y luego la derivación al estilo Fitch.

Prueba: Usando el principio del tercero excluido obtenemos dos casos:

• Si $\forall y \, D(y)$ entonces no importa $x, y$, trivialmente tenemos $D(x) \rightarrow D(y)$, así que en particular $\exists x \forall y \, D(x) \rightarrow D(y)$.
• Si $\neg \forall y \, D(y)$ entonces por DeMorgan para cuantificadores obtenemos $\exists y \, \neg D(y)$. Entonces hay un $a$ con $\neg D(a)$ lo que implica $\forall x \, D(a) \rightarrow D(x)$ de nuevo dándonos $\exists x \forall y \, D(x) \rightarrow D(y)$. $~~\Box$