Studiamo su [SM] la definizione precisa di regola derivabile.



Sia Numbers (N) il sistema formale definito da
S={0,s,(,),i,N}
W={xiN | x in S*}
Ax={s(s(0))iN}
R={pippo,pluto}

dove

pippo= __xiN__ per ogni x in S*
        s(x)iN

pluto= _s(0)iN_
         0iN

dimostrare  che pluto non e' derivabile in N\{pluto} equivale a dire che non e' possibile che
  s(0)iN  |-N\{pluto}  0iN 
 (cioe' che la fbf 0iN non sia derivabile in N\{pluto}  utilizzando l'insieme di ipotesi {s(0)iN})
Definiamo una proprietà dei numeri naturali da poter dimostrare per induzione e che sia equivalente al fatto che non sia possibile che  s(0)iN  |-N\{pluto}  0iN
Prendiamo la seguente proprieta':
"se una fbf alpha di N e' ottenuta come conclusione di una derivazione in N lunga n (con n>=1) e che eventualmente utilizza ipotesi nell'insieme {s(0)iN},
allora alpha contiene un numero di simboli 's' maggiori o uguali ad 1"

Caso base n=1:
per n=1 la deduzione (derivazione) è composta unicamente dalla fbf alpha che, per definizione di derivazione,  deve essere necessariamente
un assioma oppure una ipotesi (in questo caso s(0)iN). Notiamo che alpha non puo' essere la conclusione di una regola di inferena di N\{pluto} (quindi pippo)
poiche' la derivazione e' lunga 1.
Se alpha e' un assioma allora alpha=s(s(0))iN e quindi la proprieta' vale.
Se alpha e' una ipotesi allora alpha=s(0)iN e quindi la proprieta' vale.

Caso induttivo n>1
dobbiamo ora far vedere che la proprieta' vale per un n generico supponendo che valga per tutti i numeri minori di n.
Sia quindi alpha derivabile con una derivazione lunga n.
Per definizione di derivazione, alpha puo' essere:stata inserita come conclusione della derivazione perche' e'

    Un'assioma
    Un'ipotesi
    Una conclusione di una regola (che non puo' essere che pippo, poiche' stiamo supponendo che alpha sia derivata nel sistema N\{pluto})

Nel primo e nel secondo caso possiamo ragionare come per il caso base, ottenendo che la proprieta' vale.
Se invece alpha e' stata derivata utilizzando la regola pippo, allora alpha ha la forma s(x)iN e nella derivazione e' presente la premessa della regola pippo,
cioe' la fbf xiN.
Prendiamo allora la parte di derivazione che termina con xiN
Questa e' anch'essa una derivazione corretta, ed ha xiN come conclusione, ed e' piu' corta di n.
Quindi per l'ipotesi induttiva (cioe' che la proprieta' vale per tutte le derivazioni piu' corte di n)
per vale la proprieta', poiche' e' una derivazione sicuramente piu' corta di n.
Quindi xiN contiene un numero di 's' maggiore o uguale ad 1.
Questo comporta che alpha contiene un numero di 's' maggiore o uguale a 1.

Avendo dimostrato il caso base e il caso induttivo, possiamo applicare l'induzione e dimostrare che
la proprieta' vale per ogni n>1.

Questo fatto ci permette di dimostrare che non e' possibile che che  s(0)iN  |-N\{pluto}  0iN
Infatti, supponiamo per assurdo che  esista una derivazione con conclusione 0iN nel sistema  N\{pluto}  e che utilizzi solo ipoteri in { s(0)iN},
Allora per la proprieta' appena dimostrata per induzione (che vale per ogni n>1), la fbf 0iN dovrebbe contenere un numero di 's' maggiore od uguale ad 1,
ma questo e' impossibile, poiche' in tale fbf il numero di n e' 0.