体系内で体系自身のモデルの存在を証明するとは

質問

「体系内でその体系のモデルを構成する」という文言をよく目にするのですが、これの意味するところが分かりません。これはどういった行為をいっているのでしょうか。もしくは自身のモデルの存在を証明できる、構成できる体系というのはどういったものなのでしょうか。

　例えばＺＦＣで存在が証明できる対象に、述語を加えてつくった〈Ｍ、∈〉が性質として（つくった実装側で）、ＺＦＣの公理を満たす
ということなのでしょうか

　事実、ＺＦＣ内でＺＦＣのモデルの存在証明ができないことは承知していますが、「体系内（ＺＦＣに限らず）でモデルを構成できる」とはどういう状況を意味するのかを教えて頂きたいがために以上のような書き方をしました。
　お時間あれば、ご教授よろしくお願いします。

回答No.1

rabbit_cat · ベストアンサー

まず、
１．体系内で体系自身のモデルを構築する
ことと、
２．さらに、構築したモデルの完全性を証明する。（存在ではなくて、完全性ですかね）
ことは、別の話です。
実際、ゲーデルの有名な仕事は、ＺＦＣ（等）で、１を行う方法を編み出したことと、２が不可能であることを明らかにしたこと、の２つを行っています。

で、具体的にどうやって１を行うか、いろいろなところに解説があると思います。
単純に言えば、自然数の素因数分解の一意性を利用して、ＺＦＣでの任意の命題 に、１対１で対応するような自然数を定める、ということです。すると、その命題に関して何か考えることは、対応する自然数に関すして考えることと同じになります。

さらに言えば、自然数について何か考えるということのは、つまり、ＺＦＣでの命題そのものですから、この命題（もとの命題についての考え方を考える、メタ命題です）に対応する自然数も一意に定めることができます。

お礼

遅くなってしまいすいません。回答ありがとうございます。

　１、が私が質問していたことと感じますが、とても参考になりました。ある体系内の論理式を扱う際に、直接ではなく（たとえば）自然数などの対象を扱うことに対応させることを「モデルを構成する」といい、そのことによってその体系の性質を調べるわけですね。
　ただ自然数のような対象と体系の関係について追加で伺ってよろしいでしょうか。もしお時間ありましたらお願いします。

　今回は有意義な意見、本当にありがとうございました、助かりました。

補足

「体系内で体系自身を」というのは自然数のような対象と体系には関係があるからこそと思うのですが、これはどういった関係なのでしょうか。
　体系内で扱っているもの（たとえば自然数や集合）の相互関係と体系の論理式の性質を対応つけられるということとは思うのですが、しかし「ＺＦＣが対象として集合を扱い」、「ペアノ算術が自然数を扱う」というのは構文規則から生成される文字列を集合をあらわしているがごとく、自然数をあわらしているがごとく解釈可能ということであって、目の前には文字列以上のものはないわけですよね。

　とすると結局同じ体系を扱うこと自体は変わらないのでしょうか、つまり目的は（たとえば）体系の証明可能性を調べることになるが、
行うことはそのもとの体系を扱って（論理式と対応させた）自然数などの性質をみることであり、そのことが体系自身を調べることになると考えていいのでしょうか。
　この辺の事情の解説をお願いできれば、お時間あれば、よろしくお願いします。