¿Cómo podemos demostrar $(P \to \neg P) \to \neg P$ en este sistema?

Question

Se ha días que estoy atascado en una prueba simple de $(P \to \neg P) \to \neg P$ el uso de un sistema axiomático, y, cada vez que creo que estoy más cerca de él, me acabo de enterar de que estoy caminando en círculos.

El sistema va como sigue:

• Ax1: $(\varphi_1 \to (\varphi_2 \to \varphi_3)) \to ((\varphi_1 \to \varphi_2)\to(\varphi_1 \to \varphi_3))$
• Ax2: $\varphi_1 \to (\varphi_2 \to \varphi_1)$
• Ax3: $\varphi_1 \to ((\neg \varphi_1) \to \varphi_2)$
• Ax4: $((\neg \varphi_1) \to \varphi_1) \to \varphi_1$
• Ax5: $(\neg \varphi_1) \to (\varphi_1 \to \varphi_2)$

• Ax6: $\varphi_1 \to ((\neg \varphi_2) \to (\neg (\varphi_1 \to \varphi_2)))$

• Reglas: Modus Ponens (teorema de la Deducción también es aceptable).

• Idioma: $\neg$ $\to$ como primitivas.

Es comprobable a todos?

Cualquier ayuda será muy apreciada.

Answer 1

Queremos probar lo siguiente: $$\vdash (P \to \neg P) \to \neg P$$

Observe cómo la misma este es su Axioma 4 - sólo necesitamos para reemplazar todas las instancias de $P$ $\neg P$ y, a continuación,$\neg \neg P$$P$. Esto nos da una pista acerca de por dónde empezar. Si su idioma no define a $\neg P$ $P \to \bot$ (o si no tiene un símbolo de $\bot$), entonces usted puede saltar el Lema 1.

Lema 1: $P \to \neg \neg P$.
Prueba: el Axioma 3, los estados que $P \to ((\neg P) \to \bot)$, que es mano de $P \to \neg \neg P$.

Lema 2: $\neg \neg P \to P$.
Prueba: por el teorema de la deducción, podemos suponer que $\neg \neg P$ e intentar demostrar $P$. Axioma 5 $\neg \neg P \to (\neg P \to Q)$; modus ponens da $\neg P \to Q$. Axioma 4 da $(\neg P \to P) \to P$, por lo tanto, dejar $Q = P$ y el modus ponens da $P$, según se requiera.

Es decir, hemos demostrado que $\neg \neg P$ es equivalente a $P$.

Por lo tanto, una prueba de $(P \to \neg P) \vdash \neg P$ (que es equivalente al teorema de la deducción), es la siguiente:

1. $(\neg \neg P \to \neg P) \to \neg P$ (Axioma 4)
2. $P \to \neg P$ (hipótesis)
3. $\neg \neg P \to P$ (lema 2)
4. $(P \to \neg P) \to (\neg \neg P \to (P \to \neg P)) $ (Axioma 2)
5. $\neg \neg P \to (P \to \neg P)$ (modus ponens, las líneas 4 y 2)
6. $(\neg \neg P \to (P \to \neg P)) \to ((\neg \neg P \to P) \to (\neg \neg P \to \neg P))$ (Axioma 1)
7. $(\neg \neg P \to P) \to (\neg \neg P \to \neg P)$ (modus ponens, líneas 5 y 6)
8. $\neg \neg P \to \neg P$ (modus ponens, las líneas 3 y 7)
9. $\neg P$ (modus ponens, líneas 1 y 8)

Answer 2

Prover9 producido un sistema totalmente automatizado de prueba utilizando hyperresolution rápidamente. El uso de hyperresolution viene como similar a la utilización de condensados desprendimiento (que puede obtener dijo a encontrar el más general resultado de la sustitución de las instancias de dos bien formado fórmulas mediante modus ponens por la búsqueda de la menor cantidad de sustitución en el antecedente de la no sustitución de la instancia de las dos wffs, y la mayor cantidad de la sustitución en el consecuente de la misma sustitución de la instancia de la más wff). Aprender a seguir a esta prueba yo te sugiero que veas aquí.

% \begin{align} \lim_{x \to 0} \dfrac{f(x) - f(0)}{x-0} & = \lim_{x \to 0} \dfrac{f(x) - 0}{x} & \textrm{ as } f(0) = 0 \\ & = \lim_{x \to 0} \dfrac{x^2 \sin\left(\frac{1}{x}\right)}{x} & \\ & = \lim_{x \to 0} x \sin\left(\frac{1}{x}\right) & \end--- Comentarios de la prueba original --------

La prueba % 1 en 3.78 (+ 0.47) segundos.

% De la longitud de la prueba es de 32.

% El nivel de la prueba es de 13.

% Máximo de la cláusula de peso es de 14.

% Cláusulas de 1206.

1 P(C(C(x,N(x)),N(x))) # etiqueta(non_clause) # etiqueta(meta). [meta].

2 -P(C(x,y)) | -P(x) | P(y). [asunción].

3 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))). [asunción].

4 P(C(x,C(y,x))). [asunción].

5 P(C(x,C(N(x),y))). [asunción].

6 P(C(C(N(x),x),x)). [asunción].

7 -P(C(C(c1,N(c1)),N(c1))). [deny(1)].

9 P(C(x,C(y,C(z,y)))). [hyper(2,a,4,a,b,4,a)].

10 P(C(C(x,y),C(x,x))). [hyper(2,a,3,a,b,4,a)].

13 P(C(x,C(y,C(N(y),z)))). [hyper(2,a,4,a,b,5,a)].

