命題をモデル論的にチェックする方法 （たぶん前半）

論理に「タブローの方法」というものがあります。しばしば、「タブローにより“証明する”」という言い方がされます。しかしT先生によれば、タブローの方法は証明じゃない、と。何をもって「証明」というかがハッキリしてるわけでもないですが、僕の感覚（厳密性は主張しません）からも「あれは証明じゃない」と感じます。この「感じ」がどこから来るのか、そこらへんのところを少し述べます。

この記事はタブローの方法を紹介するものではありません。タブローの方法も含めて、論理についてのある程度の知識は前提とします。タブローの方法の背景となっている（と思われる）モデル論的なチェックについて考えてみます。一気に書こうと思ったのですが、やっぱり息切れしたので、今日はモデル論の基本事項の復習です。

内容：

1. 命題とその真偽
2. 命題の2次元配置
3. タブローに対する妥当性
4. タブローの普遍妥当性と充足不可能性

命題とその真偽

「真偽が判定できる論理式を命題と呼ぶ」とか習ったと思いますが、これはナンダカよく分かんない話ですね。論理式は、形式的な（人工的な）言語の要素としてそれを定義できます。論理式の集合のなかで、例えば自由変数を含まない論理式として「命題」を定義できますが、それは構文的な定義*1であって、「真偽が判定できる」には直結しません。

構文的な形だけから「真のはずだ」と分かる論理式もありますが、論理式の真偽は通常モデルに対して相対的なものです。モデルMに対して、論理式αが真であることを、M |= α と書くことにします（これは一般的な記法です）。メタな主張「M |= α」が意味を持つには、様々な準備が必要ですが、全部端折ります。M |= α は（メタに）判断できるとして、そのような判断が可能な論理式αを命題と呼ぶことにします。

単一のモデルだけではなくて、たくさんのモデルを考えるので、モデルの集合（プロパークラスかもしれない）をW（worldのつもり）とします*2。M∈W と書いたら、Mは我々が考える範囲のモデルだ、ってことです。モデルMは、単なる集合以上の構造を持つナニモノカのときが多い*3のですが、個体領域（あるいは台集合）として集合を持っているとします。記号の乱用で、モデルMの個体領域＝台集合も同じ記号Mで表すことがあります。

「命題」と呼ばれる論理式の範囲と、「モデル」と呼ばれるナニモノカの範囲が定まって、記号「|=」で表される真偽の判定（妥当性、充足性）もキッチリ決まったものとして話を進めます。

命題の2次元配置

タブローの方法では、命題の集まりを紙面とか黒板とかの2次元の面のうえに描きます。通常は命題群をツリー状に配置します。もともとはマトリックス状に配置されていたようです（そのような配置の現物を見たことはありませんが）。タブロー（＝テーブル）という名前はマトリックスのような形状に由来するのだそうです。

ここでは、オリジナル(?)に戻ってマトリックス状の配置を使います。例えば：

　α1　　β1

　α2　　β2

　α3

このような配置を、入れ子のリストを使って、[[α₁, α₂, α₃], [β₁, β₂]] のように書くことにします。入れ子の内側のリストが縦方向の並び（カラム）であること注意してください。

命題を並べたリストを、A, B など英字大文字で表すとします。A = [α₁, α₂, α₃]、B = [β₁, β₂] とか。“命題のリストのリスト”は、ギリシャ文字大文字 Φ, Ψ などで表します。例えば、Φ = [A, B] = [[α₁, α₂, α₃], [β₁, β₂]]

命題のリスト、例えば [α₁, α₂, α₃] が縦方向の並びであることを強調するために、リストの前に記号∧を付けることにします。∧[α₁, α₂, α₃]、∧[β₁, β₂] という具合です。また、入れ子のリストの外側のリストの前には記号∨を付けます。∨[A, B] = ∨[∧[α₁, α₂, α₃], ∧[β₁, β₂]] のようになります。

今説明したような入れ子のリストを、命題の2次元配置と同一視してタブローと呼ぶことにします。内側のリストはカラムと呼びましょう。ツリー状に描くときは、カラムは枝と呼ばれます。複数のカラムをよりコンパクトに描く工夫がツリー状の配置方法です。

タブローに対する妥当性

単一の命題αに対してその妥当性（モデルに対する真偽） M |= α は定義されています（そう仮定しました）が、タブローの妥当性はまだ定義されていません。

まず、カラム ∧[α₁, ..., α_n] に対して、M |= ∧[α₁, ..., α_n] とは次の意味だとします。

• M |= α₁ かつ M |= α₂ … かつ M |= α_n

M |= ∧[α₁, ..., α_n] とは、M |= (α₁∧ ... ∧α_n) のことなので、事後的に、

• ∧[α₁, ..., α_n] とは、α₁∧ ... ∧α_n の略記と思ってもいい

ことが正当化されます。

次に、タブロー Φ = ∨[A₁, ..., A_k] に対する妥当性を定義します。タブローを構成するカラム A_i （i = 1, 2, ..., k）に対する M |= A_i の意味はすでに定義済みなので、M |= Φ は次のことだとします。

