ゲーデルの S4 翻訳から見る直観主義論理のクリプキモデル

今，我々が前提にしているのは，以下の二つの条件のみである．

• S4のクリプキモデルの定義とその完全性

• ゲーデル・マッキンゼイ・タルスキの定理

では以下で，以上の二つの条件から直観主義論理のクリプキモデルを導き出すことを試み てみよう．S4では，次のことが成り立つ．

命題 35.

S4⊢A² ↔2(A²)

この証明は，A の複雑度についての帰納法を用いてすぐに示せる．続いて，この命題と S4のクリプキモデルに対する完全性より

第6章 論理体系を用いた命題概念の分析 142

任意のS4フレームFに対し，F|=A² ↔2(A²).

である．つまり，任意のS4モデルM=⟨W, R, V⟩^とw ∈W について

M, w|=A² ⇔ M, w|=2(A²) ⇔ ∀u ∈W (wRu ならばM, u|=A²) であり，ここでさらにS4フレームにおける到達可能性関係が推移的であることを考慮に 入れると次のようになる．一旦，ある世界w ^{で真となった}A^{2 は，}w^{から到達可能なあ} らゆるuでM, u|=A²であるということであり，このことが表しているのは，S4でA² が単調であるということに他ならない．このとき加えて，S4のクリプキモデルに対する 完全性より，次のことが成り立つ．

命題 36.

S4⊢A² ⇔ ^任意のS4フレームFに対し，F|=A². そして，ゲーデル・マッキンゼイ・タルスキの定理より，

Int⊢A ⇔ S4⊢A² であり，次のことが成り立つ：

Int⊢A ⇔ ^任意のS4フレームF^に対し，F|=A² · · ·⋆ 以上のことを踏まえ，ここで考えなければならないのは：

1. フレーム条件を定める．

2. 直観主義論理モデルとなるN=⟨W, R, U⟩^{の，付値となる}U の条件を定める．

3. 直観主義論理モデルにおける充足条件|=^{を改めて定義する．}

の三点である．1点目については，S4翻訳を参考に考える．直観主義論理からの翻訳と 命題 35^から

Int⊢A⇔ S4⊢2A²

第6章 論理体系を用いた命題概念の分析 143 であり，このとき，任意のS4モデルM = ⟨W, R, V⟩^{において，}V(2A²)はRについ て上方閉（つまり単調）となるので，直観主義論理モデルN = ⟨W, R, U⟩ ^{についても，}

U(A)が上方閉になるようにRとU を与えるのが自然である．

すると，まずRは「上方」という概念が自然に定義できるような性質を持つことが要求 される．つまり，Rが少なくとも弱い意味での順序，所謂，擬順序（推移的で反射的）で あることが要求されるということを表す．そこでさらにU について考えてみる．まず原 子式について定め，次に複合式について議論する．では，原子式についてである．

V は，2 に対して，単調性を実現する．そこで，直観主義論理の付値U に関しても，

そのような単調性が実現されれば良い．S4 の 2 の性質，すなわち，いわゆる 4 公理

（S4⊢2A⊃22A）によって生み出されている性質からして，

任意のv ∈W に対して，wRvかつw∈V(2P)ならばv∈V(2P)

が成り立つ．そこで，このことから，U はP に関して単調でなければならないという条 件が必要になる．つまり，

任意のv ∈W に対して，wRvかつw∈U(P)ならv∈U(P)

と定めるということである．このとき，いつものように，原子式の場合は次のように定め られていると考えて良く，

N, w|=P ⇔ w ∈U(P)

と定義する．このようにして，付値関数U が単調であると決まったが，複合式もS4翻訳 を考慮に入れて見直すと，それらの式の真理集合も単調になっている．つまり，到達可能 性関係に関して，真理が保存される．したがって，直観主義論理の場合も|=を定める上 で，単調性が成立するように配慮しなければならない．

&^と∨については，古典論理と同じ充足条件の定義を用いれば，単調性は帰結する．そ

のため問題は含意の場合である．では，含意の場合について考える．今，現在 ̸|=Aかつ

̸|= B^{（このとき，}|= A⊃B）として，そこから到達可能などこかで，|=A^かつ̸|= B^（こ のとき，̸|=A⊃B）となる場合を考える．このとき，各論理式の単調性だけから，含意式 の単調性を保証することができない．そのため，

N, w|=A⊃B ⇔ N, w|=A ならば N, w|=B

第6章 論理体系を用いた命題概念の分析 144 と定義してしまうと，含意式は単調性を満たさないということである．よって，A⊃Bを 直観主義論理モデルにおいて単調にさせるには，孤立した可能世界についてのみ注目し，

充足条件を定めてはならず，つまり，古典論理的に充足条件を定めてはならず，他の世界 との関係において定めなければならないのである．では，具体的にはどうすれば良いだろ うか．ここでは，S4^{における，}2(A²⊃B²)の充足条件を参考にすることが有効である．

S4では，S4のクリプキモデルの定義より，

M, w |=2(A²⊃B²) ⇔ ∀v∈W(wRvならばM, v|=A²⊃B²)

となっているので，これをこのまま採用してみる．ではその議論を具体的に見てみよう．

実際に S4^{翻訳から，}M, w |= 2(A²⊃B²) を参考にし，その定義を与えることを試み る．今，

M, w|=2(A²⊃B²) は，様相論理の充足条件より，

∀v∈W(wRvならばM, v|=A²⊃B²) と同値であり，さらにまた様相論理の充足条件より，

∀v∈W(wRvならば(M, v|=A²ならばM, v |=B²))

と同値になることはすぐにわかる．そこで，この最後の変形の結果を参考に，直観主義論 理におけるA⊃Bの充足条件を次のように，

N, w|=A⊃B ⇔ ∀v∈W(wRvかつN, v|=AならばN, v |=B) と定めれば良い．

このように定義することで，直観主義論理の含意の論理式も単調性を満たすようにな る．これらのことから，直観主義論理の|=はよく知られた，以下のような定義でよいこ とがわかる．

第6章 論理体系を用いた命題概念の分析 145

N, w|=P ⇔ w∈U(P) (⇔w∈V(2P)) N, w|=⊥ ^{成り立たない}

N, w|=A&B ⇔ N, w|=A かつ N, w |=B N, w|=A∨B ⇔ N, w|=A または N, w|=B

N, w|=A ⊃B ⇔ ∀v∈W(wRv かつ N, v|=A ならばN, v|=B)

直観主義論理の|=は複合式に関しても単調な形で定めるのが自然であり，この定義は，

S4翻訳とも整合的である．