[090] Traccia della dimostrazione. Notate che la dimostrazione usa solo gli assiomi di Peano e il principio di induzione. Dato ricordiamo che è il precedessore, si veda [1YP] (usando l’aritmetica potremmo scrivere
ma questo teorema è usato nel definire l’aritmetica...) Data una qualunque definiamo la proiezione sulla prima componente
Consideriamo la famiglia delle relazioni che soddisfano
2
3
Mostriamo che sotto queste condizioni ; sappiamo che ; se , allora esiste per cui ma allora da ** segue che , e otteniamo .
La famiglia è non vuota perché . Sia poi l’intersezione di tutte le relazioni in . è dunque la minima relazione in .
Si può verificare che soddisfa le precedenti proprietà * e **. In particolare .
Dobbiamo ora mostrare che è il grafico di una funzione (che è la funzione desiderata), cioè che per ogni esiste un unico per cui .
Sia ; scriviamo per indicare il numero di elementi in ; siccome allora per ogni . Mostreremo che per ogni . Lo dimostreremo per induzione. Sia
Verifichiamo il passo induttivo.
Supponiamo per assurdo che ma ; moralmente in il grafico della “biforca” e la funzione diventa “multivoca”. Definiamo per comodità ; potremmo togliere alcuni elementi a (quelli che non hanno un “predecessore” secondo la relazione **) definendo
⧵
si mostra che soddisfa * e **, ma sarebbe più piccola di , contro la minimalità di . Per provare che , si definisce e si procede allo stesso modo.
Il precente ragionamento mostra anche che la funzione è unica, perché se il grafico di una qualsiasi funzione soddisfacente a * e ** deve contenere , allora .