こちらの復習編。
選択公理について
ACとAC'という二つの形の選択公理が出てきた。これらの同値性は新井先生の本で証明されているが、 ITTにおいても同値になるのかどうかはまだ調べていないのでわからない…
選択公理が証明できるということはITTは古典数学より強い体系なのかというと、まあそんなことはないはずで、どこかで代償を支払うはずである。そもそも選択公理が証明できたのも、前件が真であるためにはそれの証明となる具体的なメソッドが必要であるという厳しい条件のおかげで、これが他の定理の証明でどのようにきいてくるのか。ただしそうしたメソッドの要求というのはなかなか地に足ついた考え方でよい。
コーシー列
例えば という無理数は
という列で表せる。以下でやっているのは、もしこれがコーシー列ならば例えば として
をとったとき（そして同時にそれが
より大きいという証明も）、
のような有理数（これは上の列の（0番目から始めて）3番目の要素）を返すことの確認である。
この返す手続きは を定義したときに目撃情報として含まれていなければならない。これはなかなか厳しい話だが、こうすることである程度の解析学ができる。目撃情報を用意できないような無理数についてはITTでは扱えないということかと。
あと具体的にどうやって のコーシー列を作るのかは知らない…
