MSHL の概要

そこで以下、 MSHLの概要を説明しておく（詳細はAを参照）。MSHLは基本的に、

単一のクリプキ構造を記述する従来の様相論理を、複数の異なるクリプキ構造を同時に記 述できるように拡張したものである^*7。出発点のアイディアは、言語に用意された命題変 数たちを、いま与えられている複数のクリプキ構造たちのうち、どの構造に適用可能なの かに応じて、種別（sort）化する、というものである。そのために、各命題変数を適用先 のクリプキ構造に応じて種別化するための、ソート（sort）の有限ないし可算無限集合I

= {i, j . . .}^{を用意する。これら}i, j . . .たちは結局、複数並存する各々のクリプキ構造を 表示する名前と考えて差し支えない。このとき、ある命題変数pがクリプキ構造iに適用 可能であるならば、pのソートはiである。例えば、スミスの可能な状態から成るクリプ キ構造を S, ジョーンズの可能な状態から成るクリプキ構造をJ, ^{東京の可能な状態から} 成るクリプキ構造をT として、I = {S, J, T . . .}^{する。すると、}p:=「ポケットに10枚 のコインが入っている」のとき、これはスミスとジョーンズの状態に有意味に適用可能な ので、p^{のソートは}S^でもJ でもある。しかし、これは東京の状態には有意味に適用可能 でないので、pのソートはT ではない。逆に、q:=「雨が降っている」のとき、これは東 京の状態に有意味に適用可能なので、q のソートはT であるが、スミスとジョーンズの状 態に有意味に適用可能ではないので、qのソートはSでもJ でもない。

その上で、これらi, j . . .たちに対して特別な位置に立つクリプキ構造の名前としてu を選ぶ。この u は直観的に、そこからu 自身の内部だけでなく、i, j . . . たちが表すク リプキ構造内部の状態の名前（ノミナル）にも言及できる、その意味でそこから自他の クリプキ構造内部の状態に言及可能な、“俯瞰的”クリプキ構造を表示する。詳細には、

‘u : @_(i:a)(i: φ)’の形で、「構造iの状態a でソートiの論理式φが成立している、とい うことが、構造u で言える」を意味することができる^*8。このときI 中のi, j . . .たちを

「局所ソート（local sort^）」、u^{を「普遍ソート（}universal sort^{）」と呼び、}I^+u = I∪ {u} とする。

このI^+u に対し、矢（arrow）の集合Aを与える。Aの要素r:i →j は、クリプキ構 造i^とj の間の関係（その特殊な場合として関数を含む）を表す。このクリプキ構造間の 関係や関数を表すr : i→ j が、各構造だけでなく、同時に、各構造に種別化された各論 理式をもつなぐ、この論理にとっても、本論文にとっても、概念的に核となる構成要素で

*7この体系がハイブリッド化を伴っていること、つまり、ノミナル‘a’たち（クリプキ構造上の各状態に対 する名前と考えてよい）と、その各ノミナルに応じて充足演算子‘@a〜’^（「状態a^{で〜が成り立つ」を意} 味する）を導入している理由は、それによってこの体系の完全性が容易に得られるためである。ハイブ リッド化なしで完全性が得られるどうか、つまり完全なMSL^（Many Sorted Logic^{）が可能かどうか} は、今後の課題である。

*8従来のハイブリッド論理では、各状態の名前（ノミナル）には、それが属している単一のクリプキ構造内 部でしか言及できない。ただしこれは、従来のハイブリッド論理が単一のクリプキ構造しか記述しないこ とから自動的に生じている制約である。

ある。いま、I^+u とA の対をN = (I^+u, A)とすると、N は直観的に、有限個のクリプ キ構造たちとその間の関係や関数たちが成す（uから俯瞰可能な）ネットワーク構造を表 現する。そこでこのN が表現するクリプキ構造たちのネットワーク構造のことを、「クリ プキネットワーク Kripke network」と呼ぶ。また、これに基づいて論理式の真偽を評価 するモデルのことを、「クリプキネットワークモデル Kripke network model」と呼ぶ。

