Demostrar p a partir de ¬¬p

Question

Estoy atascado en la pregunta 2 de estas notas de clase en la lógica proposicional:

"2. Prueba proposicional. Dé una prueba formal de la frase p a partir de la premisa única ¬¬p utilizando únicamente el Modus Ponens y los esquemas axiomáticos estándar. Advertencia: Esto es sorprendentemente difícil. Aunque no lleva más de diez pasos, la prueba no es obvia. Este problema ilustra las dificultades de trabajar con métodos de demostración concebidos más para la minimización que para la facilidad de uso."

Como dice la pregunta, es sorprendentemente difícil, al menos para un novato como yo.

¿Alguien podría darme una pista sobre cómo empezar? He intentado varias aproximaciones pero nada.

Por ejemplo:

premise: ¬¬p
1) ¬¬p -> p            to prove    
2) ¬¬p -> (p -> ¬¬p)   II, 1    
3) p -> ¬¬p            premis, 2

Claramente no es el comienzo correcto, y (1) parece obviamente incorrecto :(

Gracias de antemano.

Answer 1

Sólo daré algunas pistas, como me pediste. En primer lugar, observa que sólo el esquema de realización de la contradicción utiliza la negación, por lo que tenemos que utilizarla de alguna manera en nuestra prueba. Si usáramos sólo los otros dos, no tendríamos información sobre cómo se comporta la negación.

Ahora, echemos un vistazo: $$(\lnot\phi \Rightarrow \psi) \Rightarrow ((\lnot\phi \Rightarrow \lnot\psi) \Rightarrow \phi) $$ nos gustaría introducir de alguna manera la doble negación. Adivinemos y sustituyamos $\lnot\phi$ para $\psi$ para conseguir $$(\lnot\phi \Rightarrow \lnot\phi) \Rightarrow ((\lnot\phi \Rightarrow \lnot\lnot\phi) \Rightarrow \phi) $$ Esto parece prometedor. Somos capaces de probar $\lnot\phi \Rightarrow \lnot\phi$ (que también es algo no trivial), tras lo cual podemos aplicar MP para deducir $$(\lnot\phi \Rightarrow \lnot\lnot\phi) \Rightarrow \phi$$ Ahora bien, si tenemos la suposición $\lnot\lnot\phi$ podemos demostrar $(\lnot\phi \Rightarrow \lnot\lnot\phi)$ utilizando el esquema de introducción de la implicación. Al juntarlo, demostramos que $\phi$ de $\lnot\lnot\phi$ .

---

Actualización: Cómo probar $\phi\Rightarrow\phi$ : \begin {align} [1] & ( \phi\Rightarrow ( \underbrace {( \phi\Rightarrow\phi )} \Rightarrow\phi )) ⇒ (( \phi\Rightarrow\underbrace {( \phi\Rightarrow\phi )}) \Rightarrow ( \phi\Rightarrow\phi )) & \mbox {sustituir $\phi$ , $\phi\Rightarrow\phi$ y $\phi$ en ID} \\ [2] & \phi\Rightarrow ( \underbrace {( \phi\Rightarrow\phi )} \Rightarrow\phi ) & \mbox {sustituir $\phi$ , $\phi\Rightarrow\phi$ en II} \\ [3] & ( \phi\Rightarrow\underbrace {( \phi\Rightarrow\phi )}) \Rightarrow ( \phi\Rightarrow\phi ) & \mbox {Modus Ponens [1] y [2]} \\ [4] & \phi\Rightarrow ( \phi\Rightarrow\phi ) & \mbox {sustituir $\phi$ , $\phi$ en II} \\ [5] & \phi\Rightarrow\phi & \mbox {Modus Ponens [3] y [4]} \\ \end {align}

Answer 2

Mi prueba, versión 2:

$$ premise: \lnot\lnot p $$ \begin {array}{ll} 1) & \lnot\lnot p & : p_1 \\ 2) & ( \lnot \phi \Rightarrow \psi ) \Rightarrow (( \lnot\phi \Rightarrow \lnot\psi ) \Rightarrow \phi ) & : CR \\ 3) & ( \lnot p \Rightarrow \lnot p) \Rightarrow (( \lnot p \Rightarrow \lnot\lnot p) \Rightarrow p) & : 2, \phi =p, \psi = \lnot p \\ 4) & ( \lnot p \Rightarrow \lnot p) = ( \lnot p \lor p) = \top & : válido \\ 5) & ( \lnot p \Rightarrow \lnot\lnot p) \Rightarrow p) & : 3,4 \\ 6) & ( \phi \Rightarrow ( \psi \Rightarrow \phi ) & : II \\ 7) & ( \lnot\lnot p \Rightarrow ( \lnot p \Rightarrow \lnot\lnot p) & : 6, \phi = \lnot\lnot p, \psi = \lnot p \\ 8) & ( \lnot p \Rightarrow \lnot\lnot p) & : p_1,7 \\ 9) & p & : 8,5 \\ \therefore \lnot\lnot p \Rightarrow p \end {array}

¿Es esto correcto, en términos de pasos y explicaciones a la derecha?

Gracias.

Mi prueba, versión 1 (Incorrecta)

p1 (premise): ¬¬p
1) ¬¬pp                                      : p1
2) (¬p => ¬¬p) => ((¬p => ¬(¬¬p)) => p)      : 1, CR
3) (¬p => ¬¬p) => ((¬p => ¬p) => p)          : 2, double negation
4) (¬p => ¬¬p) => p                          : 3, (¬p => ¬p) is valid
5) ¬¬p => (¬p => ¬¬p)                        : II, 4
6) (¬p => ¬¬p)                               : p1, MP, 5
7) p                                         : 6, MP, 6
∴ ¬¬p => p