モデル理論について詳しく解説

モデル理論は数学的真理の理論です。それは本質的に、理論が真実である宇宙を定義できれば、その理論は数学的に有効であると言うことから成ります。

モデル理論の概要

これは最初にアルフレッド タルスキーによって完全かつ一貫した方法で定式化され、彼はそれを述語微積分の意味論とも呼びました。その理由は 2 つあります。

• それは、実証^{[ 1 ]}が論理的に何を与えるかに関係なく、真実と論理的帰結の定義を与えます。
• これは、言語の意味の問題に対する部分的な答えを与えてくれます。なぜなら、可能世界において真の文を作ることができれば、言葉には意味があるからです。

しかし、そのルーツはさらに奥にあります。意図的に作成された最初のモデルは、非ユークリッド幾何学の誕生とともに現れます。当初は純粋に演繹的であったこれらの幾何学形状は、モデル、つまり線を指定するための特定の解釈を備えた幾何学的なサポートを提供できるようになった瞬間から、徐々に受け入れられるようになりました。たとえば、ポアンカレは、複素平面の半平面から双曲平面のモデルを与えます。

いわば対称的に、アベ・ビュエとジャン＝ロベール・アルガン（アルガン計画）、そしてガウスとコーシーが複素数の幾何学的モデルを与えました。

モデルはまず、論理理論または数学理論を検証するための構造として機能します。

理論が真実であるモデルが存在する場合、その理論は矛盾していないと言います。公式とその否定の両方を証明できない場合、それは一貫性がある (または一貫している) と言います。理論に一貫性があることを示すことは、必ずしも簡単または可能であるとは限りません。モデルを強調表示するだけで十分であるため、矛盾がないことを示す方が簡単な場合があります。ゲーデルの完全性定理は、モデル理論の基本定理と考えることができます。これは、無矛盾と一貫性という 2 つの概念間の等価性を確立し、適切な演繹システムで証明可能な場合に限り、式がどのモデルでも真であることを示すことを可能にします。これは、レーヴェンハイムの定理 (1915 年) に遡り、数学的真理へのヒルベルト的アプローチに触発された研究を結論づけるものです。したがって、モデルは、矛盾を引き起こさない理論に取り組むという確実性を与えます。

古典的な命題計算のモデル

古典論理の命題微積分では、存在量指定子や全称量指定子は存在しません。数式は、論理コネクタによって反復的にリンクされた原子命題で構成されます。モデルは、原子命題変数ごとに真理値(真または偽) を定義することで構成されます。そうすれば、複雑な式の真偽を推測できるようになります。

数式の複雑さは、ネストされた演算子の最大数によって測定されます。たとえば、

、またはそしていいえ相互にネストされています。しかし、「いいえ」と「そして」 そうではありません。この命題は、最大 2 つのネストされた演算子を持つため、複雑さ 2 です。

複雑度 0 の式は原子式です。真実値を定義するのは選択されたモデルです。

複雑さnのすべての式の真偽が定義されているとします。複雑さn + 1の公式の真偽を定義する方法を示しましょう。 P を、論理結合子を使用して、複雑度n以下の式QおよびRから得られる複雑度n + 1の式とする。したがって、 QとAの真偽はすでに定義されています。

もっている）

: Qが真の場合、否定の定義により、 P は偽になります。 Qが false の場合、同じ理由でP はtrue になります。

b)

: QとRが両方とも true の場合、 P も同様ですが、それ以外の場合はPは false になります。

c)

: QとRが両方とも false の場合、 P も同様ですが、それ以外の場合はPが true になります。

d)

: Qが true でRが false の場合、 Pは false ですが、それ以外の場合はすべてPが true になります。

あらゆるモデルにおける真の公式はトートロジーと呼ばれます。式にn個の原子命題変数がある場合、実際には、 n 個の原子命題にさまざまな真理値を与える2 ^{n 個の}可能なモデルで式の真実性を検証するだけで十分です。モデルの数が有限であるため、命題の計算が決定可能であることになります。式がトートロジーであるかどうかを決定できるアルゴリズムが存在します。

さらに、命題微積分の完全性定理は、トートロジーであることと、適切な演繹系で証明可能であることとの間の等価性を確立します。

例

それを見せてみましょう

(パースの法則) はルール d) を使用したトートロジーです。 Pが真の場合、 形であることそれは本当です。 Pが false の場合、 それは本当です、 は誤りであり、かつそれは本当です。

どのモデルでも真実ですが、

トートロジーです。したがって、自然演繹などの演繹体系によって証明することもできます。

しかし、

証明できない。実際、 Pが偽であるモデルでは、 も誤りです。

