It seems to me that he’s talking at least as much about the fact that S(S(0))+S(S(S(0)))=S(S(S(S(S(0))))) is a theorem of PA, and asking what it means for that to be “true”.
It seems to me that he’s talking at least as much about the fact that S(S(0))+S(S(S(0)))=S(S(S(S(S(0))))) is a theorem of PA, and asking what it means for that to be “true”.