term と formula の違いくらい知ってるに決まってるだろ
だいたい、言語だっていうなら順番はむしろ大事だろ
同じ記号を使っていても、順番が違えば違う式だよ普通

後半は意味不明(あ、等号の意味は当然しってるよ)
自然数の構造を入れて評価する前の「記号列としての式」がちゃんとかけるか、を見てるんでしょ?

あ、もちろん、俺は自然数の標準的な定義も知ってるし
乗法の定義もかけるし、交換法則が成り立つことも証明できるけど
それが何の関係があるのかわからん