述語計算のモデル

古典論理の一次述語の計算では、使用される述語が変数に適用されます。したがって、モデルを定義するには、その要素が変数に割り当てられる値として機能するセットを導入することが適切です。命題微積分の場合と同様に、与えられた領域における原子式の真偽を定義することから始め、その後、複合式の真偽を徐々に定義していきます。したがって、理論の基本的なシンボルから構成される一次論理のすべての複雑な式の真実性を連続的な段階で定義できます。

論理演算子 (否定、結合、存在など) が含まれていない場合、式はアトミックです。ここでのアトミックとは、式にシンボルが 1 つだけ含まれることを意味するのではなく、基本的な述語シンボルが 1 つだけ含まれることだけを意味します。その中の他の名前はオブジェクト名であり、非常に複雑になる場合があります。式がアトミックであるということは、式に部分式が含まれていないことを意味します。これは論理的な原子性です。

モデル内の原子式の解釈

一次言語の解釈は、次の要素によって定義されます。

• 空でない集合 U、理論の世界。言語で言及される各オブジェクト名 (定数) は、U の要素に関連付けられます。
• この言語で言及されている基本的な単項 (1 位) 述語はそれぞれ、この述語の拡張である U の一部に関連付けられています。述語が真であると判断する値のセットです。この言語で言及されている基本的なバイナリ述語はそれぞれ、デカルト積U × U の一部に関連付けられています。これは、述語が真となるすべてのペアのセットです。同じことが三項述語、またはより高いアリティの述語にも当てはまります。
• 言語で言及される各単項演算子は、U の U の関数に関連付けられます。言語で言及される各二項演算子は、U の U × U の関数に関連付けられます。同じことが、より高いアリティの演算子にも当てはまります。

集合 U、またはそれが一部である解釈は、この理論のすべての公理がこの解釈に対して真である場合の理論のモデルです。

モデルという言葉は複数の意味で使用されることがあります。時には集合 U を指定し、時には真の原子式の集合を、時には解釈を指定します。多くの場合、理論のモデルを言うと、自動的にそれが真実であると仮定します。しかし、理論はモデルにおいては誤りであるとも言えます。

複雑な数式の真実を定義する

理論の解釈が得られれば、定数、述語、および基本演算子のみに言及するすべての式の真実性を定義できます。原子の式から始めて、より複雑な式に再帰的に進みます。

命題計算のモデルに関連する段落で定義されたルールを採用し、全称および存在量指定子に関連する 2 つの追加ルールを定義します。

e)

: Qの解釈において、 xの自由な出現すべてを U の要素に置き換えることによって得られる式の 1 つが false の場合、 Pは false になります。そうでない場合、 Qにx以外の自由変数がない場合、 P はtrue になります。

f)

: Qの解釈において、 xの自由な出現すべてを U の要素に置き換えることによって得られる式の 1 つが true の場合、 Pは true になります。そうでない場合、 Qにx以外の自由変数がない場合、 P はfalse になります。

e) と f) により、すべての閉じた式、つまり自由変数なしで真偽を定義できるようになります。

したがって、自由変数を持たない一次論理のすべての複雑な式の真偽は、特定のモデルで決定できます。

あらゆるモデルにおける真の公式は、論理法則または定理と呼ばれます。命題微積分に関しては、ゲーデルの完全性定理は、適切な演繹系における論理法則と証明可能な公式との等価性を述べています。命題の計算とは異なり、考慮できるモデルの数は一般に無限であるという事実を考慮すると、この結果は注目に値します。さらに、命題の計算とは異なり、述語の計算は決定可能ではありません。

例

式

は論理的な法則です。実際、空ではない U モデルを考えてみましょう。その場合、可能性は 2 つあります。

• あるいは、 yにUの任意の値が代入されている場合に真の値を R( y ) に代入し、この場合、 xに U の任意の値を代入します。
  $$ {R(x) \to R(y)} $$
  したがって、 U のすべてのyに対して true になります。
  $$ {\forall y \; (R(x) \to R(y))} $$
  は U にも当てはまり、 xも U の要素を示します。
  $$ {\exist x \; \forall y \; (R(x) \to R(y))} $$
  Uでは真実です。
• または、U の少なくとも 1 つのyに対して R( y ) に値 false を代入します。次に、この要素をxで指定しましょう。つまり、U全員にとって、
  $$ {R(x) \to R(y)} $$
  それは真実なので、
  $$ {\forall y \; (R(x) \to R(y))} $$
  U では true であるため、
  $$ {\exist x \; \forall y \; (R(x) \to R(y))} $$
  も真実です。

