直観主義論理: 可能世界意味論(命題論理)

公開日: 2022/09/08

最終更新: 2023/05/07

この記事では、直観主義論理に対する意味論のうち、可能世界意味論(possible world semantics) ないし クリプキ意味論(Kripke semantics) と呼ばれるものを紹介する。

なお以下では、命題変数の加算無限集合 $PV$ が与えられているものとし、(命題)論理式の集合 $Fml$ を以下のように帰納的に定める。

$⊤, ⊥ \in Fml$
$^{\forall} p \in PV . p \in Fml$
$φ, ψ \in Fml ⟹ φ \land ψ, φ \lor ψ, φ \to ψ \in Fml$

また、 $\neg φ \overset{def}{=} φ \to ⊥$ とする。

非形式的な説明

直観主義論理(intuitionistic logic) の1つの特徴は、排中律( $φ \lor \neg φ$ )が一般には成立しないことである。一方で、これは「真でも偽でもない命題が存在する」「真・偽に加えて第3の真理値を導入する」ということではない。実際、直観主義論理は3値論理としては特徴づけられない¹。

このような一見奇妙な振る舞いは、「真である」という概念の捉え方に起因する。直観主義は「私たちの認識から独立した真理」という見方を批判し、「 $φ$ が真である」と言うためには、 $φ$ が真であることの証明が実際に構成できなければならないと主張する。

この観点からすると排中律が成り立たないのは自然なことである。なぜなら、数学の未解決問題のように、まだ肯定的な証明も否定的な証明も得られていない命題が存在するからである。やや紛らわしいかもしれないが、「偽である(真とはいえない)」と「否定が真である」は等価ではないということになる。

以上のような立場のもとでは、論理結合子の意味は古典論理とは異なった形で解釈されることになる。非形式的な説明としてしばしば引き合いに出されるのは、以下の BHK解釈(BHK interpretation) である。これは、各論理結合子の「証明が得られる」とはどういうことかを説明している。

定義. BHK解釈

$⊥$ の証明は存在しない
$φ_{1} \land φ_{2}$ の証明は、 $φ_{1}$ の証明と $φ_{2}$ の証明の組である
$φ_{1} \lor φ_{2}$ の証明は、 $i \in {1, 2}$ と $φ_{i}$ の証明の組である
$φ_{1} \to φ_{2}$ の証明は、 $φ_{1}$ の任意の証明を $φ_{2}$ の証明へと変換する(実効的な)手続きである

そしてこのBHK解釈を反映しているのが、本ページで説明する 可能世界意味論 である。このモデルにおいては、命題の真偽は絶対的に決まるのではなく、1つ1つの「状態」において決まる。そして、状態と状態の間の遷移関係を「時間の経過」のように捉え、遷移とともに真である(証明が得られた)命題が増えていくようにする。ちょうどこれは、数学者が時間の経過の中で証明を行い、だんだんと数学的知識を増やしていくような様子をモデル化しているといえる。

定義

まず、状態とその間の関係をフレームとして定義する。

定義. フレーム

直観主義命題論理の フレーム(frame) を、以下から成る組 $⟨ W, \leq ⟩$ のこととする。

$W$ : 非空な集合
$\leq$ : $W$ 上の擬順序

$W$ の元のことを 状態(state) ないし 可能世界(possible world) という。 $\leq$ のことを 到達可能性関係(accessibility relation) という。

次に、古典命題論理と同様に、各命題変数の真偽を付値によって与える。ただし、付値は各状態に対して定義される。

定義. モデル

直観主義命題論理の モデル(model) を、フレームに以下を加えた組 $⟨ W, \leq, (v_{w})_{w \in W} ⟩$ のこととする²。

$v_{w} : PV \to {0, 1}$ であって、以下の条件を満たすもの

