Un prueba en la teoría Nicod-Lukasiewicz

Veamos la prueba de «p → p» en el sistema Nicod-Lukasiewicz.

Recordemos el axioma: p/qr | (s/ss) / (sq → ps)

Sustituyendo en él: 'p' por 'p/qr', 'q' por 's/ss', 'r' por 'sq → ps' y 's' por 't', obtememos:

[p/qr|(s/ss)/(sq → ps)] | t/tt / (t|s/ss → p/qr|t)

Nótese que la parte entre corchetes es el axioma mismo, por tanto podemos aplicar la regla, lo cual nos permite afirmar:

(I)  t|s/ss → p/qr|t


Sustituyendo, nuevamente en el axioma, 'p' por 't|s/ss', 'q' y 'r' por 'p/qr|t', 's' por 'w', obtenemos:


(t|(s/ss) → p/qr|t) | (w → w) / (w|(p/qr|t) → t/(s/ss)|w)

Y aplicando la regla (teniendo en cuenta I), obtenemos:

(II)   w|(p/qr|t) → t/(s/ss)|w


Ahora, realizamos en (II) la siguiente sustitución:

'w' por 'p/qr'; 'p', 'q' y 'r' por 's'; 't' por 'sq → ps', 's' por 't' y 't' por 'sq → ps'. Obtenemos el condicional:

p/qr|(s/ss)/(sq → ps) → (sq → ps)/(t/tt)|p/qr

Cuyo antecedente no es sino al axioma, y por ende:

(III)    (sq → ps)/(t/tt)|p/qr

Sustityendo en (I) 't' por '((st → ts)|t/tt)' y 's' por 't':

(st → ts)/(t/tt)| t/tt → p/qr | (st → ts)/(t/tt)

Y como reemplazando en (III) 'p', 'q' y 'r' por 't' nos da:

 (st → ts)/(t/tt)|t/tt

Luego:

(IV)     p/qr | (st → ts)/(t/tt)


Reemplazando en (IV) 'p' por 't|s/ss' y 'q' y 'r' por 'p/qr|t', obtenemos:

(t|s/ss → p/qr|t) | (st → ts) / (t/tt)

Aplicando la regla (teniendo en cuenta (I)), deducimos:

⊢ t/tt

Que es lo que se quería probar.