２０２２年４月２８日 （ｓｉｎｇｕｌａｒの日）
今回は前回からの続きとして。
ｈａｎ公理体系をｓｉｎｇｕｌａｒ公理体系の観点から見ていきます。
ＺＦでは、無限公理で｛｝を採用していますね。
だから、ＺＦのｔｅｒｍには｛｝が設定されていると言えなくもない。
しかし、｛｝は記号なのですから。
どこかで定義する必要があります。
ｔｅｒｍ設定では、採用記号の種類だけを提示し、記号の定義はしません。
では、どこでやるのか？
通常は公理の方で実施します。
ところが、ＺＦ中には、｛｝の具体化公理が登場しません。
これでも大丈夫と思ってきたわけです。
理由は？
公理的集合論の前に、素朴集合論というのがあり。
素朴なんだから、記号の定義なんかアドホックに遣りたい放題。
だから、矛盾したので、ＺＦで公理化したのですが。
その公理化がチンケなの。
記号｛｝の定義をＺＦ内でやらずに済むと思ってきたわけだ。
これがｈａｎ公理体系の基本思想です。
つまり、便利な簡略記号として使うというポリシー。
しかし、それは、記号を素朴に考えるということ。
非常に危険な思考法です。
「簡略記号として導入しておけばＯＫ宇宙。」
なんて考え出すと、それはもう、素朴集合論の世界ですよ。
その程度の脳なのですよ、猿とは。
それじゃ駄目だと認知できてないの、ＺＦのｈａｎ公理体系では。
何の為の公理化なのかね、矛盾してるのに。
いいですか、集合論は数学のベースになるＯＳです。
数学全体を乗せる場所。
全ての数学が翻訳できる場所。
証明作業の基本。
ここ以外の、何処で、定義するのよ、集合関係の関数や個体定数を。
これで具体化問題が大事になることが判明すると言う筋書き。
｛｝の具体化公理、どう設定する気ですか？
教科書では、簡略記号として、素朴に
｛ｘ｝＝｛ｘ，ｘ｝・・・（１）
と設定していますが。
アノネー、これが出来るのは、関数記号
｛ｘ，ｙ｝
をｔｅｒｍで採用した後の話。
これをｔｅｒｍで採用しても、定義は別儀。
そこで、対の公理
∀ｘ∀ｙ∃A∀t（ｔ∈A «（ｔ＝ｘ ∨ ｔ＝ｙ））・・・（ＡＰ）
を持ち出して具体化しようと画策するでしょう。
外延性公理で一意性が保証されると言ってますが。
∀ｘ∀ｙ∀t（ｔ∈｛ｘ，ｙ｝↔（ｔ＝ｘ ∨ ｔ＝ｙ））・・・（｛ｘ，ｙ｝）
と直訳して良いのか？
ωの場合は、直訳で一意決定できてないし。
⏀の場合は、矛盾の原因になっている。
さて、｛ｘ，ｙ｝の場合や如何に？
本当に、外延性公理で一意性が保証されているの？
一意決定されていると言い張るのは、素朴な直観なのでは？
ここから、更に分析していくと、事の重大さが判ってくるというシナリオ。
仮に、何らかの｛，｝具体化公理をＺＦに追加導入すると仮定します。
キチンと議論するため、⏀と｛，｝だけでｔｅｒｍ設定し。
具体化公理を追加した集合論を
ＺＦ（⏀，｛，｝）
とします。
一方、従来の、｛，｝ｔｅｒｍ設定してないＺＦをＺＦ（⏀）とすると。
ＺＦ（⏀）を公理的集合論という場合。
それは、ｓｉｎｇｕｌａｒ体系ですね。
｛｝がｔｅｒｍ設定されてないのだから。
こういう風にキチンと把握しないから、矛盾が認知できないの。
それが証拠に、ＺＦ（⏀）の場合、
「対の公理（ＡＰ）は、何を意味するのか？」
という根本的な課題が生起します。
公理体系における∀や∃の範囲問題です。
ｔｅｒｍに｛ｘ，ｙ｝が採用されてなければ。
エルブラン宇宙に対応する対象が無いの。
「具体例が存在しない体系とは何か？
何であるべきか？」
ＺＦ（⏀）のエルブラン宇宙では、ホクト、（ＡＰ）は偽になるの。
だって、ＺＦ（⏀）のエルブラン宇宙は個体定数⏀だけの単一宇宙ですよ。
関数記号がないの。
要素が２個の集合は生成できません。
そこで（ＡＰ）考えて、どうするというのか？
というわけで、ＺＦ（⏀，｛，｝）を考える必要があるわけですが。
今度は、｛ｘ，ｙ｝の一意決定性問題が勃発するという仕組み。
それでも、何とか、この難局を乗り越えたと仮定します。
そこから、（１）により、｛ｘ｝が定義されるわけですが。
こういう（１）なんてのは、ＺＦ中に出てきませんね。
なにせ、便宜上の記号とかホザイテいるのですから。
そんなことを言ってるから、ｔｅｒｍ設定の重要さが把握できないのよ。
ここから、非常に大事な論点に入ります。
以後の集合論はＺＦ（⏀，｛｝）。
つまり、エルブラン宇宙が個体定数⏀と関数記号｛｝で生成される理論です。
ＺＦの公理中に出現する記号だけでエルブラン宇宙を考えるということ。