Equivalencia entre Peirce ' Ley s y medio excluido en lógica intuicionista

Question

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)$

Answer 1

La implicación $$[((P\rightarrow Q)\rightarrow P)\rightarrow P ] \rightarrow P\lor\neg P \quad\quad\quad\quad (1)$$ en realidad no es un teorema de intuitionistic lógica proposicional. Usted puede comprobar esto semánticamente, con un marco de Kripke con dos mundos $w_1\le w_2$, $P, Q$ satisfecho tanto en $w_2$ y ninguno de ellos satisfecho en $w_1$. Ver aquí para el fondo. O usted podría intentar demostrar (1) en un secuente cálculo y descubrir que te quedas atascado.

Lo que es cierto es que si usted hace Peirce la ley de un axioma adicional, a continuación, $P\lor\neg P$ se convierte en un teorema. En símbolos: $$\{((A\rightarrow B)\rightarrow a )\rightarrow\} \vdash P\lor\neg P$$ Aquí las llaves se supone que se refieren a la colección de todas las instancias de sustitución. Esto es discutido en la respuesta que enlaza. (Para Peirce la ley y de la LEM son equivalentes en el sentido de que la adición de cualquiera de ellos te dará la lógica clásica.)

Por el teorema de la deducción, a continuación, obtener una implicación similar a (1) como un teorema, pero si usted compruebe qué (sustitución) ejemplo de Peirce fue utilizado realmente, usted encontrará que $A=P\lor\neg P$, $B=\bot$. Así $$\vdash [((P\lor\neg P\rightarrow \bot)\rightarrow P\lor\neg P )\rightarrow P\lor\neg P] \rightarrow P\lor\neg P ,$$ que por supuesto no es el mismo (1).

En cuanto a tu última pregunta, tomado en un sentido abstracto, es definitivamente posible tener "$\vdash A$ implica $\vdash B$" satisfecho, sino $A\rightarrow B$ no es formal teorema: la hipótesis sostiene siempre que $\not\vdash A$, y no hay ninguna razón por la que esto haría a $A\rightarrow B$ un teorema.