数学基礎論講義をこっそり読む（その４）

今回は結構悩みました。p.38 辺りです。まずは系3.11のメモから。

『次の系は上の定理からただちに導かれる』とあるのですが、そこが第一の悩みポイントでした。分かってしまうとなーんだということになるのですが、系3.11の条件の下で、(は複数のxの略記と理解してください。)

としたとき、実は とは同値（お互いに他方の定理を導ける）で、が定理3.10より、の保存的拡大なので、もそうなるということです。

同値になることの証明:
は、からを得て、と置くと。は公理なので、左向き矢印からとなり、について一般化法則を適用すれば を得る。

は、公理 より、が証明できる。
一方、は証明できるので、も証明でき、結局、が証明できる。
反対向きは、仮定によりから証明されるは、（その２ の導出を参考）に同値なので、特ににを代入すると、となり、は証明できるので、。後はで結合して一般化すればよい。□

さて、その次のが私的には問題でした。いや、テキストに書いてあることはまあまあ納得できるのですが、その前提になっているのが であって、どうしてではまずいのかという点が第二の悩みポイントでした。の作り方は別に問題は無いので、結論である が成立しないような反例があるに違いないと...

これも分かってしまうとなーんだなのですが、反例はとして、得られる は一般には成立しません。このことは例の『ある形式体系Tにおいて、が証明できても、が証明できるような、あるが存在するとは限らない』（その３を参考）を使って、とすればよいです。は証明できるので、が証明できることになって、矛盾します。
ちなみにさらに存在の唯一性があると、エルブランの定理を経由して、が証明できる項の存在が証明できるので、上記のような問題は発生しないという理屈になります。

しかし、妙な反例は全て、証明も反証もできない命題の存在から発生しているようで、とても興味深いです。