^{\forall} w, w^{'} \in W . w \leq w^{'} ⟹ (^{\forall} p \in PV . v_{w} (p) = 1 ⟹ v_{w^{'}} (p) = 1)

各 $v_{w}$ のことを 付値(valuation) といい、この条件のことを 遺伝性(heredity) または単調性(monotonicity)という。

補足. 遺伝性の条件は、「ある状態で命題が真と分かれば(= 証明が得られれば)、その後の状態でも真であると分かっていることに変わりはない」ことを反映していると解釈できる。なお後述するが、この性質は一般の論理式に拡張できる。

次に、命題変数に対して定義された真理値を論理式全体に拡張し、「モデル $M$ の状態 $w$ で論理式 $φ$ が真である」という関係を定義する。含意 $\to$ に関する定義が特徴的である。

定義. 充足関係

モデル $M = ⟨ W, \leq, v ⟩$ と状態 $w \in W$ に対して、論理式 $φ$ の充足関係 $M, w ⊨ φ$ を以下のように帰納的に定める³。

$p \in PV$ : $M, w ⊨ p \overset{def}{⟺} v_{w} (p) = 1$
$M, w ⊨ ⊤$
$M, w ⊭ ⊥$
$M, w ⊨ φ \land ψ \overset{def}{⟺} M, w ⊨ φ and M, w ⊨ ψ$
$M, w ⊨ φ \lor ψ \overset{def}{⟺} M, w ⊨ φ or M, w ⊨ ψ$
$M, w ⊨ φ \to ψ \overset{def}{⟺}^{\forall} w^{'} \geq w . M, w^{'} ⊨ φ ⟹ M, w^{'} ⊨ ψ$

このとき( $M$ において) $w$ で $φ$ が真であるという。モデルが明らかな場合は $M$ を省略して $w ⊨ φ$ と書く。

また、論理式の集合 $Γ \subseteq Fml$ に対して、

w ⊨ Γ \overset{def}{⟺}^{\forall} φ \in Γ . w ⊨ φ

なお、否定は $φ \to ⊥$ として定義されていたので、帰結関係は次のように定まる ( $w ⊭ φ$ との違いに注意)。

w ⊨ \neg φ ⟺^{\forall} w^{'} \geq w . w^{'} ⊭ φ

補足.

\to

に関する定義の「任意の

w^{'} \geq w

となる状態

w^{'}

で...」という全称量化は、冒頭の説明のBHK解釈を反映したものである。BHK解釈によれば、「

φ \to ψ

が真である」と言えるためには、「

φ

の証明が与えられたら、

ψ

の証明を構成するような手続き」が構成できていなければならない。そして

φ

の証明はどのタイミングで与えられても良いはずなので、「この先の任意の状態で...」という量化をすることになる。

以下では、フレームを下図のように有向グラフで表し、各状態で論理式が真なら $+$ 、偽なら $-$ を付けて表す。関係 $\leq$ を表す辺のうち、対称性・推移性により必要となるものは適宜省略する。

w_{1} - φ w_{2} + φ w_{3} + φ \leq \leq

最後に、推論の妥当性を、任意のモデルにおいて前提から結論に充足関係が保存されることとして定義する。

定義. 妥当性

$Γ \cup {φ} \subseteq Fml$ とする。 $Γ$ から $φ$ への推論が 妥当である(valid) ことを、任意のモデル $M = ⟨ W, \leq, (v_{w})_{w \in W} ⟩$ と状態 $w \in W$ に対して $w ⊨ Γ$ ならば $w ⊨ φ$ であることと定義する。これを $Γ ⊨ φ$ と書く。

なお、前提を真・結論を偽とするような状態が存在するモデルのことを 反例モデル(counter model) という。すなわち、からへの推論に対する反例モデルは以下を満たす。

性質

基本的な性質

遺伝性の拡張

モデルの定義では、遺伝性の条件は命題変数の場合に限定されていた。この性質は論理式全体に拡張できる。

命題.

任意のモデル, となる状態に対して、

証明.

論理式の構成に関する帰納法で示す。 $\to$ についてのみ示す。

$w ⊨ φ \to ψ$ を仮定する。 $w^{'} ⊨ φ \to ψ$ を示すために、 $w^{″} \geq w^{'}$ となる $w^{″} \in W$ を任意にとる。このとき、推移性より $w^{″} \geq w$ でもあるから、仮定より $w^{″} ⊨ φ ⟹ w^{″} ⊨ ψ$ となる。これと充足関係の定義より $w^{'} ⊨ φ \to ψ$ となる。

※ $\to$ の場合には帰納法の仮定を使う必要がない。

(閉じる)

選言特性

古典論理にはない性質として、次の 選言特性(disjunction property) がある⁴。

命題.

なお、これが古典論理では成り立たないことは、例えば適当な命題変数に対してが反例になることから分かる。

証明.

概略のみ示す。 $⊭ φ_{1}$ と $⊭ φ_{2}$ を仮定し、対偶を示す。仮定より、各 $i = 1, 2$ に対してモデル $M_{i} = ⟨ W_{i}, \leq_{i}, (v_{w})_{w \in W_{i}} ⟩$ と状態 $w_{i} \in W_{i}$ が存在して、 $M_{i}, w_{i} ⊭ φ_{i}$ となる。

反例モデルのフレームとして、 $W_{1}$ と $W_{2}$ のそれぞれ $w_{1}, w_{2}$ より後の部分だけ取り出し、それらに新たな最小元 $w_{0}$ を付け加えたようなものを考える(下図参照)。付値については、状態 $w_{0}$ では全て $0$ とし、 $W_{i}$ の元に対しては各 $M_{i}$ での値を適用する。これにより構成されたモデルを $\overset{―}{M}$ とする。

w_{0} - φ_{1} - φ_{2} ∴ - φ_{1} \lor φ_{2} w_{1} - φ_{1} ⋮ \leq W_{1} w_{2} - φ_{2} ⋮ \leq W_{2} \leq \leq 遺 伝 性 遺 伝 性

このとき、 $\overset{―}{M}$ においても $w_{1}$ で $φ_{1}$ が偽になり $w_{2}$ で $φ_{2}$ が偽になることが示せる。これと遺伝性(の対偶)より $w_{0}$ では $φ_{1}, φ_{2}$ がともに偽になるため、 $\overset{―}{M}, w_{0} ⊭ φ_{1} \lor φ_{2}$ となり、 $\overset{―}{M}$ が反例モデルになることが分かる。

(閉じる)

有限モデル性

妥当ではない推論に対しては反例モデルが存在するが、直観主義論理では任意の反例モデルを状態数が有限のモデルへと変換できる。このような性質を 有限モデル性(finite model property) という。

命題.

のとき、状態数が有限の反例モデルが存在する。

証明. 反例モデルの状態集合

に対して適当に同値類をとることで有限のモデルを構成する。詳細は割愛⁵。

系.

直観主義(命題)論理は決定可能である。すなわち、(前提が有限個の)任意の推論に対して、それが妥当か非妥当かを計算する実行的な手続きが存在する。

証明.

適当な証明論を用意することで妥当な推論を枚挙できるので、妥当な推論の判定は実効的に行える。非妥当な推論については、有限モデル性より、有限なモデルを順に枚挙していくことにより反例モデルが発見できる。

(閉じる)

推論に関する性質

まず、直観主義論理は古典論理に含まれている。

命題.

(直観主義論理で)のとき、からへの推論は古典論理でも妥当である。

適当な証明体系を与えれば簡単に示せるが、今回はモデルによる証明を与える。

証明.

対偶を示す。(概略) 前提を全て真・結論を偽にする古典論理の付値 $v : PV \to {0, 1}$ が存在することを仮定する。状態1つだけ( $w_{0}$ )のフレームで付値を $v$ により与えるようなモデル $M$ を考えると、 $v ⊨ φ ⟺ M, w_{0} ⊨ φ$ となることを論理式の構成に関する帰納法で示せる。

(閉じる)

補足. なお、この証明と同様に考えると、状態

が「

となる状態が自分以外にない」ような状況のとき(下図参照)、

上では充足関係が古典論理のように振舞うことが示せる(例えば

)。

一方で、古典論理では妥当な推論の一部が実際に非妥当になることが確認できる。

命題. 非妥当な推論

排中律:
二重否定除去:
パースの法則:
ド・モルガン(の片方):
対偶:

証明.

排中律についてのみ証明を与える。命題変数 $p \in PV$ を1つとって固定し、以下のようなモデル $M = ⟨ W, \leq, v ⟩$ を考える。

$W = {w_{1}, w_{2}}$
$\leq = {⟨ w_{1}, w_{1} ⟩, ⟨ w_{2}, w_{2} ⟩, ⟨ w_{1}, w_{2} ⟩}$ (確かに擬順序)
$v_{w_{1}} (p) = 0, v_{w_{2}} (p) = 1$ (その他の引数のとき値は $0$ )

付値の定義より $w_{2} ⊨ p$ であるから、これと $w_{2} \geq w_{1}$ より $w_{1} ⊭ \neg p$ であることが分かる。よって、 $w_{1}$ では $p$ も $\neg p$ も真ではないので、 $w_{1} ⊭ p \lor \neg p$ であり、 $M$ が反例モデルになることが分かる。

w_{1} - p - \neg p w_{2} + p \leq

(閉じる)

フレームに関する性質

直観主義論理のフレームにもう少し強い制限を加えても、妥当な推論に影響はないことが知られている。このことを形式的に述べるために、まずフレーム上に制限した妥当性を定義する。

定義. フレーム上の妥当性

フレーム上でからへの推論が妥当であることを、上の任意の付値に対して以下が成り立つことと定義する(ただし)。

これをと書く。

命題. フレームの制限

とする。以下の3条件は同値である。

任意のフレームに対して
最小元を持つ任意のフレームに対して
が半順序となる任意のフレームに対して

証明.

$(1) \Rightarrow (2), (1) \Rightarrow (3)$ の向きは自明であり、この逆を示せば十分である。どちらも対偶をとり、反例モデルを適当に変換することで証明できる。概略のみ示す。

まず $not (1)$ を仮定すると、あるモデル $M = ⟨ W, \leq, v ⟩$ と状態 $w_{0} \in W$ が存在して、 $w_{0} ⊨ Γ, w_{0} ⊭ φ$ となる。このとき、新たなモデル $M^{'}$ を次のように構成する。

$not (1) \Rightarrow not (2)$ : 状態の集合を $W^{'} = {w \in W ∣ w_{0} \leq w}$ とし、 $\leq, v$ をこの集合上に制限してモデルを構成すれば、 $w_{0}$ が最小限になる。このとき $W^{'}$ 上の状態では充足関係に変化がないことを論理式の構成に関する帰納法で確認すればよい。
$not (1) \Rightarrow not (3)$ : $x \leq y and x \geq y$ により $W$ 上の同値関係 $\sim$ を定義し、 $W / \sim$ を状態の集合とする。関係と付値は自然に定義できる。あとは $M, w ⊨ φ ⟺ M^{'}, [w] ⊨ φ$ を論理式の構成に関する帰納法で確認すればよい。

(閉じる)

参考文献

Sørensen, M. H., & Urzyczyn, P. (2006). Lectures on the Curry-Howard isomorphism. Elsevier.
大西琢朗. (2021). 『3ステップシリーズ3 論理学』. 昭和堂.

証明の大枠は以下の通り: 相異なる4つの命題変数に対してとする。直観主義論理が適当な3値論理として特徴づけられるならば、どれか2つの命題変数が同じ真理値を持つので(部屋割り論法)、となる。すると後述の選言特性により、あるに対してが成り立つことになるが、これに対しては反例モデルが与えられるので、矛盾する。 ↩
付値を関数として定義し、の代わりにとする流儀もある(実質的には同じ)。 ↩
付値をそのまま拡張して、各論理式にを割り当てるような関数を定義する流儀もある(実質的には同じ)。また、この関係のことを強制関係(forcing relation)と呼ぶ文献もある。 ↩
多くの文献では、選言特性は証明論的妥当性に関する定理として紹介される。健全かつ完全な証明体系であれば結局のところ同値なので些末な点ではあるが、厳密にはここで紹介しているのは「選言特性のモデル論的な書き方」ということになる。 ↩
この手法は 濾過法(filtration) と呼ばれており、様相論理に対しても一般化できる。これに関する記事を前にMathlogで書いたので気になる方はそちらを参照のこと。 ↩

直観主義論理: 可能世界意味論(命題論理)

非形式的な説明

定義

性質

基本的な性質

遺伝性の拡張

選言特性

有限モデル性

推論に関する性質

フレームに関する性質

参考文献

Footnotes