様 相 と 証 明 可 能 性
(I)
田 畑 博 敏 (平成 3年6月30日受理)§
1
概
観1,1
様相 論理 通 常の古典論理 に,「 必然1生」 や「 可能′性」,
あ るいは それ らに関連 す る「 合意」 といった概 念 を 表す語彙 を付 加 した体系 (古典論理 の拡張体系)の
論理 的研 究 が,様
相 論理 で あ る。様 相論理 で は, 「,中は必然 で ある」「 必然的 に… で ある」とい う言葉 使 いは,文
演 算子 とみ な され,記 号 “□"で
表 す。 また,「・…は可能であるJと
い う言葉使 いも,
“◇"と
い う文演算子で表す。 こ うして,
“A"を
任 意の文 とす るとき,
“□A"は
「Aは
必然である」 と読 み,
“◇A"は
「Aは
可能である」 と読 む。 □ と◇ とは相互 に定義で きる。すなわち,□
を原始記号 とす るとき,
“◇A"は
“司□司A"と
定義 で き,逆
に◇ を原始記号 とす るとき,“□A"は
“司◇￢A"と
定義で きる。 さて,本
論では,様
相論理の口 を “…は証明可能である"と
読 み,◇
を “…は無矛盾である"と
読 む解釈 を取 るときの様相命題論理の体系 を考察す る。 このよ うな体系は,
クル ト・ゲーデルにち なんでGと
呼ばれるが, ゲーデルの有名な定理 (と くに形式的算術体系の無矛盾性 に関す る定理) に関連す る興味深 い結果 を導 くことになる。1)Gに
おいても,大
部分の様相命題論理 が文 とみなす 表現 を文 とす るが,定
理 についてはGは
ある特徴 を持っている。Gの
公理 は,す
べての トー トロジー と,□
(A→ B)→
(□A→
□B)と
い う形式のすべての文であ り,
さらに, □(□A→
A)→
□A
とい う形 の文が公理 に加 わる。Gの
推論規則 はモ ドゥス・ポ ネンスと必然化である。Gに
おいては, 例 えば “□p→p"は
定理ではない,と い う一見奇妙 なことが起 こる。 これは,Gが
必然性 とい うよ りむ しろ証明可能′性の概念の研究のために考案 された体系 であることに起囚す る。 様相論理の研究 は,
ソール・ クリプキが「可能世界意味論」 とい う新 しい形 の意味論 を導入 して 以来,大
幅 に進歩 した。2)ク
リプキは,可
能世界 と呼ばれる要素 からなる集合 (領域)Wと
,Wの
要 素 間 に成 り立つ二 項 関係 (接近 可能性 の関係 と呼 ば れ る
)Rと
,領
域 の メ ンバ ー と文変項 か ら成 る各対 に真理値 を付与 す る関数Pと
の三者 か ら構 成 された順序 三組 〈W,R,P〉
を,様
相 文 の解釈 のモ デ ル とす る。 ここでは,文
は各世 界 ごとに真理値 が決 ま る。 す なわ ち,要
素 文(=文
変項)は
各世 界で関数Pに
よ り直接 に真理値 が与 え られ,真
理 関数的複 合 文の真理値 は通常 の仕方で その世 界で の各要素文の真理値 か ら計算 され る。□Aと
い う形 の文 が あ る世 界 αで真 で あるのは,
その世 界 か ら接近可能 な (つま り,
αと関係Rを
満 たす)す
べ ての可能世 界で文Aが
真 で あ ると き,
かつ その と きにか ぎる。 こ うして,演
算子 □ は,二
項 関係 を備 えた非空 の集合上 で定義 された一種 の量 化子 とみ な され る。 また,文
は あ るモ デルのすべ ての可能世 界で真 で あると き,
そのモ デ ルで妥 当 で あると言 われ る。 ク リプキは,様
相 論理 に関す る以下 の形 の 多数 の健 全性 および完全性 定理 を証 明 した。す なわ ち,様
相 論理 の よ く知 られた体系 の定理 で ある文 は,
あ る性 質 を持 つ (接近 可能性 とい う)二
項 関係 の定 め られたすべ てのモ デ ルで妥 当 な文 と一致 す る。 ところで,様
相 命題論理 の体系 は,
その定理 の集合 がすべ ての トー トロジー と □(A→
B)→
(□A→
□B)と
い う形 のすべ ての文 を含み,モ
ドゥス ・ポ ネ ンス と必然化 と代入 につ いて閉 じて い るな らば,正
規 的(nOrmal)と
呼 ば れ る。 よ く研 究 され て い る様相 命題 論理 の体系T, S4,B,
S5と
ともに,体
系Gも
正規 的体系 で あ る。体系Gに
も ク リプ キ流 の健 全性 定理 ・完 全性 定理 が成 り立 つ。す なわ ち, 関係Rは
, ………W3Rw2&W2Rwl&wi Rw。
で あ るよ うな, いかな る無限夢」:WO,Wl,ヽ
ハ/2,W3, ・……・ も存 在 しない と き,
よ く基礎 づ け られてい る(well―founded)と
呼 ば れ るが,Gの
定理 は,接 近可能 性 関係 の逆 関係 がよ く基礎 づ け られてお りかつ推移的で あ るよ うなすべ てのモ デ ルで妥 当な文 と一 致 す る。 以下 では この よ うなGの
構 文論 的 かつ意味 論的性 質 を研究 す るが,□
を「証 明可能性」 と解す る と き,
それは正確 には「算術 での証 明可能性」 で ある。 そこで次 に,算
術 につ いて概 観 す る。1 2
ペ ア ノ算術ここで考察 の対象 とな る算術 は
,ペ
ア ノ算術 (Peano arithmetic I以下,PAま
た は単 に「算術」 と記す ことがあ る)と
して知 られ る,数
学的帰納 法 の公理 と,後
者,加
法,乗
法 を支配す る公理 を 持 つ古 典 第一 階 の形 式的算術 で あ る。 これは,ゲ
ーデ ルの不完 全性 定理 が標準 的 な仕 方 で証 明 されるとい う観 点 か ら見 た ときに
,
もっ とも普通 に問題 に され る形 式的理論で あ る。さて
,ゲ
ー デルはペ ア ノ算術(PA)の
各 言語表現,す
なわ ち,記
号,(論
理 式 の よ うな)記
号 の 有限列,(証
明の よ うな)記
号 の有 限列 の有限列 の各 々 に自然 数 を一対― に機械 的 に割 り当て る方様相 と証明可能性(I) 法 (これ をゲーデ ル数づ け とい う
)を
考案 した。 その よ うな割 り当て に よって各 表現 に割 り当 て ら れた 自然 数は,
その表現 の「 ゲー デ ル数」 と呼 ばれ る。ペ アノ算術 にIDhいて は,数
(以 後,0を
含 む 自然 数 の こ とを数 と呼ぶ)nを
表 す数詞 は,ゼ
ロ記号0に
n個
の後 者記号′を付 加 した表現 で ある。 (例 えば,数
5に
対 す る数詞 は0″′アで あ り,数
ゼ ロの数詞 は0で
あ る。) そ こで,PAの
表現Fの
ゲーデ ル数 に対す る数詞 を表 す記法 を導入 す る。 この数詞 を, 匡F￢ で表示 す る。 また,「Fは
PAの
定理 で あ る」 とい うことを意味 す るの に, 卜PA F と書 く。1 2.1
算術 におけ る証 明可能′陛 ゲー デ ル数づ けの技法 によって,式
Bew(x)(beweisbarつ
ま り “証 明可能 な"に
由来 し,「
ゲ ーデ ル数xの
式 はPAで
証 明可能 で あ る」 を意味 す る)を
PAの
中で構 成 で きる。 そ して この式 は 以下 の三つの条件 を満 たす。PAの
すべ ての文S,Qに
対 して,(I)も し 卜PA Sな ら Iゴ, 卜PA BeW(「 S￢)
(Ⅱ)卜PA BeW(「
(S→
Q)￢ )→(Bew(匡
S￢ )→Bew(「
Q￢ ))(Ⅱ
)卜
PA BeW(「 S￢ )→Bew(匡 Bew(「
S￢)￢ )以後
,Bew(「
S￢)に
,「Sが
証 明可 能 で あ る」 と主張 して い る文(Sの
証 明可能性 を表現 した文) と して言及す る。 さて,上
の(I)の
条 件 によれば,
も し文Sが
PAで
証 明可 能 で あれば, Sの
証 明可能性 を表現 した文 もまたPAで
証 明可 能 で あ る。 また,
この条件 は様相 論理 におけ る必然化規 則,す
なわ ち,
卜A⇒
トロAに
似 て い る。 条件 (Ⅱ)に
よれば,
も し条件法 とその先 件 が証 明 で き るな らば,そ の後件 も証 明で きる。 これは様相 論理 での□ の配分原理 :□(A→
B)→
(□A→
□B)
に以 てい る。 さらに条件 (Ш)に
よれば,(I)の
内容,つ
ま り「Sが
証 明可 能 な らば,Sの
証 明可 能性 を表理 した文 も証 明可能」 とい うことを表理 す る文 がPAで
証 明可能 で あ る。 これ は様 相 論理 での,□
A→
□□Aと
い う原理 に似 てい る。 ゲーデ ルは その論文 において,
きわめ て巧 妙 なや り方で,「
Sは
証 明 で きない」 とい うこ とを主 張 す る文Sと
(彼 が考察 した算術 体系Pで )同
値 にな る文 を構 成 した。0
その構 成 は相 当 に一般 的 なテ クニ ックを用 いた もので あって, PAに
おいて も同様 に実行 で きる。 それ によって, PAの
任 意 の一項述 語P(x)に
対 して, 卜PA S PP(「
S￢) となるよ うな文Sが
存 在 す る とい うこ と (対 角 化補 題 と呼 ば れ る)を
示 す こ とがで きる。Sど
P(匡
S￢)が
(理 論Tで)証
明可能 で あ るよ うな文Sは
,述
語P(x)の
(Tに
おけ る)不
動点(fixed point)と 呼 ば れ る。 こ うして
,ゲ
ーデ ルは述 語 司Bew(x)(の Pで
の対応物)の
(Pに
おけ る)不
動 点―一 ￢Bew(x)の
不動 点 は特 に “ゲー デ ル文"と 呼 ば れ る一― をい か に構 成 す るか を示 した。 あ る理 論 の言語 で作 られた文 (三自由変 項 を含 まない論理 式)は
,
その理 論 で証 明 も反証 (否 定 形 の証 明)も
され ない とき,
その理 論 の決 定 不能 文 と呼 ば れ るか,
または その理 論 では決定 で きな い と言 われ る。理論 は,
その中 に決 定不能文 が存 在す るとき,(構
文論的 に)不
完 全 で あ る と言 わ れ る。1.2 2
ゲー デ ルの定理 さて,ゲ
ーデ ルによれば以下 の ことを示 す ことがで きる。(1)も
しPAが
無 矛盾 で あれば,￢
Bew(x)の
い かなる不動点 も証 明可能 では ない。(2)も
しPAが
“ω無矛盾"と
い う無矛盾性 よ り強 い性 質 を持 てば,￢
Bew(x)の
い かな る不 動 点 も反証 され ない (不 動点の否定形 が証 明で きない)。 ところで,￢
Bew(x)の
不動点 は れ っ きと して存 在 す るか ら,(3)も
しPAが
ω無 矛盾 な らば, PAは
不完 全 で ある (ゲ ーデルの第一 不完 全性 定理)。 ゲーデ ルの第一 不完 全性 定理 は1936年
にロ ッサ ー によって よ り強 い形 に改良 された。 す なわ ち, “ω無矛盾"と い うこの定理 の もつ前提 をよ り弱 い “無矛盾"に
置 き換 えて,定
理 自体 を強 くす るこ とがで きるこ とが示 された。 さらに,つ
ぎの こ と を示 す ことがで きる。(4)そ
の先件 がPAの
無矛盾性 を表現す るPAの
文 で あ り,
それの後件 が ￢Bew(x)の
不動 点 で あるよ うなすべ ての条件法 は証 明可能 で ある。従 って
,こ
れ と(1)に
よって,(5)も
しPAが
無 矛盾 で あれば, PAの
無矛盾性 を表現す る文 はPAで
は証 明で きない (ゲ ーデ ルの第二 不完 全性 定理) を示 す こ とがで きる。(5)の
逆 は明 らかで あ る。 とい うの は,矛
盾 した理 論 において は その言語 に 属 す る文 のすべ て が その理論 で証 明で きるか ら,対
偶 によ り,
その理 論 で証 明で きない少 な くとも 一 つ の文 がその理 論 に存在すれば その理論 は無矛盾 で あ るか ら,で
ある。 ところで,「PAの
無矛盾性 を表現 した文」とは ど うい う文 か,そ
の こ とをここでは っ きりさせて お く。 「矛盾 した理論」 の定義 と して,以
下 の同等 な四つの定義 がある。 す なわ ち,① その言語に属するすべての文がその理論で証明可能ならば, その理論は矛盾 している
;② ある文とその否定形がともにその理論で証明可能ならば, その理論は矛盾 している
;③ その否定が明 らかに定理であるような, ある特定の文がその理論で証明可能ならば, その理論
は矛盾 している
;④少なくとも一つの矛盾がその理論で証明可能ならば
,
その理論は矛盾している。
様相 と証 明可能性(I) 以上 の定義 と同様 よ く用 い られ
,以
後 われ われ が主 と して考察 す るこ とにな る定義 は, (※)上
が その理論 で証 明 され るな らば,
その理 論 は矛盾 してい る, とい うもので あ る。 ここで,
“上"は
常 に偽 の真理値 を与 え られ るゼ ロ項 命題 結合 子 で あ る。 また これ とは対照的 に,
“T"は
常 に真 の真理値 を与 え られ るゼ ロ項 命題 結合子 で あ る。 上 と条件 法 に よってpの
否 定 :￢pは
, p→
上 と定義 で きる。 われわれは, 上 を原始記号 と して持 つ よ うなPA
の ヴ ァー ジ ョンにつ いて考察 して い るもの とす る。 す ると, PAの
無 矛盾性 を表現す るPAの
文 と しては, ￢Bew(匡
上￢) とい う文 を採 ることにな る。 そこで,(5)は
こ う言 い換 えることがで きる:/PA上 な ら ば , /PA￢ BeW(匡 上￢)。
1 2 3
ヘ ンキ ンの問題 とレー ブの定理 ここで,
これ まで暗黙 に前提 していたPAの
意味論 (モ デ ル論)を
明確 に しよ う。PAの
標 準 モ デ ルは,
まず その領 域 と してゼ ロ を含 むすべ ての 自然数 を持 つ。数詞0は
この標準 モデ ルで数 ゼ ロ を指示 し,以
下 同様 にn個
のアを伴 う0,
または数詞nは
数nを
指示 す る。 また,
ア,十 ,
・ は そ れ ぞれ 自然数上 の後 者,加
法,乗
法 を指示 す る。式Bew(x)が
数nに
つ いて標準 モデ ルで真 とな る (あては まる)の
は,数
nが
PAで
の証 明可能 な式 のゲーデ ル数 で あると き, かつ その ときにか ぎる。 こ うして, Sを
PAの
文 とす ると き,Bew(匡
S￢)が
(標 準 モ デ ルで)真
となるのは, Sが
(PAで
)証
明可能 な文 で あ る と き,か
つ その と きにか ぎる。 とい うのは,Bew(匡
S￢)が
真 で あ るのは,数
詞匡S￢ によって指示 され る文Sの
ゲー デル数 につ いて, Bew(x)が
あては まる と き, かつ その と きにか ぎるか らで ある。 また, PAの
すべ ての定理 は標準 モ デ ルで真 で あ る。従 って,PAは
無矛盾 で ある (文Sと
その否 定形 が標準 モデ ルで ともに真 にな ることは ありえない)。 す る と, 文 ￢Bew(『
上￢)は
真 で あ り, 1 2 2の
(4)に
よって,￢
Bew(x)の
不動点 (卜PA S P￢BeW
(匠S￢)で
あ るよ うな文S)は
￢Bew(「
上￢)か
ら導 出 され るか ら,
この よ うな不動点 もすべ て 真で あ る。 ところで,ヘ
ンキ ン(L Henkin)は
Bew(x)の
不動 点,す
なわ ち, 卜PA S PBeW(「
S￢) となるよ うな文Sに
つ いての問題 を提 出 した。。 この よ うな文Sは
,「Sは
証 明可能 で あ る」 とい う 主張 と同値 で ある。 いわば,
それ 自身 の正 当性 を自己言及 とい う形 で主張 してい る文 (この よ うな 文 はヘ ンキ ンに ちなんで “ヘ ンキ ン文"と
呼 ばれ る)で
あ る。 この文Sは
すべ て証 明可能 (従 って 真)な
の か,
それ ともすべ て証 明 不可能 (従 って偽)な
の か?そ れ とも,
あ るもの は証 明可能 で あ り, あ る ものは そ うでは ないの か?こ
のヘ ンキ ンの問題 に対す る答 は,
レー ブ (Lёb)に
よって与 え られた。9
レー ブは,すべ ての文
Sに
対 して, 卜PA BeW(『 S￢ )→ S な らIゴ, 卜PA S で あることを示 した(レー ブの定理)。 こ うして,そ れ 自身 の証 明可能性 の主張 と同値 なすべ ての文 は証 明可能 で ある。 さて,
この レー ブの定理 とゲーデ ルの第二 不完全性 定理 とは密接 な関連 を持 つ ことが知 られて い る。す なわ ち,
まず レー ブの定理 は,単
一 文 によるPAの
拡 張 に対 す るゲーデ ルの第二 不完全性 定 理 か らの直接 の帰 結 で あ る。￢Sを
公理 と して付加 す るこ とによ りPAを
拡 張 した結果 を PA子 と しよ うI PA+=PA十
(￢S)。 PA十 が無矛盾 で あるのはSが
PAで
証 明 で きない と き,か
つ その と きにか ぎる (実 際,
も し 卜PA Sな ら トギSだ
か らPA+は
矛盾 す る し,逆
に PA十 が矛盾 して お れば 卜融￢S→
S,
ゅ ぇに 卜PA S
とな る)。 従 って,PA十
の無矛盾性 を表現す る文 は, PAに
お いて も, ゆ えにPA+1こ
19・いて も, ￢Bew(匡
S￢)と
同値 で あ る。こ うして , 卜PA BeW(「 S￢ )→S
⇔ 卜PA￢S→
￢Bew(『
S￢) ⇔ 卜PA+￢BeW(匡
S￢) ⇔PA十
の無矛盾性 を表現 した文 が PA十 で証 明可能 で あ る , で あるか ら,
ゲー デ ルの第二 不完 全性 定理 (PA十 が無矛盾 な らば, PA十 の無 矛盾性 を表現 した文 はPA+で
は証 明で きない)に
よって, ⇔PA十
が矛盾 ⇔ 卜PA S, となる。 す なわ ち,
も し 卜PA BeW(匡 S￢ )→S
な らば,
ゲ ー デ ルの第二 不完 全′性定理 によ り, 卜PA S
で あ る。 逆 に, PAに
対 す る第二 不完 全性 定理 は,
レー ブの定理 か ら直 ちに帰 結 す る。 実際,
こ うなる。 い まPAが
無矛盾,つ
ま り/PA上
とす ると, レー ブの定理 によ り, /PA BeW(匡
上￢)→上 で あ る 。 ゆ え に, /PA￢ BeW(F上
￢)。(な
ぜ な ら, も し 卜PA￢BeW(「
上 ￢)な
ら ば,
卜PA￢BeW
(匡上 ￢)→
(Bew(匠
上￢)→ 上)(ト
ー トロ ジ ー)だか ら,卜 PA BeW(「上 ￢)→上 と な る か ら で あ る 。)ここで
,￢
Bew(「
上￢)は
PAの
無矛盾性 を表現 したPAの
文 だ か ら, PAが
無 矛盾 な らば, PA
の無矛盾性 を表現 した文はPAで
は証 明で きない,
とい うこ とになる。1 3
様相 論理 と算術1.3.1
翻】訳 によ る対応 づ け さて,
これか ら様 相論理 とPAと
の関連 を考 える。 せ る翻訳 を定義す ることで それ を具体 化す る。 まず, その際,様
相 論理 の各式 にPAの
式 を対応 さ その翻 訳 の基礎 と して,様
相 論理 の各 文変 項様相 と証 明可能性(1)
pど に算術 の式
Qを
割 り当て る関数 φ (す なわ ち φ(pど)=Q)を
定義 し,こ
の関数 φを実現 (realiza‐tion)と 呼ぶ。 この実現 とい う関数 によって
,様
相 論理 の文Aの
実現 φの下 での翻訳 (translation)A″ をつ ぎの よ うに帰納 的 に定義 す る。
Aが
文変項の とき, A″
=φ (A)
A=上
ならば, Aφ
=上
φ=上
A=￢
(B)な
らば, Aφ
=司
(Bφ)A=(B&C)な
らIゴ, Aφ
=(Bφ &C″)A=(BVC)な
らば, Aφ
=(Bφ VCφ)A=(B→
C)な
らば, A″
=(Bφ →Cφ)A=□ Bな
らば, Aφ
=Bew(匡
Bφ￢)(`◇'は `￢□￢
'の
略式の記法 とみ な し,最
外側の括弧 は誤解のないか ぎり省略す る。)こうして
,例
えば,
φ(p)=0′
+0′ =0′′ とす ると,((□p→
p)&p)φ
=(Bew(匡
0ア+0′=0″
￢)→0′+0′=0″
)&0′ +0′ =0′′
である。 また
,
φが何であれ常 に,(司□ 上 → ￢ □ ￢ □ 上)φ =司 Bew(匡 止￢)→￢Bew(「 ￢Bew(匡 上￢)￢ )
で あ り
,
これはPAに
対 す る第二 不完 全性 定理 を表 現 す るPAの
文 で あ る。 さ らに,Aが
様 相 論理 の文でSが
PAの
文 で あ り, Aφ
=Sな
らば,(□(□
A→ A)→
□A)φ=Bew(匡
(Bew(「
S￢)→ S)￢)→Bew(FS司
)で あ り
,
これは,
も しBew(匡
S￢)→Sが
証 明可能 な らばSも
証 明可能 で あ る,と い うこと (レーブの定理
)を
主張 す る算術 の文で あ る。 こ うして,□
(□A→ A)→
□Aの
形 のGの
各 公理 のすべ て の翻訳 は レー ブの定理 の ある事例 が成 り立つ とい うことを主張 す る。 そ ういった翻 訳 の各 々は,後
に見 るよ うに
,
それ 自身証 明可能で あ る。 実際,Gの
各定理 の翻 訳 はすべ て算術 の定理 とな る。 さて,
その定理 の翻 訳 がすべ て算術 の定理 とな るよ うないかなる様相 論理 の体系 も,□
p→pを 定 理 とす ることは ない。 とい うのは, Sが
￢Bew(x)の
不動点,す
なわ ち 卜PA S P￢Bew(匡
S￢ )で あ り
,
φ(p)=Sと
す る と,PAの
無 矛盾性 によって,/PA BeW(匠
S￢)→Sで
あ るか らである。(も し, 卜PA BeW(「 S￢)→ S な ら ば, 卜PA BeW(匡 S￢)→￢Bew(Fs￢ ), ゅ え に 卜PA￢ BeW
(匡S￢
),ゆ
えに 卜PA Sと
な り,
￢Bew(x)の
不動点Sが
PAの
定理 となるが,
これは先の 1.2 2の
(1)に
反す るからである。)こ
うして,
もし φ(p)が
￢Bew(x)の
不動点であれば,
φの下での(□p→
p)の
翻訳はPAの
定理 ではない。(こ
の ことはまた,つ
ぎの理 由か らも分 かる。φ(p)=上 , 卜PA(□ p→ p)φ な ら ば,そ の と き,「 PA BeW(F上 ￢)→ 上,ゆ え に 卜PA￢ BeW(匡 上￢)。 しか し
,第
二 不完 全性 定理 によ り,
これはPAが
矛盾 で あることを導 く。)1.3.2
実証文 様相論理Gを
研究す ることによ り,算
術(PA)の
証明可能性や無矛盾性 に関す る興味深 い事実 を知 ることがで きる。 例 えば,「
算術 は無矛盾 である」 とい うことを表現す るPAの
文は ￢Bew
(「上￢)で
ある力ヽ これは ￢□上 の翻訳で ある。 また,「
算術 が無矛盾 ならば,算
術 の無矛盾性 を 表現 した算術 の文は算術では証明で きない」 (第二不完全性定理)を
表現す る算術 の文は ￢Bew
(げ止￢)→￢Bew(匡 ￢Bew(匡 上￢)￢)で あ る が, こ れ は ￢ □ 上 → ￢ □ ￢ □ 上 の 翻 訳 で あ る 。 ￢ □ 上の よ うないかな る文変項 も含 まない様相 論理 の式 の算術へ の翻訳 を実証 文 (deictic sentences) と呼ぶ。 実証 文 は実現 φの いかん に拘 わ らず,文
変項 を含 まない様相 文 に一意 に対応 し, Bew
(匡上￢)と,上 , Tを
含 む真 理 関数 か ら構 成 され る算術 の文 (従 って 自由変項 を含 まない)で
あ る。 実証 文は算術 の証 明可能性 と無矛盾性 につ いて あ る事 を主張 してい るか ら,実
証 文 に対応 しかつG
に属 す る文 (なぜGに
属 さねば な らないかは直 ぐ後 に述 べ る)の
証 明可能性 と真偽 を調 べ る こ とに よって,算
術 の証 明可能性 と無矛盾性 に関す る主張 の証 明可能性 と真偽 を知 ることがで きる。 ゲー デルは,
卜PA S P司Bew(匡
S￢)で
あ るよ うな文S,つ
ま り,そ
れ 自身 の証 明不可能性 の主 張 と同値 な文,
い わゆ るゲーデル文の構 成 の仕 方 を示 したが,
われ われは ゲー デ ル文以外 に,
それ 自身 の証 明可能性 の主張 と同値 な文,
い わゆ るヘ ンキ ン文,
また,
それ 自身 の反証 可能性 の主張 と 同値 な文,
それ 自身 の反証 不可能′性の主張 と同値 な文,等
々の クラスにつ いて研究 す るこ とになろ う。 さらに,ゲ
ーデ ルは,ゲ
ーデ ル文 が実証 文 で ある無矛盾性 の主張 と同値 にな ること,すなわ ち,卜PA S P司
Bew(匡
S￢)な
るSに
つ いて 卜PA S P司Bew(匡
上￢)で
あ る こ とを示 した。 また レー ブは,す
べ てのヘ ンキ ン支,つ
ま リ トPA S PBeW(匠
S￢)な
るS力ヽ これ も実証 文で あ るT(=￢
上)と
同値 で ある,つ
ま リ トPA S「Tで
あ るこ とを示 した。 ゲーデル文やヘ ンキ ン文等 は,様
相 命 題 論理 の記法 と実現 の概 念 によって定義 され るある自然 な クラスに分類 され る。 そ して,
その よ う な クラス に対 しては, その クラスの全 メ ンバ ー が それ と同値 になるよ うな実証 文 が存 在 す ることが わか ってい る (ベ ルナルデ イとスモ リュ ンスキーの定理0)。 こ うして,ゲ
ー デル とレー プが確 立 した証 明可能性 と無矛盾性 に関す る事 実は,Gに
関 す る さま ざまの定理 ・ メ タ定理 を証 明す ること によって,成
り立つ こ との証 明 が得 られ る。 では なぜ,体
系Gで
なければ な らないか?こ
れ に対す る答 は ソロヴェイの完全性 定理 が与 える。1.3.3
ソロヴェイの二 つの完 全性 定理R.ソ
ロ ヴェ イは,様
相 論理Gの
諸定理 は,
それのすべ ての翻訳 が算術 の定理 とな るよ うな,
そ うい う様相 文の クラスに外 な らない ことを示 した。つ この定理 をGに
関 す るソロ ヴェ イの第一完 全 性 定理 と呼ぶ。注 意 すべ きことは,
ここでの「完 全性」 はモ デルの それでは な く,実
現 の完 全性 の こ とを述べ てい るとい う点で ある。□ を「・・・は証 明可能 で あ る」 と読 む ことによって,様
相 論理 の 文 は証 明可能′性 につ いての諸原理 を表現 してい るとみ なす ことがで きる。す ると,
ソロ ヴェ イの第様相 と証 明可能性(I) 一完 全性 定理 は
,様
相 論理 の どの文 が証 明可能性 につ いての証 明可能 な原理 で あるのか,
との 問 い に決着 をつ け る。 では,様
相論理 の どの文が証明可能性 についての真 なる原理であるのか?こ
れについても,
ソロ ヴェイの もう一つの完全性定理 が答 える。標準モデルにおいて,算
術 の定理 はすべて真 である。従 って,す
べての文Sに
ついて, Bew(匡
S￢)→Sは
真である。(レーブの定理 によ り,Bew(「
S￢) →S
が証明可能であるのはSが
証明可能であるとき, かつ その ときにか ぎる。 しか し, Sが
証明可能であろ うとなかろ うと
, Bew(匡
S￢)→Sは
真 である。)こ
うして,□
A→
Aの
形 のすべての文のすべての翻訳 は真 である。 この翻訳は
,算
術 が無矛盾 であるかぎり算術 の定理ではない。 そ う す ると,Gの
定理の翻訳である算術 の定理 (これ らはすべて真 である)以
外 に,算
術 の証明可能性 に関す る真 なる原理 があることになる。では,
その よ うな算術 の真理 に対応す る様相論理の体系 は 何 か?そ
こで,Gの
定理の翻訳 にBew(「
S￢)→Sを
加 えた算術 の真理 に対応す る様相論理の体系 を考 える。つまり,Gの
すべての定理 と□A→
Aの
形 のすべての様相文 を公理 とし,(算
術 の真理 はモ ドゥス・ポネンスに関 して閉 じているから)モ
ドゥス・ポネ ンスに関 して閉 じた様相論理の体 系 をG*と
す る。 このG*は
(必然化 について閉 じていないか ら)正
規体系 ではないが,G*の
すべ ての定理のすべ ての翻訳は算術の真理である。逆 に, G*に
対す るソロヴェイの第二完全性定理 に より,
ある任意の様相文のすべての翻訳が算術 の真理 ならば,
その様相文はGキ の定理である。1 3.4
以後の計画 われわれは,様
相論理Gと
他の体系 の比較 から始 め,Gに
関す るかぎりでの算術 に関す る事実 を 確認す る。ついで,Gの
意味論 を検討 し,規
範モデルおよび本の方法 によるGの
完全性定理 に触 れ る。 さらに,ベ
ルナルデイとスモ リュ ンスキーの定理 とその一般化,
そしてソロヴェイの完全1生定 理, S4の
定理のある証明論的双 り扱 い,Gに
対す るクレイグの補完定理等 に至 る予定である。 §2 Gと
他の正規様相論理 との比較2,1
様相命題論理G
本節では,様
相命題論理Gの
構 文論的 (証明論的)性
質 について調べ,他
の正規体系 との比較 を 行 う。 まず,様
相文 を定義す るために,以
下の記号の可算無限列 を用意す る: 上,
→,
□,(, ), pl, p2, p3,・
……… `上'は「偽」 を表す0項
命題結合子であり, `→ 'は条件法, `□ 'は「必然性」 の演算子, `('
と`)'は
括弧,pI以
下は文変項である(適宜,pl, p2, p3の
代 わ りにp,q, r等
で代用 させ るこ とがある)。A,Bを
支変項上 を走 るメタ変項 として用いる。 さて,様
相文(mOdal sentences)を
つ ぎの よ うに帰納 的 に定義 す る。
(1)上
は様相 文で あ る,(2)各
文変項 は様 相 文 で あ る,(3)Aと
Bが
様 相 文 な らば,(A→ B)も
様 相 文 で あ る,(4)Aが
様 相 文 な らば,□
Aも
様 相 文で あ る。 □Aを
「Aの
必然化」 と呼ぶ。また,上
,□
上,(□
上→ ■)の
よ うな文変項 を含 まない様相 文 を 「 文変項無 しの文」 または「純 然 た る文」 と呼 ぶ。O項
命題結合 子 `止'を
原始 記 号 と して採 用 す る理 由は主 と してつ ぎの三点 で ある。 まず第一 に , 命題 計算 で常 に偽 とい う値 を持 つ`上'は ,`→'と ともにすべ ての命題結合子 を表現で きるとい う意 味 での命題結合子 の「完 全系」 を形 づ くることで ある。 第二 に,
も し上が原始 記号 で あれば,体
系 が無矛盾 で あ ることを,「 上は その体系 の定理 では ない」 (つ ま り/上
)と ,
きわめ て簡潔 にかつ一 般 的 に表現で きるこ とで ある。第二 に,上
が原始記号 で あれば,
あ る文変項無 しの文の存在 が保証 され るこ とで ある。 い くつ かの文変項 無 しの文は,算
術 の い くつ かの重要 な命題 の「代表」となる。 例 えば,□
上 は算術 は矛盾 してい るとい う (偽 の)命
題 を代表 し,￢
□ 上→￢□ ￢□ 上 は第二 不完 全性 定理 を代表す る。 さて,他
の命題 結合子 や様相演 算子 につ いての定義 を して お く。 ￢A=Df(A→
上) 下 三Df。 ￢ 上(AVB)=Df.(￢
A→
B)
(A&B)=Df。
￢(A→
￢B)
(APB)=Df.(A→ B)&(B→
A)
◇A=Df￢
□ ￢A
また,後
に必要 とな る「部分 文」 の帰納 的定義 を与 える。(1)す
べ ての文 は それ 自身 の部 分文で ある,(2)(B→ C)が
文Aの
部 分 文の とき,B,Cも
Aの
部 分 文 で あ る,(3)□
Bが
文Aの
部 分 文 の と き,Bも
Aの
部 分 文 で あ る。 ここで,様
相 命題 計算 とい うもの を,計
算 の公理 と呼 ばれ る文の集合 に計算 の推 論規則 と呼 ばれ る文上 の関係 の集合 がイ半うもの と して理 解す る。 その計算 にお け る文 の証 明 は,通
常 の よ うに,各
構 成要素 が計算 の公理 かまたは列 内の先行す る文 か ら推 論規則 によって直接 に導 かれ る文 で あ り, その最後 の文 が当の文で あるよ うな,文
の有限列 で あ る。 (文Bが
Al,中
●,Anか
ら推 論規則Rに
よって直接 に導 かれ るのは,〈Al,―
・,An〉CRの
と き,
かつ その と きにか ぎる。)ま
た,文
が計算 の定理 で あるのは,
その計算 において その文の証 明 が存 在す る ときで ある。(`卜A'に
よって「Aは
様相 と証 明可能性
(I)
■Lの
定理 で あ る」 を意味 す る。)モ
ドゥス 。ポ ネ ンスはすべ ての順序 三つ組:〈A,(A→
B),B〉
を 合 む関係 で あ る。必然化 はすべ ての順序 対 :〈A,□
A〉 を含 む関係 で ある。代入 は,あ る文変項pl, …, pら お よびあ る文Cl,―
・,Cnに
対 して,Bが
Aに
おけ るpl,・・・,pnの
各 出現 をそれぞれCl, …, Cnの
出現 で置 き換 えて得 られ る結 果で あ るよ うなすべ ての順序 対 〈A,B〉
を合 む関係 で ある。Bが
Aか
ら代入 によって直接 に導 かれ るとき, Bは
Aの
代入例 と呼 ば れ る。 こ こで正式 に様相命題論理Gを
定義 す る。Gの
公理 はすべ ての トー トロジー,□
の配分 公理,す
なわ ち □
(A→
B)→
(□A→
□B)の
形 のすべ ての様相 文, お よび □ (□A→ A)→
□A
の形 の すべ ての様 相 文で ある。Gの
定理 は上 の三種類 の公理 を含み,モ
ドゥス・ポ ネ ンス,必
然 化,代
入 の二つの推 論規則 に関 して閉 じた文 の集合 で ある。 さて,
トー トロジー と□ の配分 公理 を含 み,モ
ドゥス・ポ ネ ンス と必然化 と代入 に関 して閉 じて い る体系 を正規体系 と呼ぶ。Gも
正規 体系 で あ る。 これか ら考 える正規体系 の うち,T, S4,B,
S5が
□p→pを
定理 とす るの に対 して,Gは
これ を定理 とは しない。 も し定理 な らば,必
然化 に よ り,
□ (□ p→p)も
定理 だ か ら,公
理 □ (□ p→p)→□pか
ら□pも
定理,従
ってpが
定理 とな り,任
意 の文 が定理 とな り矛盾 す る。 しか し,後
に見 るよ うに,Gは
無矛盾 で あ る。 ゆ えに □p→ p はGの
定理 とは な り得 ない。2.2
正規 体系 こ こで,Gを
他 の正規体系 と比較 す るため に,Gを
含 む七つ の正規 体系 で あ る様相 命題 計算 を定 義す る。 すべ ての トー トロ ジー とすべ ての配分 公理 (□(A→
B)→
(□A→
□B)の
形 の文)は
各 体系 の公理 で あ る。各体系 の推 論規則 はモ ドゥス・ ポ ネ ンス と必然化 で あ る (代 入規則 は派 生す る ことをす ぐ後 に示 す)。 計算Kは
他 の公理 を持 たない (七 つの うちの最小体系 で ある)。 計算K4の
他 の公理 は□
A→
□□Aと
い う形 の文で あ る。計算Tの
他 の公理 は□A→ Aと
い う形 の文で あ る。 計算S4の
他 の公理 は□A→ Aと
□A→
□□Aと
い う形 の文で ある。 計算Bの
他 の公理 は□A→
A
と
A→
□◇Aと
い う形 の文で あ る。計算S5の
他 の公理 は□A→ Aと
◇A→
□◇Aと
い う形 の文 で ある。計算Gの
他 の公理 は,
□ (□A→ A)→
□Aと
い う形 の文で ある。体系
Lの
定理 がすべ て体系Mの
定理 で あるとき,体
系Mは
体系Lの
拡 張 で ある (ま た は, Lは
M
へ と拡張 された)と
言 われ る。 そ こで,
“Lの
すべ ての定理 はMの
定理 で あ る"を
`L⇒
M'
と略 記す る と,上
の定義 か ら明 らかにつ ぎの よ うにな る。G
今K⇒
K4
け↓
S5ぐ T⇒
S4
↓B
実 は
,以
後 に証 明 す る定理 によれば,実
際 には この七 つ の体系 はつ ぎの よ うな関係 に あ るこ とが半J 明す る。K⇒
K4⇒
G
↓サ
T⇒ S4
サけ
B⇒
S5
さて,
これ ら七つの体系 が正規 で あることを示 す。 それ には,七
つ の体系 がすべ ての トー トロジ ー と配分 公理 を含 み,モ
ドゥス・ポ ネ ンス と必然化 を推 論規則 とした か ら,
これ らの体系 の定理 の あ らゆ る代入例 が再 びその体系 の定理 とな ることを示 せば十分 で ある。Aを
,七
つ の うちの任意 の 一 つ の体系 の定理 と し,Bを ,Aに
おけ る文変項 pl,・・・, pnの
各 出現 をそれ ぞれCl,…
。, Cnの
出現 で置 き換 えた結 果 とす る。
Al,―
・, Am(=A)を
その体系 におけ るAの
証 明 とせ よ。 文Dに
対 して, D° を,Dに
お け る各pど のすべ ての出現 を各CJで
置 き換 えて得 られ る結 果 とす る。 そのと き, A°三
Bで
あ る。 ここで, Al°,・・・,A∫
はBの
証 明 で あ るこ とを確 かめ た い。 その ため に, まず,
その体 系 の公理 の代入例 はすべ て再 び その体系 の公理 で あ るこ と,をまず確 かめ る。 これは, 公理 が実際 には公理 シェーマで あ る こ とか ら明 らかで あ る。 つ ぎに,モ
ドゥス・ポ ネ ンス と必然化の関係は〔°
'の
操作 を通 じても保存 されることを示す。実際 に, Akが
AJと
Aj(=Aヶ
→Ak)か
らモ ドゥス 。ポネンスによって得 られた とすれば,Aj°
=(Aザ
→Ak)° 三AF→
Afだ
から,Aざ はAデと
Aj:か
らモ ドゥス・ポネンスによって得 られる。 また, Ak(=□
Aど)が
Aど から必然化 によって得 られた とす ると, Ak°
=(□
Aど)°=□
Aド だから,Ak° はAFか
ら必然化 によって得 られる。 こうして
,上
の七つの体系はすべ て正規体系であることが示 された。また
,正
規体系は真理関数的帰結 についても閉 じている。実際,
もしBが
,正
規体系 の定理Al,…
, Anの
真理関数的帰結 ならば,
その ときBも
その体系の定理である。 なぜ な ら,Aは
,Al,・
・・,Anと
トー トロジー (Al→ (・中(An→ B)・・・))か
ら,モ
ドゥス 。ポネンスをn回
適 用す ることによって得 られるか らである。 さらに
,A→
Bが
正規体系Lの
定理 ならば,□A→
□Bも
Lの
定理である。とい うのは
,卜
LA→ Bな
らば,必
然化 によ リ トL□(A→
B),配
分公理 よ リ トL□(A→ B)→
(□A
→□
B),ゆ
えにモ ドゥス 。ポネンスによ リ トL□A→
□Bだ
からである。 それゆ え,APBが
正規 体系の定理 ならば,□
Aユ
ロBも
その体系の定理である。Kは
他のすべての正規体系へ と拡張 され るとい う意味で,最
小の正規体系である。 さてここで,以
後の考察 に必要 なか ぎりで,
い くつかの定理 (正確 にはメタ定理)を
記録 してお く。2.3
い くつ かの定理定理
2-1((2-1'の
`2'は
§
2の
2で
あり
,`1'は
そこでの通し番号。以下同様。
)様相 と証明可能性
(I) 13
すべ ての文
A, Bに
つ いて,卜K□
(A&B)言
(□A&□
B)。《
証明》
A&B→ Aは
トー トロジー だ か ら,
卜【A&B→
A。 必然化 と配分公理 によ り,卜K□(A&B)→
□A。 同様 に
,
卜K□(A&B)→
□B。 ゆ えに命題 計算 によ り,
卜K□(A&B)→
□A&□
B。 逆 は こ うなる。rK A→
(B→
A&B)(ト
ー トロジー)か
ら必然化 と配分 公理 によ り,
卜K□A→
□(B→
A&B)。
しか るに配分 公理 よ り,
卜K□(B→
A&B)→
(□B→
□(A&B))。
これ らか ら 命題 計算 によ り,
卜K□A→
(□B→
□(A&B)),す
なわ ち 卜K□A&□
B→
□(A&B)。
こ うし て,
卜K□(A&B)●
(□A&□
B)。Q.E D.
定理
2-2
すべ ての文
AI,…
。,Anに
つ いて,卜K□
(Al&・
・・&An)'(□Al&‥
・&□
An)。《
証明》
定理
2-1を n-1回
使 う。すなわち,
卜K□(Al&…
&An)P(□
Al&□
(A2&…
&An))ど
(□
Al&□ A2&□
(A3&…
・&An))'・
…P(□
Al&…
・&□
An)。 ゆ えに,
卜K□(Al&…
・&
An)'(□
Al&…
,&□
An)。Q.E.D
定理
2-3
Lを
正規体系 とす る。 その とき,卜
LAl&…
・&An→
B
ならば,
卜L□Al&…
・&□
An→ □B。《
証明》
卜
LAI&…
&An→
B
とす ると正規性 より(つま り,必
然化 と配分公理 より),
卜と□(AI &
・¨
&An)→
□B,
しかるに定理2-2よ
リ トL□(AI&… &An)'(□Al&…
・&□
An),
ゆ えに卜L□
Al&…
&□
An→ □Bo Q.E.D
系1
Lが
正規体系 であ り,
かつ 卜LA→ Bな
らば,
卜と◇A→
◇B。《
証明》
Lが
正規 で 卜LA→ Bと
す る。 文↓偶 よ リ トL￢
B→
￢A。 定理2-3に
よ り,
卜L□
￢B→
□ ￢A,
ゆ えに対偶 よ リ トL￢
□ ￢A→
￢□￢B,つ
ま リ トL◇
A→
◇Bo Q.E D.
系 2
Lが
正規体系 な らば,
卜L◇
A&□
B→
◇(A&B)。
《
証明》
ゆえに
,
卜L□
B→
(□￢(A&B)→
□￢A),
後作の対偶 によ り,
卜L□
B→
(￢□￢A→
￢□￢(A&B))。
ゆ えに,
卜￢□￢A&□
B→
司□￢(A&B),
すなわち 卜L◇
A&□
B→
◇(A&
B)o Q E D
定理2-4(同
値代入)F(A)(ま
た はF(B))は
,
あ る支F中
のpの
すべ ての出現 を文A(ま
たはB)の
出現 で置 き 換 えた結 果 で あ る。 その と き, Lが
正規体系 でかつ 卜LA●
B
な らば, 卜LF(A)ど
F(B)。
《
証明》
証 明 は文Fの
複雑 さに関 す る帰納 法 による。 まず,
卜LAPBと
仮 定 せ よ。 も しFが
上の と き,F(A)も F(B)も
上で あ る。 上ど 上は トー トロ ジーで あ るか ら,
卜LF(A)言
F(B)。
も しFが
pそ
の もので ある と き, F(A)は A,F(B)は
Bだ
か ら,仮
定 よ り,当
然 卜LF(A),F(B)で
あ る。 も しFが
p以
外 の文変項qの
と き, F(A)も F(B)も
qで
あ り, qご
qは
トー トロ ジーだ か ら,
卜LF(A)ユ
F(B)。
つ ぎに帰納 のステ ップで ある。Fが
(G→
H)と
す る。このときF(A)
は
(G(A)→
H(A)), F(B)は
(G(B)→
H(B))で
あ る。帰納 法 の仮 定 によ り,「 LG(A)
,G(B),
■LH(A),H(B)だ
か ら,命
題 計算 によって,
卜L((G(A)→
H(A))ご (G(B)
→H(B)),
す なわ ち,
卜LF(A)ど
F(B)。
最後 に, Fが
□Gと
す る。帰納 法 の仮 定 によ り, 卜
LG(A),G(B)。
Lは
正規 体系 だったか ら,必
然化 によ り,「
L□
(G(A),G(B)),
ゆ え に,定
理2-1と
命題 計算 によ り,
卜L□
(G(A)→
G(B))&□
(G(B)→
G(A)),
配分 公理と命題 計算 によ り
,
卜L(□G(A)→
□G(B))&(□
G(B)→
□G(A)),つ
ま リ トL□
G(A)ご
□
G(B),す
なわ ち,
卜LF(A)「
F(B)。
Q E.D.
以後,定
理2-3, 2-4は
断 りなしで用いるし,
また,□
と￢◇￢,￢
□ と◇￢,￢
◇ と□￢, および真理関数的 に同値 な文 を互 いに自由に交換す る。 定理2-5
定理2-4と
同 じ仮 定 の もとで,
卜K4□(APB)→
□(F(A)言
F(B))
《
証明》
証 明 は定理2-4の
証 明のK4で
の形式化 とな る。Fが
上の と きF(A)も
F(B)も
上で あ り, 「 Kl上Ptto K4は
正規 だ か ら必然化 によ り,
卜K4□(上言 上)。 ゆ えに,
卜K4□(ArB)→
□(上 ど 上)。Fが
pな
らば, F(A)は A, F(B)は
Bだ
か ら,
トリヴ ィアルに,「
K4□(APB)→
□(Aご
B)。Fが
p以
外 の文変項qの
と き,Fが
上の と きと同様 に 卜(4 q tt q か ら必然化 と命題 計 算 よ り,
卜(4□(A「 B)→
□(qど q)。 つ ぎに帰納 の ステ ップで あ る。Fが
(G→
H)の
と き,帰
納 法 の仮 定 よ り,卜 Kl□
(APB)→
□(G(A)ユ
G(B)),
卜K4□ (A tt B)→ □(H(A)言
H(B))。
様相 と証明可能性
(1) 15
ら
,定
理2-3よ
り,
卜K4□(G(A)言
G(B))&□
(H(A)ど
H(B))→
□(F(A),F(B))
で あ る。 ゆ えに,命
題 計算 によ リ トKl回(Aど B)→
□(F(A)「
F(B))。
最後 にFが
□Gの
と き,帰
納 法 の仮 定 よ り,
卜K4□(ArB)→
□(G(A),G(B))。
こ こで, G(B)は G(A),G
(B)と
G(A)の ,G(A)は G(A),G(B)と
G(B)の
,
それ ぞれ真理 関数的帰 結 だか ら, 定理2-3に
よ リ トK4□(G(A),G(B))→
(□G(A)→
□G(B)),
卜Kl□(G(A),G(B))
→(□G(B)→
□G(A)),
ゅ えに命題 計算 によ り,
卜KI□ (A tt B)→ (□G(A)言
□G(B)),
す なわ ち,
卜K4□(APB)→ (F(A)=F(B))。
必然化 によ り,
卜K4□ □ (A tt B)→ □(F(A)
,F(B))。
ところがK4に
固有 な公理 によ り,「
KH□(APB)→
□□(A tt B),ゆ えに,
卜K4□(Aど
B)→
□(F(A)言
F(B))。
Q.E,D.
定理
2-5は
K4に
関す る定理 で あ るか ら, K4の
すべ ての拡 張 に関す る定理 で もあ る。 また, この証 明 において,
□ p→pが
使 われて い ない こ とに注 意 して お こ う。定理
2-6
卜
TA→
◇
A,
卜T□
A→
◇
A
《
証明》
Tに
固有な公理により, 卜
T□
￢A→ ￢
A,
ゆえに 卜
TA→
￢□￢
A,つ
まり
「
TA→
◇
A。ま
た
,
これと 卜
T□
A→
Aか
ら 卜
T□
A→ ◇
Ao Q.E.D.
定理
2-7
卜
S4□◇
AP□
◇□◇
A
《
証明》
S4の
固有公理により
,
卜
sI□◇
A→
□□◇
A。ところで
,定
理
2-6よ
リ トT□ ◇
A→
◇□◇
A。
正規性 と
S4が
Tの
拡張であることにより
,「
sI□□◇
A→
□◇□◇
A。ゆえに
,
卜
s4□◇
A
→□◇□◇
A。逆 に
,定
理
2-6と
S4が
Tの
拡張であることにより
,
卜
sI□◇
A→
◇◇
A。定理
2-3の
系 1よ り
「
sI◇□◇
A→
◇◇◇
A, S4の
正規
'性よリ ト
s4□◇□◇
A→
□◇◇◇
A。一方
,S4の
固有公理 によリト
s4□￢
A→
□□￢
A,対
偶 によリト
sI◇◇
A→
◇
A,同
系 1に よリ ト
s4◇◇◇
A→
◇◇
A,
ゆえに 卜
sI◇◇◇
A→
◇
A。ここで正規性 により
,
卜
s4□◇◇◇
A→
□◇
A。従
って
,
卜
sI□◇□◇
A→
□◇
A。以上より
,
卜
s4□◇□◇
Aユ
ロ◇
A。Q.E.D.
この定理 に関連 して言 えば
,後
に全 く別 の根拠 か ら,
卜G□
◇Aど
□◇ □◇Aで
あ るこ とが証 明 され る。さて
,
ここで正規体系S5を
含 む任 意 の正規体系 は体系S4と
体系Bを
ともに含 み,
かつ その逆 も成 り立つ こ と,言
い換 えるとS5=S4+Bで
あ る こ と,
を示 す。 その ため に, S4+B=5S
と して, 5Sと
い う新 たな体系 を設定す る。 す ると,体
系5Sの
固有 公理 は □A→
A,□
□A→
定理 が一致 す ることを示 す。 定理
2-8
卜
S5A
の と き, かつ その と きのみ 卜5S A。《
証明》
卜
5S◇A→
□◇
A,「
s5□A→
□□
A,
卜s5A→ □◇
A
を示せば十分である。
(1)「
5S B→□
◇
Bだ
から
, Bと
して◇
Aを
とると
,
卜
5S◇A→
□◇◇
A。ところで
,
卜
s4□￢
A→
□□￢
Aと
対
偶 によリト
s4◇◇
A→
◇
Aで
あるから
,正
規性 によリト
5S□◇◇
A→
□◇
A。ゆえに
,
卜
5S◇A→
□◇
A。 (il)卜 s5□￢B→ ￢
Bと
対偶 より
,
卜s5B→ ◇
B,Bと
して□
Aを
とると
「
s5□A→
◇□
A。
ところで
「
s5◇B→
□◇
B,Bと
して□
Aを
とると 卜
s5◇□
A→
□◇□
A,
ゆえに
,
卜
s5□A
→□◇□
A。ところで
,「
s5◇￢
A→
□◇￢
Aと
対偶 によリ
ト
s5◇□
A→
□
A,
正規性 よリト
85□◇□
A→
□□
A。ゆえに
,
卜
s5□A→
□□
A。 ()卜
s5□￢
A→
司
A
と対偶 によリトs5A→
◇A。 ところで
,
卜s5◇A→
□◇A。 ゆ えに,「
s5A→
□◇A。定理
2-9
Q.E D
/G□
p→ p《
証明》
各様相 文
Aに
だ を対応 させ,も しAが
Gの
定理 で あれ ばAは
トー トロ ジーで あ るが,(□ p→p)* は トー トロ ジーで ない ことを示 す ことによって証 明す る。*を
つ ぎの よ うに定義 す る:上*=上
pキ
=p(す
べ ての文変項pに
対 して)(A→
B)半=Aキ
→B*
(□
A)*=T。
つ ま り
, A*は
,Aに
おけ る□ を “真理演 算子"とみ た ときの結果で あ る。 も しAが
トー トロ ジー な らば,明
らか にA*も
トー トロ ジーで あ る。 も しAが
配分 公理 □(B→
C)→
(□B→
□C)な
らば,A*=T→
(T→
T),つ
ま りA*は
トー トロ ジーで あ る。 また,す
べ てのAに
対 して,(□
(□A→
A)→
□A)*=T→ T,
つ ま りA*は
トー トロ ジーで ある。 こ うしてGの
任 意 の公理Aに
対 して:A*は
トー トロ ジーで ある。AⅢ と(A→
B)キ=A*→ B*が
トー トロ ジー な らば,B・
も トー トロ ジ ーで ある。 また, A*が
トー トロ ジーで あれば,(□
A)・=Tも
トー トロ ジーで あ る。 こ うして, 解釈*に
おいて,モ
ドゥス・ポネンス と必然化 は トー トロ ジー性 を前提 か ら結論へ と伝 達 す る。 ゆ えに,Aが
Gの
定理 な らばA*は
トー トロ ジーで ある。 しか し,(□
p→ p)・三T→
p
はpと
同値 では あ るが,
トー トロ ジーで は ない。従 って,□
p→pは Gの
定理 では ない。 系 1Q.E.D
様相 と証明可能性
(I) 17
/K□
p→
p 《証 明》 定理2-9と ,Gが
Kの
拡 張 で あ ることによ る。 系 2Q E.D.
正規 体系Gは
無 矛盾 で あ る。《
証明》
定理2-9よ
り,Gで
は証明で きない式が少 な くとも一つ存在す るか らGは
無矛盾である。Q.E D.
ところが,Gの
固有公理 (の一つ)で
ある □(□p→p)→
□p
はS5の
定理ではない,
それゆ え,K,K4,T, S4,Bの
いずれの定理で もない(S5は
これ らの拡張 だか ら)。 定理2-10
/S5□
(□p→p)→
□p《
証明》
★
をつぎのように定義する
: 上★=上
p★=p
(A→
B)★=A★
→B★ (□A)★=A★
要す るに, A★ は
,Aか
らすべ ての□ を消去 した結 果で あ る。 この と き,(□
(A→
B)→
(□A→
□ B))士=(A☆
→B★)→ (A・→B★)は
トー トロジー。 (□A→
A)★=A★
→A士 は 卜_ト
ロ ジー。(◇
A→
□◇A)★=￢
￢A★→ ￢￢A★ は トー トロ ジー。 こ うして,Aが
S5の
定理 な らば,A★
はトー トロ ジーで ある。 しか し
,(□
(□p→ p)→□p)★=(p→
p)→p=pは
トー トロ ジーで は な い。 ゆ えに,□
(□p→p)→
□pは
S5の
定理 で は な い。Q.E.D
こ うして,Gと
Tは
ともに無矛盾 な様相論理 の体系 で あ るが,Gと
Tの
いず れ をも含 む (両 者 の 拡張 で ある)無
矛盾 な体系 は存 在 しない ことにな る。 定理2-11
卜G□
p→
□□ p《
証明》
p→ (□
p&□
□p→p&□ p)は
トー トロ ジーで あ る。 ゆ えに,
卜Gp→
(□p&□
□p→p&
□p)。 定理2-1に
よ り,
卜G□
(p&□
p)=□
p&□
□p…
… (*)。 ゆ えに,定
理2-4よ
り,卜
Gp→
(□(p&□
p)→p&□
p)。 正規性 によ り,
卜G□
p→□(□(p&□
p)→p&□
p)。 と ころが,Gの
固有公理 :□(□p→ p)→□pの
〔p'1こp&□
pを
代入 す る こ とによ リ トG□
(□(p
&□
p)→p&□
p)→ □(p&□
p)。 ゆえに,
卜G□
p→ □(p&□
p)。(*)に
よ り,
卜G□
p→ □p&□
□p。 ゆ えに,
卜G□
p→ □□po Q.E.D.
Gは
正規体系 だか ら,定
理2-11に
より,固
有公理 として□A→
□□Aの
み を持つ正規体系であ るK4の
すべての定理 はGの
定理で もある。 こうして,定
理2-5は
, `K4'を
`G'に
置 き換 えて も成 り立つ。す なわち, 系 定理2-4と
同 じ仮 定 をお くとき,
卜G□
(APB)→
□(F(A),F(B))。
定理2-12
(a)卜 G□
(□A→
A)=□
A
(b)卜 G￢
□A「
◇(￢A&□
A)
(C)卜 G◇
Bユ
◇(B&□
司B)
(d)卜 G□
A●
□(A&□
A)
(e)卜 G□
A→
(◇B,◇
(B&A&□
A))
《
証明》
(a)Gの
固有公理 よ り,
卜G□
(□A→ A)→
□A。 また,
卜GA→
(□A→
A)と
正規性 よ り 卜G□
A→
□(□A→
A)。 ゆ えに 卜G□
(□A→ A)ご
□A。(b)(a)の
両辺 を否定すれば得 られる。(c)(b)で
Aを
￢Bと
す ることか ら得 られる。(d)ま
ず,定
理2-11よ
り「G ttA→ □□A。 ゆえに 卜G□
A→
□A&□
□A。 ところが定理
2-1と
Gが
Kの
拡張 であることによ り,
卜c□
(A&□
A)「
□A&□
□A。 ゆ えに,卜G□
A→
□(A&□
A)。 逆 に,
卜GA&□
A→
A
と正規性 よ り「
c□
(A&□
A)→
□A。 ゆ え1こ 卜G□
AP□ (A&□
A)。(e)定
理2-3の
系2に
よ り,
卜G◇
B&□ (A&□
A)→
◇(B&A&□
A)。 これ と(d)に
よ り,
卜G◇
B&□
A→
◇(B&A&□
A)。 ゆ えに,
卜G□
A→
(◇B→
B&A&□
A)。 逆 に,B&A&□
A→
Bが
トー トロジーであることと,定
理2-3の
系1よ
り,
卜G◇
(B&A&□
A)→
◇B。 ゆ えに,
卜G□
A→
(◇(B&A&□
A)→
◇B)。 ゆえに 卜G□
A→
(◇Bご
(◇B&A&□
A))。
定理2-13
Q.E.D.
卜
G□
上
'□
◇
p《
証明》
卜
G上→◇
p,そ
れゆえ
Gの
正規性によリ ト
G□
上→□釣 。逆に, 卜
Gp→
T,定
理
2-3の
系
2よ
リ トG◇
p→◇T,正
規 性 に よ リ トG□
◇ p→□ ◇ T。 と こ ろ 力比 卜c◇ TP司
□ ￢T,「
G◇様相 と証 明可能性(I)
