[Hilbert] metodo di risoluzione strano(?)

[AlexanderSC]

Ciao a tutti,
recentemente mi sono fiondato su Hilbert e su come dimostrare teoremi attraverso il suo sistema.

Sò che per dimostrare un teorema bisogna arrivare a suddetto teorema attraverso una sequenza di proposizioni, le proposizioni accettabili sono:
1)Le istanze degli assiomi;
2)Le proposizioni ottenute applicando la regola del Modus Ponens a 2 proposizioni precedenti.
3)Proposizioni ottenute attraverso la deduzione (se si fanno uso di premesse).

Ok, però mi sono bloccato davanti un esercizio che vuole che dimostri come teorema questo enunciato:
" \( \neg( A\rightarrow B) \rightarrow ((A\rightarrow B)\rightarrow B) \) "

La risposta è che essa è un istanza dell'assioma:
\( \neg A\rightarrow (A\rightarrow B) \)

Quando l'assioma originale è:
\( B\rightarrow (A\rightarrow B) \)

in pratica non è una riproduzione fedele dell'assioma originale, come la spieghiamo una dimostrazione del genere?

 

[otta96]

Ma non c'è mica solo un'assioma.