En primer lugar, vamos a la refundición de los esquemas como bien formada fórmulas. Esto hace que las sustituciones de mecánica y menos propenso a errores. O más fácil de corregir cuando se producen errores.
Axioma 1 (P→→(P→→P))
Axioma 2 ((S→→(P→→P))→→((S→→P)→→(S→→Q)))
Axioma 3 ((¬¬Q→→¬¬P)→→(P→→P))
Queremos llegar a (¬¬P→→(P→→P)). Si nos fijamos en el Axioma 3, con la consiguiente coincide con el consiguiente de que el objetivo de la fórmula. Así que, ¿cómo nos deshacemos de (¬¬Q→→¬¬P) y poner ¬¬P en frente de (P→→P)? O podemos hacer una de estas dos?
Así, se da el caso de que (P→→P) fue un teorema, entonces el Axioma 1 nos permitiría poner cualquier fórmula, como ¬¬P, en frente de (P→→P). Axioma 1 también puede acostumbrarse a deducir cualquier consecuente de una fórmula ωω si el antecedente de la ωω puede conseguir deriva del Axioma 1 por sustitución. Axioma 2 "dice" nosotros que si tenemos algún S en frente de un condicional χχ, podemos transferir S al frente de el antecedente de χχ y el frente de la consiguiente de χχ. Yo uso αα/ββ para indicar que αα obtiene sustituido con ββ. Cuando escribo αα * ββ, tanto en αα ββ indican equiform fórmulas. Por lo tanto, poner a todos juntos...
:Axioma 1 P/((¬¬Q→→¬¬P)→→(P→→P)), Q/¬¬P * 1
1 (((¬¬Q→→¬¬P)→→(P→→Q))→→(¬¬P→→((¬¬Q→→¬¬P)→→(P→→Q))))
:1 * (Axioma 3→→2)
2 (¬¬P→→((¬¬Q→→¬¬P)→→(P→→Q)))
:Axioma 2 S/¬¬P, P/(¬¬Q→→¬¬P), Q/(P→→P) * 3
3 ((¬¬P→→((¬¬Q→→¬¬P)→→(P→→Q)))→→((¬¬P→→(¬¬Q→→¬¬P))→→(¬¬P→→(P→→Q))))
:3 * (2→→4)
4 ((¬¬P→→(¬¬Q→→¬¬P))→→(¬¬P→→(P→→Q)))
:Axioma 1 P/¬¬P, Q/¬¬Q * 5
5 (¬¬P→→(¬¬Q→→¬¬P))
:4 * (5→→6)
6 (¬¬P→→(P→→P))
El de arriba es un poco de falsa historia si se lee como una indicación de cómo me encontré con esta prueba, pero quizás también ofrece un poco más de metalogical insight.