Demostración formal de la sentencia en el cálculo de primer orden, ejemplo.

Question

Es una observación bien conocida que en todo bar no vacío siempre hay un cliente que puede gritar con razón "Cuando yo bebo, todos beben". En la lógica de primer orden esto se expresa con la sentencia $$\exists x(x = x) \supset \exists x(D(x) \supset \forall y D(y)).$$ ¿Cómo sería una demostración formal de esta frase en el cálculo de primer orden?

El libro de texto que estoy utilizando no tiene muchos ejemplos, y sería esclarecedor tener un ejemplo detallado y trabajado para tenerlo en mente cuando se piense en cosas relacionadas.

Se agradecería cualquier ayuda.

Answer 1

Lo demostraré con Deducción natural .

Asumiendo la semántica "estándar", con dominio no vacío para la interpretación, el antecedente $\exists x (x=x)$ es válido; por lo tanto, demostraré sólo la validez del consecuente :

$\exists x (Dx \to \forall y Dy)$ .

Prueba :

1) $\lnot\exists x (Dx \to \forall y Dy)$ --- asumido [a]

2) $\lnot Dx$ --- asumido [b]

3) $Dx$ --- asumido [c]

4) $\bot$ --- de 2) y 3) por $(\lnot \text E)$

5) $\forall y Dy$ --- de 4) por $(\bot \text E)$

6) $Dx \to \forall y Dy$ --- de 3) y 5) por $(\to \text I)$ , descargando [c]

7) $\exists x (Dx \to \forall y Dy)$ --- de 6) por $(\exists \text I)$

8) $\bot$ --- de 1) y 7) por $(\lnot \text E)$

9) $Dx$ --- de 2) y 8) por $(\text {DN})$ ( Doble negación ), descargando [b]

10) $\forall y Dy$ --- de 9) por $(\forall \text I)$

11) $Dx \to \forall y Dy$ --- de 10) por $(\to \text I)$

12) $\exists x (Dx \to \forall y Dy)$ --- de 11) por $(\exists \text I)$

13) $\bot$ --- de 1) y 12) por $(\lnot \text E)$

$\exists x (Dx \to \forall y Dy)$ --- de 1) y 13) por $(\text {DN})$ , descargando [a].