Prueba de equivalencia en lógica de primer orden

Question

Tengo una pregunta sobre cómo probar $$(\neg \forall x \, P(x)) \rightarrow (\exists x \, \neg P(x)) $$ con una prueba de deducción natural, donde $P$ es un predicado.

Especialmente tengo problemas con qué hacer con la negación delante de $\forall$ .
En general, ¿cómo debo abordar el problema si tengo una negación delante de la fórmula, especialmente si se trata de una suposición? Pregunto esto en el contexto de una prueba de deducción natural, como la de arriba (o eg. $\neg \exists ..., etc.$ )

Answer 1

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $ No especifica qué conjunto de reglas está utilizando, pero voy a suponer que las que se encuentran en forallx: Calgary libro.

Queremos demostrar una sentencia sin locales. Lo primero sería preguntarse cuál es el principal conectivo lógico . En este caso, una implicación. Entonces, Implicación Introducción tiene el siguiente esquema:

$ \fitch{}{ \fitch{i.\mathcal A}{ j. \mathcal B }\\ \mathcal{A \to B} \qquad\mathbf{\to I}\,i-j } $

En nuestro caso,

$ \fitch{}{ \fitch{\lnot \forall xP(x)}{ \vdots\\ \exists x \lnot P(x) }\\ \lnot \forall x P(x) \to \exists x \lnot P(x) \ii{} } $

Podríamos intentar asumir $P(a)$ e intentar utilizar Introducción universal regla...

$ \fitch{}{ \fitch{1.\,\lnot \forall xP(x)}{ \fitch{2.\lnot P(a)}{ 3. \forall xP(x)\\ \bot\\ }\\ \exists x \lnot P(x) }\\ \lnot \forall x P(x) \to \exists x \lnot P(x) } $

pero inmediatamente vemos que su aplicación está prohibida porque el nombre a ya se produce en un supuesto no liquidado (línea 2).

Un enfoque indirecto parece razonable. Si pretendemos utilizar IP (Prueba indirecta) para derivar $\exists x\lnot P(x)$ asumiendo $\lnot \exists x\lnot P(x)$ y alcanzando $\bot$ permitiría la aplicación de dicha norma.

A toda prueba:

$ \fitch{}{ \fitch{1.\,\lnot \forall xP(x)}{ \fitch{2.\,\lnot \exists x \lnot P(x)}{ \fitch{3.\,\lnot P(a)}{ 4.\,\exists x \lnot P(a) \Ei{3} 5.\,\bot \ne{2,4} }\\ 6.\,P(a) \IP{3-5} 7.\,\forall xP(x) \Ai{6} 8.\,\bot \ne{1,7} }\\ 9.\,\exists x \lnot P(x) \IP{2-8} }\\ 10.\,\lnot \forall x P(x) \to \exists x \lnot P(x) \ii{1-9} } $

Answer 2

He aquí algunas proposiciones y su negación $$\exists x P(x) \;\;,\;\; \forall x \lnot P(x)$$

$$\forall x \exists y :P(x,y)\;\;;\;\; \exists x\forall y \lnot P(x,y)$$

$$P \vee Q \;\;,\;\; \lnot P \wedge \lnot Q$$

$$P \wedge Q \;\;,\;\; \lnot P \vee \lnot Q$$

$$P\implies Q \;\;,\;\; P \wedge \lnot Q$$

$$a>b \;\;,\;\; a\le b$$