さて、以上のクリプキネットワークN = (I^+u, A)が与えられたとき、N を構成する各 クリプキ構造i, j . . .たちとuに対し、iに適用可能な論理式の集合Form(i)、j に適用可 能な論理式の集合Form(j)、...，uに適用可能な論理式の集合Form(u)を定義する。その ためにまず、次の語彙（vocabulary）を準備する。

• ^各k ∈ I^+u に対して、可算個の命題変数の集合Prop(k) = {p, q, r, ...}^{。ただし、}

相異なるk, l ∈ I^+u について、Prop(k)∩Prop(l)は非空であることを許容する。˙ つまり、一般に相異なるk, l∈I^+uについて、共通の命題変項pを共有していても よい。

• ^各 k ∈ I^+u に 対 し て 、可 算 個 の ノ ミ ナ ル（ 状 態 の 名 前 ）の 集 合 Nom(k) = {a, b, c, ...}^{。ただし、相異なる} k, l ∈ I^+u について、Prop(k) ∩Prop(l) は_空で˙ なければならない。つまり、相異なるk, l∈I^+uについて、共通のノミナルaを共 有することはない。

• ^{ブール結合子}∧^および¬^。

• ^各r :k→l ∈Aに対して、様相演算子⟨r⟩^と⟨r⁻⟩^。

• ^各k ∈I^+u に対して、様相演算子の集合Mod(k) ={31,32,33, ...}^{。ただし、こ} れらの様相演算子はすべて、一個の命題のみと組み合わせられる単項様相演算子と する。

• ^{充足演算子}@^。

以上の語彙を用いて、各k ∈ I^+u に対し、ソートkの論理式の集合Form(k)を、以下 のように同時再帰的に定義する。

(i) どの命題変項p∈Prop(k)も、ソートk の論理式である。

(ii) どのノミナルa∈Nom(k)も、ソートkの論理式である。

(iii) φとψがソートkの論理式ならば、¬φとφ∧ψもまたソートkの論理式である。

(iv) φがソートkの論理式で、3^がソートkの様相演算子（つまり3∈Mod(k)）なら ば、3φもまたソートkの論理式である。

(v) r :k →l ∈Aで、φがソートlの論理式ならば、⟨r⟩φはソートk の論理式である。

(vi) s : l → k ∈ A で、φがソートl の論理式ならば、⟨s⁻⟩φはソートk の論理式で ある。

(vii) φ が局所ソート i ∈ I の論理式で、a が局所ソート i ∈ I のノミナル（つまり

a ∈Nom(i)）ならば、@aφもまた局所ソートiの論理式である。

(viii) φ がソート k ∈ I^+u の論理式で、a がソート k ∈ I^+u のノミナル（つまり a ∈Nom(k)）ならば、@_aφはソートuの論理式である。これは言い換えれば、ど んな局所ソートのどんな@冠頭式も、同時に、普遍ソートuの論理式としてもま た組み入れる、ということである。

このうち、最も重要な同時再帰のステップは(v)^及び(vi)^である。(v)^は、構造k ^から l への関係

r:k →l

について、それに対応する様相演算子⟨r⟩^{が、ソート}lの論理式をソートkの論理式に変 換する関数

⟨r⟩:Form(l)→Form(k)

と見なすことができることを示している。このとき、r :k →lの向きと⟨r⟩:Form(l)→ Form(k)の向きが反変していることは、

⟨r⟩φ

の直観的意味、つまり、

「今置かれている構造k内部の状態とr関係にある、構造l 内部の状態があって、そこで φ^{が成り立つ」}

を考えれば判る。というのも、φ^{自体が表すのは構造}l内部の状況であるが、この構造l 内部の状況が、構造k 内部の状態から見て、関係rの先に生じている、ということが、こ の⟨r⟩φの語っていることだからである。よって⟨r⟩φそのものは、構造k 内部における、

その外部との_関˙ _係˙ 的状況を記述しているからである。その意味で、関係˙ r :k →l に対す る様相演算子⟨r⟩:Form(l)→ Form(k)とは、構造l の状況を表す論理式を、構造kから 構造lへの関係rにより、構造k内部の状態に視点化された状況を表す論理式へと変換す る機能をもつことが理解されるだろう。

同様に、(vi)は、構造lからkへの関係

s :l→k の逆関係

s⁻ :k →l

