数学と公理的集合論ZFC

ぴあのん @piano2683

@Rits_math_3rd ここで、普通の数学をZFCで展開できることは、ZFCが「十分な表現能力・構成能力」を持っていることから従います。

ぴあのん @piano2683

@Rits_math_3rd 例えば、「～という位相空間論の定理が証明できる」という事実は、ZFCの立場からすると「『集合に対して、開集合系が定まり位相空間論の公理を満たしているならば～』がZFCから証明できる」という事実に置き換えて解釈します。

ぴあのん @piano2683

@Rits_math_3rd 一方でご存知のように、「公理系から定理を証明すること」と「ある構造がその公理系を満たすこと」は区別して考えなければなりません。

ぴあのん @piano2683

@Rits_math_3rd 仮に「位相空間が矛盾している」とするならば、「位相空間論の公理系から定理を証明すること」は可能でも、その公理系がモデルをもたないので数学的には意味のない理論になってしまいます。

ぴあのん @piano2683

@Rits_math_3rd で、ZFCの立場からモデルについて取り扱うには以下のようにします。ZFCでは「空集合の存在」が仮定されているので、そこから対の公理などを用いて任意の自然数nを構成できます。 また、無限公理も仮定されているので、自然数全体の集合Nの存在も保証されます。

ぴあのん @piano2683

@Rits_math_3rd あとはZ,Q,R,Cをはじめとする数々の数学的対象を構成でき（=その存在がZFCから証明され）、それが考察している公理系のモデルであるかどうかを議論できるようになります。

ぴあのん @piano2683

@Rits_math_3rd 以上で「すべての数学はZFCで展開できる」ということがわかりました。しかし、これは「すべての数学がZFCの言葉で展開されるべき」という主張の論拠にはなりません。

ぴあのん @piano2683

@Rits_math_3rd 公理的集合論の元来の目的は「議論の安全性を保証すること」であって「実際に数学を展開すること」ではないからです。要するに、「やりたいことに応じて適切に言葉を選択しなさい」という話ですね。

ぴあのん @piano2683

@Rits_math_3rd この主張を支える事実として、すべての数学をZFCにおける形式的な議論に置き換えようと言う数学者（集合論者）はいないです。

ぴあのん @piano2683

@Rits_math_3rd 「大抵の素朴な議論は、やろうとすればZFCの言葉で形式化できる」→「形式的な議論に書き換えられるかどうかまじめに考えなきゃいけない部分以外は、直観的な議論で済まそう」となるわけです。

ぴあのん @piano2683

@Rits_math_3rd 以上に書いてきたような意味で、（嘉田先生も仰っているように）「その気になれば数学はZFCから作れる」のです。

ぴあのん @piano2683

@Rits_math_3rd まとめ代わり。「任意の分野の公理系に対してZFCからモデルが作れて、これ以降は各分野の公理だけで語れる」という認識は以下の根拠より不正確です。

ぴあのん @piano2683

@Rits_math_3rd 1.「ZFCからモデルがつくれる公理系」というのは、「ZFCから『ある集合Xが存在してXは公理系のモデルになる』が証明できる」という意味である。もちろんモデルの存在を証明できない公理系も存在する（ZFCの中でZFCを形式化したものがその例になる）。

ぴあのん @piano2683

@Rits_math_3rd 2.公理を記述したり、そこから定理を証明するのにもZFCを前提としなければならない。 以上で本論は終わりです。

ぴあのん @piano2683

@Rits_math_3rd ちなみに近年では、数学の形式化が証明支援の文脈で盛んになってきています。ただしここで基礎になっている記述体系は公理的集合論じゃないですが。

ぴあのん @piano2683

連ツイを終えた

ぴあのん @piano2683

ちなみに「数学と公理的集合論ZFC」ですが、ZFC内で一階述語論理を展開して完全性定理との関連を述べようとも思ったのですが、紛らわしくなるのでやめました。機会があればまたそのうち。