Cómo demostrar la validez de $¬∃x P(x) ⊢ ∀x ¬P(x)$ en lógica de predicados

Question

Creo que tengo que asumir $¬x ¬P(x)$ y luego hacer una prueba por contradicción, pero no estoy seguro de si eso es correcto o cómo hacerlo.

Answer 1

Necesitamos contradicción en la prueba (pero no es un pufo por contradicción) :

1) $\lnot \exists x \ Px$ --- premisa

2) $\quad\quad| \quad Px$ --- asumido [a]

3) $\quad\quad| \quad \exists x \ Px$ --- de 2) por $\exists$ -intro

4) $\quad\quad| \quad\bot$ --- ¡contradicción! de 1) y 3)

5) $\lnot Px$ --- de 2)-4) por $\lnot$ -intro , descargando [a]

6) $\forall x \ \lnot Px$ --- de 5) por $\forall$ -intro .

Answer 2

He aquí una prueba de ello en Fitch. Exactamente la misma idea que la prueba de Mauro, pero no tiene variables libres en cualquier lugar que, al parecer, su sistema de prueba no quiere tampoco:

Answer 3

Tenemos para cualquier proposición $Q$ que no contenga $x$ gratis, $(\exists x.P(x))\to Q\vdash \forall x.(P(x)\to Q)$ . Esto es constructivamente cierto. Supongamos que $P(c)$ para un valor arbitrario de $c$ , luego usar modus ponens en la suposición después de introducir un existencial, luego generalizar como $c$ es arbitraria. Como término lambda, es básicamente currying. Si elige $Q\equiv\bot$ , obtienes tu afirmación utilizando el hecho de que (incluso constructivamente) $\neg P\equiv P\to \bot$ .