Estoy buscando un intuitionistically prueba válida de la fórmula :
$[((P→Q)→P)→P] ↔ (P \lor \lnot P)$
el uso de la "norma" de Hilbert-estilo axioma del sistema de Kleene [1952], para intuitionistic cálculo proposicional (con modus ponens).
Siguiente Wiki's prueba, he reescrito la primera parte :
$\vdash (P \lor \lnot P) → [((P→Q)→P)→P]$
de la siguiente manera :
1) $P$ --- supone
2) $((P→Q)→P)→P$ --- del axioma $A → (B → A)$, $P$ en lugar de$A$$((P→Q)→P)$$B$, y 1), por modus ponens
3) $P → [((P→Q)→P)→P]$ --- a partir de 1) y 2) por el Teorema de la Deducción, "descarga" la hipótesis 1)
4) $\lnot P$ --- supone
5) $(P→Q)$ --- del axioma $\lnot A → (A → B)$ (ex falso quodlibet) y 4), por modus ponens
6) $(P→Q)→P$ --- supone
7) $P$ --- a partir de 5) y 6), por mp
8) $((P→Q)→P)→P$ --- a partir de 6) y 7), por el Teorema de la Deducción, "descarga" asunción 6)
9) $\lnot P → [((P→Q)→P)→P]$ --- de 4) y 8) por el Teorema de la Deducción, "descarga" asunción 4)
Ahora que hemos obtenido : $P → [((P→Q)→P)→P]$ (3) y $\lnot P → [((P→Q)→P)→P]$ (9), usamos el axioma $(A → C) → ((B → C) → (A ∨ B → C))$ $P$ en lugar de $A$, $\lnot P$ en lugar de $B$ $((P→Q)→P)→P$ $C$ a derivar, por modus ponens dos veces :
10) $(P \lor \lnot P) → [((P→Q)→P)→P]$.
Yo no soy capaz de manege de la Wiki de prueba de la otra parte con el fin de demostrar el condicional :
$\vdash [((P→Q)→P)→P] → (P \lor \lnot P)$.
En la Wiki de la prueba, así como en la respuesta a este post podemos encontrar la prueba de :
si $\vdash ((P→Q)→P)→P$,$\vdash P \lor \lnot P$.
El uso de la prueba de una "sustitución" de Peirce de la ley : $(((P \lor \lnot P) \rightarrow \bot) \rightarrow (P \lor \lnot P)) \rightarrow (P \lor \lnot P)$, y esto es posible sólo si la fórmula es un axioma o teorema, que no está en intuitionistic lógica.
Por una situación similar, véase Jan von Platón, Elementos de Razonamiento Lógico (2013), página 82 :
Dado $A \lor \lnot A$ si $\lnot \lnot A$ es asumido, $A$ sigue y, por tanto, la implicación $\lnot \lnot A \supset A$ sigue de $A \lor \lnot A$. Una sencilla prueba de búsqueda en intuitionistic sequent cálculo da una formales de derivación para :
$A \lor \lnot A \supset (\lnot \lnot A \supset A)$.
Similar a prueba de búsqueda de lo contrario falla, porque no hay derivación de :
$(\lnot \lnot A \supset A) \supset (A \lor \lnot A)$.
[...]
La situación general es que si $\vdash \lnot \lnot A \supset A$,$\vdash A \lor \lnot A$, pero no $\vdash (\lnot \lnot A \supset A) \supset (A \lor \lnot A)$.
Por lo tanto, la Pregunta es : ¿es posible que
si $\vdash ((P→Q)→P)→P$,$\vdash P \lor \lnot P$,
pero $\nvdash [((P→Q)→P)→P] → (P \lor \lnot P)$