Dimostrazione del teorema: PA |- S(0)+S(S(0))=S(S(S(0)))  (by G.Valenti) 

  {per_ogni}xy.(x+S(y)=S(x+y))	Assioma PA.4
  {per_ogni}x.a --> a[t/x]		SPEC
  a, a-->b |- b			MP



1.  0+S(0)=S(0+0)			(As.PA.4(0,0), SPEC, SPEC, MP)
2.  0+0=0				(As.3(0), SPEC, SPEC, MP)
3.  0+S(0)=S(0)				(1,2) (sistema formale con uguaglianza)
4.  S(0)+S(S(0))=S(S(0)+S(0))		(As.PA.4(S(0),S(0)), SPEC, SPEC, MP)
5.  S(0)+S(0)=S(0+S(0))			(As.PA.4(S(0),0), SPEC, SPEC, MP)
6.  S(0)+S(S(0))=S(S(0+S(0)))		(4,5)
7.  S(0)+S(S(0))=S(S(S(0)))		(3,6)



===================================

Una dimostrazione alternativa e' la seguente: (FB)


1. S(0)+S(S(0)) = S(S(0)+S(0))  (As.PA.4,SPEC, SPEC, MP)
2. S(0)+S(0)= S(S(0)+0)         (As.PA.4, SPEC, SPEC, MP)
3. S(0)+S(S(0)) = S(S(0)+0)     (1,2) (Assiomi per l'uguaglianza)
4. S(0)+0 = S(0)                (As.PA.3, SPEC) 
5. S(0)+S(S(0)) = S(S(S(0)))    (3,4) (Assiomi per l'uguaglianza)