18 P(C(x,C(C(N(y),y),y))). [hyper(2,a,4,a,b,6,a)].

26 P(C(x,x)). [hyper(2,a,10,a,b,9,a)].

29 P(C(C(C(x,y),x),C(C(x,y),y))). [hyper(2,a,3,a,b,26,a)].

38 P(C(C(x,y),C(x,C(N(y),z)))). [hyper(2,a,3,a,b,13,a)].

46 P(C(C(x,C(N(y),y)),C(x,y))). [hyper(2,a,3,a,b,18,a)].

167 P(C(x,C(N(C(y,x)),z))). [hyper(2,a,38,a,b,4,a)].

177 P(C(C(x,N(C(y,x))),C(x,z))). [hyper(2,a,3,a,b,167,a)].

510 P(C(C(N(x),N(C(y,N(x)))),x)). [hyper(2,a,46,a,b,177,a)].

575 P(C(x,C(C(N(y),N(C(z,N(y)))),y))). [hyper(2,a,4,a,b,510,a)].

588 P(C(x,C(C(C(y,z),y),C(C(y,z),z)))). [hyper(2,a,4,a,b,29,a)].

608 P(C(C(C(x,C(y,x)),z),z)). [hyper(2,a,29,a,b,9,a)].

652 P(C(x,C(C(C(y,C(z,y)),u),u))). [hyper(2,a,4,a,b,608,a)].

1597 P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))). [hyper(2,a,3,a,b,652,a)].

16656 P(C(C(x,C(C(y,x),z)),C(x,z))). [hyper(2,a,1597,a,b,3,a)].

16759 P(C(x,C(C(x,y),y))). [hyper(2,a,16656,a,b,588,a)].

16760 P(C(N(C(x,N(y))),y)). [hyper(2,a,16656,a,b,575,a)].

16865 P(C(x,C(y,C(C(y,z),z)))). [hyper(2,a,4,a,b,16759,a)].

17384 P(C(C(C(N(C(x,N(y))),y),z),z)). [hyper(2,a,16759,a,b,16760,a)].

20169 P(C(C(x,y),C(x,C(C(y,z),z)))). [hyper(2,a,3,a,b,16865,a)].

25974 P(C(N(C(x,N(y))),C(C(y,z),z))). [hyper(2,a,17384,a,b,20169,a)].

27812 P(C(C(x,N(x)),N(x))). [hyper(2,a,6,a,b,25974,a)].

Answer 3

Creo que me mostró que se puede comprobable en el sistema formal. Me explico.

Nos basamos en las pruebas en el sitio "Metamath Prueba Explorer". El sitio posee la prueba de $\left(\phi \to \neg\phi\right) \to \neg\phi$ (Teorema de pm2.01 (158)). Suponemos que las pruebas de esta fórmula y relevantes de los lemas son del todo correcta, porque ellos son equipo-comprobado :)

Sin embargo, existe una gran brecha restante. La prueba enlazado más arriba es que no se basa en el sistema formal. De hecho, el sistema formal utilizado en el anterior sitio dispone de los siguientes tres axiomas:

1. su Ax1 (Axioma ax-2 (6)):

   $\left(\phi \to \left(\psi \to \chi\right)\right)\to\left(\left(\phi\to\psi\right)\to\left(\phi\to\chi\right)\right)$

2. su Ax2 (Axioma ax-1 (5)):

   $\phi\to\left(\psi\to\phi\right)$

3. el axioma de la contraposición (Axioma de ax-3 (7)):

   $\left(\neg\phi\to\neg\psi\right)\to\left(\psi\to\phi\right)$

Además, tiene exactamente la misma regla de inferencia como la suya, es decir, la regla de Modus Ponens (Axioma ax-mp (8)).

Así, El único axioma que carece en su sistema formal es ax-3 en la lista anterior. El problema se ha reducido a probar ax-3 en su sistema. Vamos a meta-demostrar que el sistema tiene la prueba.

Bajo los supuestos de $\neg\phi\to\neg\psi$, $\psi$ y $\neg\phi$, usted tiene $\psi$$\neg\psi$, y por lo tanto $\phi$ por Ax3 y la regla de inferencia. Por el Teorema de la Deducción, tiene $\neg\phi\to\phi$ asumiendo $\neg\phi\to\neg\psi$$\psi$; por lo tanto, por Ax4 hay una prueba de $\phi$ con la misma suposición. De nuevo por el teorema de la Deducción, no es una prueba formal de ax-3 en el sistema formal, sin ningún tipo de suposición.

Yo no directamente dar la prueba de $\left(\phi \to \neg\phi\right) \to \neg\phi$; sin embargo de lo anterior se demostró que hay algunas pruebas de $\left(\phi \to \neg\phi\right) \to \neg\phi$, en su sistema. Que es, en primer lugar, recuperar la prueba de $\left(\phi \to \neg\phi\right) \to \neg\phi$ en el Metamath, en los que la usan son los axiomas ax-1, 2, y 3. No es una prueba en su sistema, pero se puede sustituir cada ocurrencia de ax-3 por la prueba de ax-3 en su sistema, obtenida anteriormente. A continuación, la secuencia resultante de bien formado fórmulas es una prueba en su sistema, para lo que cuenta ya no tiene una ocurrencia de ax-3 como un axioma; en lugar de ax-3 sólo es un resultado intermedio demostrado mediante ax1, 2, 3 y 4. Por supuesto, ax-1 y 2 no son un problema en absoluto, ya que son su ax2 y 1.