どちらの場合も、式は true です。 U は任意であるため、この式はどのモデルにも当てはまり、演繹系によって証明することもできます。

一方、式は

証明できない。 2 つの要素aとb を含む集合 U をモデルとして取り、P と Q( a ) を true、Q( b ) を false に設定するだけで十分です。 U では false ですが、 は true ( x = aの場合)。その結果、 は U では false です。反証可能な式は定理ではありません。

直観主義的論理のモデル

これまでに提示したモデルは古典論理のモデルです。しかし、他の論理、たとえば、前提から実証を構築する論理である直観主義論理もあります。このロジックにはモデルの理論、つまり完全性定理を備えたクリプキ モデルがあります。つまり、式は、クリプキ モデルで真である場合に限り、直観主義的ロジックで証明可能です。

これらのモデルにより、たとえば次の質問に答えることができます。 F を閉じた式とします。

• あるいは、 F は直感的論理の定理ではありません。これを示すには、式を無効にするクリプキ モデルを示すだけで十分です。
• またはF は古典論理の定理です。これを示すには、古典論理の演繹システムで証明を提供するだけで十分です。次に、2 つのサブケースがあります。

あるいはFも直観論理の定理です。これを示すには、直観主義的演繹系で証明を与えるだけで十分です (または、すべてのクリプキ モデルでFが真であることを示すだけです)。

あるいは、 F は直観的論理では証明できません。これを示すには、式を無効にするクリプキ モデルを与えるだけで十分です。

これは次のことを証明する方法です。

$$ {(\lnot \forall x \;F(x)) \to (\exists x \; \lnot F(x))} $$

は古典論理の定理ですが、直観主義論理の定理ではありません。

$$ {(\lnot \exists x \;F(x)) \to (\forall x \; \lnot F(x))} $$

は直観主義論理 (および古典論理) の定理です。

Kripke モデルは、モーダル ロジックのモデルを提供するためにも使用されます。

モデルの適用例

すでにモデルの応用例を示しました。

• 式を満たす、または逆に反証する（たとえば、古典論理では真の式が直観主義論理では偽であることを区別します。式はどの古典モデルでも真ですが、直観主義論理にはそれを反証するモデルが存在します）。
• すべての公理を満たすモデルを示すことによって、理論または公理系が矛盾していないことを証明します。

公理系に関しては、公理相互の独立性を示したり、別の系の一貫性に依存して公理系の一貫性を確立したりするためにモデルも介入します。いくつか例を挙げてみましょう。

幾何学では、ユークリッドの第 V 公準は幾何学の他の公理から独立しています。実際、一方では、ユークリッド幾何学の平面は、この公準が真実であるモデルです。一方、ポアンカレ半平面は、この公準が偽となる双曲幾何学のモデルです。このモデルでは、宇宙(双曲面) は上部の開いたユークリッド半平面の点で構成されます。

0 \}” >。双曲線平面の線は、方程式x = aまたは( x − a ) ² + y ² = R ²の集合です。

この宇宙では、線とその線の外側に点を与えた場合、その点を通り、最初の線と交わらない線が無限に存在します。

この例では、別のモデルの他のオブジェクト (ユークリッド半平面の半線と半円) を使用して、新しいモデルのオブジェクト (双曲面の直線) を定義できることがわかります。ユークリッド モデルの一貫性を仮定すると、双曲モデルの一貫性が確立されます。

別のモデルの相対的な一貫性を示すためにモデルを使用することは非常に一般的です。たとえば、ZF で示される公理的集合論を考えてみましょう。 ZFCで示される選択公理を追加する ZF についても考えてみましょう。 ZF が一貫している場合は、ZFC も一貫していることを示すことができます。実際に、任意の序数αに集合F _αを関連付ける序数で定義された関数 F を定義することができます。

となることによって：

• L はZF の公理をすべて満たします
• Lに属する集合F _{α は}、 F _αがF _β (β < αの場合)超限漸化によって定義されるという意味で構築可能です。
• Lのすべてのxについて、 x = F _αとなるような最小の序数αとしてxの位数を定義します。
• Lの任意のxに、最小次数のxのy要素を関連付けることができ、 y = f ( x )を設定することでLにおけるLの関数f を定義します。

次に、 Lで検証する関数を定義しました。

。言い換えれば、 f はLの選択関数であり、 L はZF および選択公理を満たします。したがって、 L はZFC のモデルです。

まだ集合論の途中ですが、

そして、任意の整数nに対して、 ( R _nの部分のセット)、任意の整数nに対するR _nの和集合は、無限の公理を除く ZF のすべての公理を検証するモデルを定義します。これは、この最後の公理が他の公理から証明できないことを証明します。