>>457
つづき

もともと，これは，１９世紀の終わりから２０世紀の初めにかけて，集合論が 現れ，カントールのパラドックス，ラッセルのパラドックスなど数々のパラドックスが 発見され，人々が自分たちのロジックに疑いを持ち始めたことから始まる． つまり，それらのパラドックスが集合論のせいなのか，もしかしたら， そもそも我々の数学的推論自身に欠陥があるものなのか自信がなくなってきた のである．

ということで，記号論理学のそのころの目的の一つとして，数学で我々が行っている 数学的推論をきちんと書き出し，それが正しいことを証明することだった．

その枠組みが次の図（冒頭の Syntax & Semantics の絵をもう少し詳細に書いたもの）のようなものである．

連続体仮説およびその否定の ZFC 集合論からの独立性証明は，それぞれが 成り立つ/成り立たないような ZFC 集合論のモデルを作ることによってなされる．

都合のよい単射を加えて， 連続体仮説が成立する/しないモデルを作ればよい．もちろん，そうして作ったモデルが 実際に ZFC の公理系を満たすことを確認しなければならない．ここらあたりの保証が フォーシング（forcing）と呼ばれる技法である．

つづく