一階述語論理と集合論は循環している？

お久しぶりです。このブログ、一年近く放ってありましたが、久々の恒真…もとい更新です。今日は、先日見つけた論理学ネタについて。

一階述語論理と集合論は循環していませんか？
一階述語論理の意味論には集合概念が使われていて集合論の公理は述語論理で記述されているように感じるのですが、これは卵が先か鶏が先かの構造になっていないのでしょうか。 

http://detail.chiebukuro.yahoo.co.jp/qa/question_detail/q13108980443

この問題は、質問者自身が言っているようにもちろん擬似問題ではあり、循環はしていないのですが、いい点に気が付いたな、と思います。これは、実は昔から論理学を学ぶ良くできる学生は必ず一度は悩むと言われている問題なのです（ちなみに僕は良くできる学生ではなかったので、自分では気がつきませんでした）。
この質問は、形式的な論理学に関し多くの人が漫然と持っている誤解と混同をあぶり出す、いい話題なため、今回の更新ではこれをネタにさせて頂きたいと思います。

もちろん、この答え、やふー知恵袋に直接書けばいいのかもしれないのですが、主義として知恵袋には書かないことにしている（メディアとしてあれは害の方が大きいと考える）ため、ここでの解答とさせて頂きます。

さて、この質問、実は二つの疑問が混同されていると言うことができます。

1. 述語論理に意味を与えるとはどういうことか？述語論理の意味論を与えるためのモデルは、どこで構成されているのか？
2.  述語論理のモデルを公理的な集合論上で構成することは、何を目的としているのか？

述語論理の意味を与える？
まず一つ目の疑問に関して。この話は、誰もが漠然と当たり前と思っているけれど、でも 突き詰めてみると実はよく分かっていない話が出発点にあります。即ち、「対象レベル」と「メタレベル」の問題です。

対象とメタ
そもそも、形式的な体系、ここでは古典論理の述語論理を例にとりますが、それらをわざわざ定義する目的とは何でしょうか。いろいろな答えがあるとは思いますが、ここでは以下のような方向で考えてみたいと思います。
そもそもの大目的は、人間が数学の場面で行う推論を理解したい、詳細に分析したいということです。ただ、人間の行う推論全体は、あまりに複雑で、なかなか分析をすることができない。複雑な現象を理解したいとき、よくやるのはコンピューターでその現象をシミュレートしてみることですね。例えると、天気を理解したいときは、まず大気圏に関する科学理論から一つのモデルを作り、そのモデルをコンピューター上に入力して、大気圏をコンピューター上でシミュレートし、現実の天気と比べてみます。だから、例えばコンピュータで推論そのものをシミュレーションできるか考えてみよう、というアプローチを採用してみましょう。このとき、シミュレーションのための仮定に相当するのが形式的な公理系なのです。
このとき、シミュレートするための枠組みを表す言葉として、以下の二種類の言葉を定義しましょう。

• メタレベル：シミュレートする人間や、シミュレートされる（実際の数学）の世界のこと。
• 対象レベル：形式的体系、つまりコンピューター上の形式的シミュレーションの世界。

 
こちらは、算数と形式化された自然数論の関係についてのイメージ図です。

形式体系の意味？
ちょっと話を戻しましょう。述語論理などの形式的体系は、一見単なる記号列で、その記号自体に意味があるようには思えません。そして、もしこれらの体系が何の意味も持たないならば、そもそもこれらを考える意味はありません。これらの形式的体系が意味を持つとはどういうことでしょうか。
もちろん、この疑問にはいろいろな考え方があります。一つの考え方は、形式的体系は「現実世界」を模倣することで意味を持つ、と考える事です。 少なくとも、「本当の数学の世界」の何らかの数学的対象「意味論」を、形式的体系が上手く表現していれば、その体系は意味を持つ（そのメタレベルの数学的対象を、うまく対象レベルの記号の世界でシミュレートしている）と考える事ができるでしょう。こういう考え方、つまり対象レベルの形式的体系の意味とはそれが表現するメタレベルの数学的対象によって決まる、を「モデル論的意味論」と呼ぶことにします。

この考え方に従うと、古典命題論理の意味論である「真理関数」や、述語論理の意味論である「タルスキ・モデル」は、対象レベルの形式的な対象ではなく、メタレベルの数学的な対象だということになります。

あまり関係無い話ですが、この形式的体系への意味の与え方の件、いろろなアプローチがあります。

では公理的集合論上では何をしているの？
前節の議論を読んで、疑問が起こった方もいるかもしれません。述語論理のモデルは、多くの場合、領域が無限のものを考えます。だから、モデルは非常に巨大な無限の大きなのものです。そんなものを上手く作ることが出来るのでしょうか？

公理的集合論：無限を分析する対象レベルの理論
無限に関しては、直観に反することがたくさん起こります。従って、数学の世界で「無限に関しこういう事が言えるはずだ」と誰かが言い出した場合、注意深くその主張を分析する必要があります。その分析のツール、それが公理的集合論なのです。公理的集合論は、もちろん対象レベルの形式的体系です。これがシミュレートするのは、人間によって行われる、メタレベルでの、無限に関する数学です。
さて、前述のように、古典述語論理のモデルの構成は、メタレベルの数学の世界で行われます。これも、無限に関する推論の一種です。だから、無限に関する数学的体系である公理的集合論で、シミュレートすることが出来ます。これが、質問者の言うところの「公理的集合論上で古典述語論理のモデルを作る」という作業なのです。
この場合、無理矢理書くと

• メタレベル：人間の数学の世界
• 対象レベル：
• 対象レベル内のメタレベル：公理的集合論
• 対象レベル内の対象レベル：古典述語論理

みたいな感じでしょうか。
下はそのイメージ図。形式的体系の中で別の形式的体系の研究をする事の最も有名な例はゲーデルの不完全性定理で、下図はそれについてのものです。



この古典述語論理のモデルを作る作業、最も典型的なのは完全性定理の証明ですね。多くの場合、完全性定理はメタ理論を人間の数学として行われます（ツオルンの補題とかケーニッヒの補題は数学の世界の原理として登場します）。
しかし、これらの作業をコンピューター上で形式的にシミュレートし、この構成法そのものをじっくり分析することも可能です。この意味で、集合論上のモデル論は、論理に意味を与えるためのものというより、数学的に論理体系を研究するための道具と言った方がいいように思えます。

この話がもう少し発展すると、「では、メタレベルにおけるＸという定理の導出をシミュレートするためには、対象レベル内部のメタレベルとして、どのくらい証明力の強い体系をもってくれば、対象レベル内部の対象レベルでＸが証明できるのか」を考える事ができます。単にめんどくさいようにも思えますが、実は、この分析は、Ｘという数学の定理を分析する上でそれなりに有効である、と言うことが分かってきました。
このように、形式的体系が、メタレベルの数学の分析の道具となってきた、これが20世紀後半以降の数理論理学の研究の流れなのです。