• M |= A₁ または M |= A₂ … または M |= A_k

実例を出しましょう。Φ = ∨[∧[α₁, α₂, α₃], ∧[β₁, β₂]] に関して、M |= Φ だとは、

• M |= ∧[α₁, α₂, α₃] または M |= ∧[β₁, β₂]

です。これは次のように書き換えられます。

• M |= (α₁∧α₂∧₃) または M |= (β₁∧β₂)

さらに、

• M |= (α₁∧α₂∧₃)∨(β₁∧β₂)

となります。つまり、タブローの妥当性は、単一の命題の妥当性に帰着できます。

2次元のマトリックス配置との関係で言えば； 縦方向に並ぶ命題達（カラム）すべての連言（AND結合）を作り、それらの連言達の選言（OR結合）を作った命題が、タブロー全体を表現することになります。

次のことは定義からすぐにわかることですが、注意しておく価値はあります。

1. M |= ∨[∧[α]] とは M |= α のこと。∨[∧[α]] は命題を1個だけ持つタブロー。
2. M |= ∨[∧[]] は常に成立する。∨[∧[]] は命題が1個もない空なタブローを表す。
3. カラムのなかで、命題の順序を変えても妥当性は変わらない。
4. カラムのなかに、同じ命題を重複させても（複数回出現しても）妥当性は変わらない。
5. タブローのなかで、カラムの順序を変えても妥当性は変わらない。
6. タブローのなかに、同じカラムを重複させても（複数回出現しても）妥当性は変わらない。

タブローの普遍妥当性と充足不可能性

命題αが、Wの任意のモデルMに対して妥当、つまり M |= α のとき、αは普遍妥当であるといいます。これは、αが特定のモデルに対してたまたま真なのではなくて、（Wのなかでは）例外なしに正しいことです。一方、どんな M∈W を取っても M |= α とはならないなら、αは充足不可能だといいます。

普遍妥当の否定が充足不可能なのではないので注意してください。メタな言明を論理記号で表すと：

• αが普遍妥当 ⇔ ∀M∈W.( M |= α)

これの否定は、

• αが普遍妥当ではない ⇔ ∃M∈W.( M |= α ではない)

となります。「M |= α ではない」ようなMは、αの反例モデルと呼びます。反例モデルは、対象としている論理体系内の全称命題に対する反例個体（モデルの個体領域の要素）とは別な概念です。もっとも、反例個体を持つモデルが反例モデルになっている場合は多いですが。ともかくも、普遍妥当ではない命題とは、反例モデルを持つ命題*4です。

αが充足不可能であることは次のように書けます。

• αが充足不可能 ⇔ ∀M∈W.( M |= α ではない)

充足不可能の否定は充足可能となります。次が充足可能の定義です。

• αが充足可能 ⇔ ∃M∈W.( M |= α )

まとめると：

1. 論理式が普遍妥当でないとは、反例モデルを持つこと。
2. 論理式が充足不可能でないとは、充足可能なこと。

論理式の体系に否定（記号は¬とする）があって、次が成立しているとします。

• M |= α であることと M |= ¬(¬α) であることは同値である。
• 同じことだが、M |= α でないことと M |= ¬(¬α) でないことは同値。
• M |= α であることと M |= ¬α でないことは同値である。
• 同じことだが、M |= α でないことと M |= ¬α であることは同値。

否定や二重否定の扱いが、メタな立場と論理体系内で“同調している”ような状況です。この状況で、αが充足不可能ならば、どんなモデルMに対しても M |= α ではないので、どんなモデルMに対しても M |= ¬α となります。つまり、充足不可能な命題αの否定¬αは常に（Wの任意のモデルに対して）妥当です。同様に、βがWの任意のモデルに対して妥当（普遍妥当）なとき、その否定¬βはWで充足不可能です。

以上より、次の二つの主張は同じことを言っていて、正しいメタな主張です。

1. 命題αが普遍妥当なら、その否定 ¬α は充足不可能。
2. 命題αが充足不可能なら、その否定 ¬α は普遍妥当。

普遍妥当な命題とは、真な命題と言ってもいいでしょう。すると、

1. 真な命題の否定は充足不可能である。
2. 充足不可能な命題の否定は真な命題である。

この事実がタブローの方法の原理になっていて、命題αが真であることを示すために、「αの否定¬αが充足不可能である」ことを示す戦略がタブローの方法です。より具体的な話は次の機会とします。

*1:構文的な観点から言うなら、自由変数を含まない論理式は「閉じた論理式」と呼ぶべきでしょう。

*2:解釈のための世界Wは固定しますが、Wを色々と動かすときもあります。インスティチューションは、解釈の世界を変えていく系統的な枠組です。

*3:例えば、モデルは順序集合や位相空間かもしれません。

*4:[追記]反例モデルを持つ命題を、「反証可能」と呼ぶようです。だけど、科学哲学で使われる印象が強いので、この言葉は僕は使わないかも。[/追記]