Dimostrazione della commutatività di "+".

Dimostro per induzione su n. Fissato m, sia I = {n N | m+n = n+m}

(1). Dimostro che 0 I.
Devo dimostare che m+0 = 0+m
Per la prima equazione della definizione per induzione che ho dato di "+", m+0 = m.
Basta che dimostri che 0+m = m e usi le proprietà di "=".

(1.1). Dimostro (per induzione su m) che 0+m = m.
Sia J = {m N | 0+m = m}
0 J per la prima equazione della definizione di "+".
Dimostro che J è chiuso rispetto a S (passaggio al successore), ossia che:
(1.1.1) se 0+m = m allora 0+S(m) = S(m).
Per la seconda eq. della def. di "+", 0+S(m) = S(0+m).
Da 0+m = m avrei dunque 0+S(m) = S(m). Ne deduco 1.1.1. FineDim.1.1.1.
Dunque J = N. FineDim.1.1.  FineDim.1.

(2). Dimostro che I è chiuso rispetto a S, ossia che:
se m+n = n+m allora m+S(n) = S(n)+m.
Per la seconda eq. della def. di "+", m+S(n) = S(m+n).
Da m+n = n+m avrei dunque m+S(n) = S(n+m). Ne potrei dedurre 2 se dimostrassi che:
(2.1) S(n)+m = S(n+m)
Dimostro anche questo per induzione su m.
Sia K = {m N | S(n)+m = S(n+m)}
0 K in quanto S(n)+0 = S(n) e S(n+0) = S(n) per la prima equazione della definizione di "+".
Dimostro che K è chiuso rispetto a S, ossia che:
(2.1.1) se S(n)+m = S(n+m) allora S(n)+S(m) = S(n+S(m)).
Per la seconda eq. della def. di "+", S(n)+S(m) = S(S(n)+m) e S(n+S(m)) = S(S(n+m))
Da S(n)+m = S(n+m) avrei dunque (per le propr. di "=") S(n)+S(m) = S(n+S(m)). Ne deduco 2.1.1. FineDim.2.1.1
Dunque K = NFineDim.2.1  FineDim.2

(3) Da 1 e 2, per il principio di induzione, ho I = NFineDim

NOTA La dimostrazione formale nell'ambito del calcolo dei predicati del primo ordine (a partire dalla descrizione di <N, 0, S, +> con assiomi formulati in un linguaggio del 1° ordine) sarebbe molto più lunga: occorrerebbe richiamare gli assiomi di "=", esplicitare il ricorso al teorema di deduzione, usare le regole di generalizzazione e di particolarizzazione, ….