定理証明手習い (52) 公理と定理と実際の用途

+と<についての公理
言ってることはわかります

(dethm identity-+ (x)
  (if (natp x) (equal (+ '0 x) x) 't))

(dethm commute-+ (x y)
  (equal (+ x y) (+ y x)))

(dethm associate-+ (a b c)
  (equal (+ (+ a b) c) (+ a (+ b c))))

(dethm positives-+ (x y)
  (if (< '0 x)
      (if (< '0 y)
          (equal (< '0 (+ x y)) 't)
          't)
      't))

(dethm natp/+ (x y)
  (if (natp x)
      (if (natp y)
          (equal (natp (+ x y)) 't)
          't)
      't))

(dethm common-addends-< (x y z)
  (equal (< (+ x z) (+ y z)) (< x y)))

(equal hoge 't)なんてhogeって書くのといっしょじゃない？と思ったけど
equalで書いておかないとequal-ifで書き換えられないんだな、と今更思うなど

まあそれはいいとして

気になるのはこの５つの公理で+やら<の性質が余すところなく表せているのかということ
それはないよなー
この公理で1+1=2が証明できるとは思えないし
それとも証明できなくっていいんだっけ？

defunで定義した関数なら定義を使って置き換えられるけど
組み込み関数ではそうはいかないし
引数が具体的に与えられれば評価できるけど変数だとそれもできない
無定義述語みたいなもので公理で表すしかない

+を組み込み関数にするんじゃなくて
Scheme手習いでやったみたいに数を定義するところから始めれば、この公理は定理になるんだろうな
それだと何が公理っていう問題はとりあえず回避できてる？
でも何か別のところがやっぱり足りないんじゃね？てなりそうな気がする

ところでこの本（の本編）で証明ができるようになったらどうなるかってのがちょっと気になってます
関数自体については全域性の証明しかしてないので、それだけでは不足ですね
だからこの関数はこういう性質を満たさなければならない、っていう定理を証明することに
なると想像してます
仕様＝定理ってことになるのかな
で、上で「公理はこれで足りてるのかな」と疑問を感じたように
実際何かプログラムのクリティカルな部分を証明したくなったとき
「定理はこれで足りてるのかな」ってなったりしないんですかね
証明したいほどのコードで「こういう定理を満たしますねでもこの定理じゃまだ不足かもしれません」って
いうんじゃ本末転倒な気がしますし

実際にはどういう使い方になるんだろうなあ