について、それに対応する様相演算子⟨s⁻⟩^{が、ソート}l の論理式をソートk の論理式に 変換する関数

⟨s⁻⟩:Form(l)→Form(k)

と見なすことができることを示している。このときも、s⁻ : k → l の向きと ⟨s⁻⟩ : Form(l)→Form(k)の向きが反変していることは、

⟨s⁻⟩φ

の直観的意味、つまり、

「今置かれている構造k内部の状態とs⁻関係にある、構造l内部の状態があって、そこ でφが成り立つ」

を考えれば判る。というのも、この場合もφ自体が表すのは構造l 内部の状況であるが、

この構造l内部の状況は、構造k 内部の状態から見て、今度はそこから関係sを遡った先 に生じている、ということが、この⟨s⁻⟩φの語っていることだからである。よって⟨s⁻⟩φ そのものは、構造 k 内部における、その外部との_関˙ _係˙ 的状況を記述しており、その意味˙ で、関係s:l →kの逆関係s⁻ :k →lに対する様相演算子⟨r⟩:Form(l)→Form(k)は、

構造lの状況を表す論理式を、構造l から構造kへの関係sの逆関係s⁻ : k →lにより、

構造k 内部の状態に視点化された状況を表す論理式へと変換する機能をもつことが理解 できる。

このように、各構造間の関係r やその逆関係r⁻ を様相演算子⟨r⟩^や⟨r⁻⟩^{によって言} 語内に明示するだけで、各構造に適用される論理式が表す情報の視点を変換できる、とい うことが、このMSHLの本質的な部分である。このことが理解されれば、「情報の視点の 変換」という構造間様相演算子の機能によって、各言語が有機的なネットワークをなす、

このシステムの概要が見て取れるだろう。

さて、上の⟨r⟩φや⟨s⁻⟩φは、これらの式全体とその構成要素がもつソートの情報をす べて詳細に明示化すれば、k : ⟨r : k →l⟩(l : φ)やk : ⟨s⁻ : k →l⟩(l :φ)となる。同様

に、(viii)における普遍ソートu の論理式@aφの式全体とその構成要素がもつソートの

情報をすべて明示化すれば、u: @_(i:a)(i :φ)となる。明示化された各ソートが、全体とし

て、意図された適合性を保っていることを確認されたい。

以上のシンタクスに対して、MSHLの公理化が行われる。この中で本論文にとって重 要なのが、関係r :k →lとその逆関係r⁻ :l →kに関する次の公理図式である。

⊢l φ→[r⁻]⟨r⟩φ · · ·(−+) この公理図式の直観的意味は、

「今置かれている構造l内部の状態でφならば、そのとき、もし今の状態からr関係で遡 ることのできる構造k内部の状態があれば、そこから見ると、関係rの先にφが成り立

つ、ということになる」

となる^*9。

最後に、MSHLは、クリプキネットワークのクラスに対して完全である。これは大ま かには、次のことを意味する。いま、任意の無矛盾なソートkの式集合∆_k（この∆_kに は、r :k →l のような構造間の関係を介して、⟨r⟩φといった式が構造l についての情報 φを含むように、構造kに視点化された構造k以外の構造たちの情報も含まれうる）が与 えられたとしよう。MSHLが完全であるとは、われわれはこのとき、∆_k に属するすべて の論理式を同時に成立させる、あるクリプキネットワーク内に位置付けられた、クリプキ 構造 k の状態を——これを取り巻く当のクリプキネットワークの全体とともに——構成 できる、ということである。

以下で行うクリプキネットワークによるゲティア反例の構成は、ゲティア反例がMSHL の無矛盾な論理式によって記述できることとと、この MSHL の完全性によって保証さ れる。

*9この公理は古典的時制論理の公理図式

⊢φ→HF φ

と完全に類比的である。なぜなら、Hは過去必然性「どんな過去の時点でも〜」、F^{は未来可能性「ある} 未来の時点で〜」を意味し、ここで過去関係は未来関係の逆関係と考えられているからである。この場 合、上の公理図式の直観的意味は、

「今φならば、これ以前のどんな過去の時点に遡ったとしても、その時点から見たとき、未来のある時点でφ^が 成り立つ、ということになる」

となる。