57
高階古典論理の形式的体系の試作 Ⅰ
兼 岩 龍
1.高 階古 典 論 理 を我 々 は
対 象領域 D (空 でない集合)
真理値 の集合 T‑〈T(true), ↓ (false)〉
オペ レー タ p (集合Aか ら集合Bへ の関数 全体 を
BAJJで表す)
の3者 の組 み合 わせで生ず る集合 の上 の算術 とみなす ことか ら始 める｡ 例 え ばTTJJは1変数真理関数全体 か らなる集合 を表 すので
TT〃‑ 〈[plp](恒等関数),‑ (not), [pIT] (Tの値 を とる定値 関数), [pl⊥] (⊥の値 を とる定値 関数)〉
となる.ここで注釈 が必要で あろう｡まずAか らBへ の関数 とはAxBの 部分集合 fが ｢各々のx∈ Aに対 して, それぞれただ1つずつ
(x, y)Ef
となるyが存在 す る｣とい う条件 を満 たす とき, この集合 fの ことをい う｡
即 ち通常,写像 のグラフ と呼 んでい る ものを我々 は関数 と呼ぶのであ る｡従 っ て関数 その ものが全射 か どうか とい うの は意味がない｡ また変域 の指定 され た変数 Ⅹ と Xの式 F (Ⅹ)を用 いて,[Ⅹ1F(Ⅹ)]で aに対 して F(a)を対応 させ る関数 を表す｡即 ち変数 Ⅹの変域指定が Aの とき
lxIF(x)]‑ ((a,F(a)):aEA)
で ある｡上記 において変数pの変域指定 はTで ある｡
他 の例 を見 てみ よう,TTJJT〃はTか らTTJJへ の関数全体 であ るか ら, これ は2変数真理関数全体 とみなす ことがで きる｡>(either), < (both),
ラ (if)はこの集合 の元 で これ らをいれてTTjLTJLには全部 で 16個 の要素が ある｡ αの関数fによる像 をjTaと書 けば, >, <,⇒ は
>T‑ [plT], >⊥‑ [plp],
<T‑ [plp], <↓‑ [pl⊥],
⇒ T‑ [plp], ⇒ ↓‑ [plT]
で特徴づ け られ る｡ここに ‑ はメタ理論(metathoery)としての等号 で ある｡
メタ理論 を,本稿 において は普通 の数学で展開す る｡
さらに1階 1変数述語全体 はTDJL,1階 2変数述語全体 はTDJLDJJ,1階 3変数述語全体 はTDJJDγD/∫,2階 のTDJJを対象領域 とす る1変数述語全 体 はTTDppとな る｡ ∀ (全称記号), ∃ (存在記号)はTTDJLFEの元 と考 え
る こ とが で きる｡ その よ うにす れ ば,通 常 ∃X X>yと書 か れ る もの は
∃ [Ⅹ[>xy]と書 かれ ることになる｡ ここに変数 Ⅹ,yの変域指定 はD,>
はTD〃D〟 の元 と考 えてい る｡ 従 って順 に
1.> ∈ TDノJDJJ, 2.>Ⅹ ∈ TDノJ,
3.>Ⅹy ∈ T, 4.[】‖>Ⅹy] ∈ TD〟, 5.jlxZ>xy]E T となる｡ ∀, ∃ は
∀p ‑ T iff P‑ [XIT],
∃p‑↓ iff P‑ [ⅩI⊥]
で特徴 づ け られ る｡ここに変数 Pの変域指定 はTDノJ,変数 Ⅹの変域指定 はD であ る｡
我々 は
D,T∈朝, A,B∈ Ⅶ impliesBA/J∈ 朝
となる最小 の集合 u をD上 の論理集合 と呼 び,Log(D)で表す ことにす るO 文字 〟,D,Tか らなる文字列が Log(D)の元 を表す ための条件 を求 めて み ようou‑ (JL,D,T)の元 で生成 され る自由半群 を 丑 (ここでFLはD,
高階古典論理の形式的体 系の試作 I
Qユニ 開 すβ若 く) ご崇
聞
D,T
図 1
59
T以外 の適 当な元 と考 えてお く),Gtを Gt‑ (0,1,2,･･弓 とす る. そ こで u ∈ u,S∈ Gtに対 して
q)(u,S)‑ S+ 1,ifu∈〈D,T)ands≧ 1;
‑S‑ 1,ifu‑jLands≧3;
‑0 ,otherwise
として uX6tか らGtへの関数 甲 を定義す る. さ らに関数 q'(u,S)を基 に して,帰納的 に丑×Gtか ら6tへの関数 少を
￠(E, S)‑ S,
￠(Xu, S)‑q)(u,￠(X, S))
で定 める｡ ここにEは 足 の単位元,X ∈ 足,u∈ u, S∈ 6tである｡ こ の ときX∈丑＼ 〈E)が Log(D)の元 を表す ための条件 は
￠(X,1)‑ 2
である.￠(X,1)≧ 1な ら Y∈丑が存在 してXYは Log(D)の元 を表す｡
4･(X,1)‑ 0な ら, この ような Y は存在 しない｡
証 明 はX∈里＼(E)の長 さに関す る帰納法 で得 られ る｡ Xの長 さとは
X ‑ulu2･･･un (ul, 狗,･･･,un∈u)
となるnの ことである.
A,A′,B,B'が 空でない集合 で組(A,B)と(A',B′)が異 なれ ばBAJL とB′A'jLは集合 として異 な るので
(X∈旦 ;￠(X,1)‑ 2)
の異 な る元 はLog(D)の異 な る元 を表 す ことになる｡ 従 って Log(D)‑ 〈X ∈旦 ;4J(X,1)‑2〉⊂里
と考 えて よい. そのわ けは,半群 足の元 でLog(D)の元 に対応 す る もの を Log(D)の元 で置 き換 えた 里に対等 な集合 B′に丑と同型 な半群構造 を与
え 里 の代 わ りに考 えることによ り実現で きる とい うことによる｡なお これ ら の ことはD‑Tの場合 に も当て はまるように議論 を進 めて きた｡D ‑Tの
ときはuが 2元集合,従 って丑が 2元生成 となるのである｡
前 にαの関数fによる像 をfa と書 いたが, これ を我 々 はもう少 し拡張 し て ′ とαの積 のように思 いたい｡例 をみ る ことに しよう｡
D ‑ (0,1,2,･･･)
の ときC> a+bをポー ラン ド記法で書 けば>C+ abとなる｡
>∈ TDJJD/∫,+ ∈ DD/JDJJ
と考 え られ る｡変数 a,b,Cの変域指定 はDであ る｡我々 は意味 として, 1.> ∈ TD/JD/∫, C∈ D,
2.>C ∈ TD〝, + ∈ DD〝D/J,
3.>C+ ∈ TD〝D/J, a∈ D,
4.>C+ a ∈ TD〝, b∈ D,
5.>C+ab∈ T
と思 うことがで きる｡ この例 で2.か ら3.へのステ ップ を除 けば,例 えば 4.か ら 5.へ の ス テ ップ で >C+ aを′,bをαと思 う こ とに よ り,
>C+ abが ′ に よるαの像faとな るように,すべ て前 の定義 で説 明 で き るが, 2.か ら3.へ のステ ップ はそ うはいかない｡ これ を説明で きるよう にす るため,少 し準備 しよう｡
A ∈ Log(D)に対 してAの特定 の元 を表 すために,我々 は定数記号 (con‑
stant)を用 い る｡ 既出の ものでいえば,
T, ⊥,‑, >, <,ラ ,∀, ∃, >,+
がそ うである.これ に対 して,Aの不特定 の元 を表 すために,変数記号(vari‑
高階古典論理 の形式的体系の試作 Ⅰ 61
able)を用 い る｡各変数記号 はあ らか じめ変域指定 されてい るもの とす る｡定 数記号,変数記号 は使われ るときには品詞 (Wortart(G),wordcユass)が決 まっている｡定数記号 について は,それが属 してい る とされ るLog(D)の元, 変数記号 について は,変域指定 されたLog(D)の元が品詞 とな る｡ 定数 (記 号),変数 (記号)お よび [変数 l句]の形 の ものを語 (Word)と呼ぶ ことに す る｡ 句 は一定 の文法 に従 った語 の列 で ある｡語 にはLog(D)の元が品詞 と して決 まっている もの とす る｡tを語 の列,αを語 とす る｡またtの品詞が定 め られてい る状態 を考 える｡tの品詞 はLog(D)∪〈E,FE)の元が想定 されて い る｡
まず語 の列 としての空列 の品詞 はEである とす る｡
次 に語列 (Wordsequence)tの品詞がEで語 αの品詞が A∈ Log(D)の とき語列 taの品詞 はAである とす る｡taの意味 は勿論,語列 tの後 に語 α を継 ぎ足 した語列 を意味す る｡
次 に 語 列 tの 品 詞 が BAFL(A,B∈ Log(D)) の 形 で 語 αの 品 詞 が
AC(C∈里)の形 に書 ける とき taの品詞 をBCとす る｡ この とき
￠(A,1)‑ ￠(AC,1)‑ 2
よ り￠(C,2)‑ 2, また ￠(β,1)‑ 2であるか ら,
￠(βC,1)‑ 2
即 ちβCはLog(D)の元 で あ る｡ この こ との意味 は次 の よ うにな る｡Cは
￠(C,2)‑ 2よ り,
C‑ C,JL･･･C2JLCIFL(Cl,･･･,C,∈ Log(D),r≧0) と書 けるか ら (図 1参照),αは品詞が Cl,･･･,C,であるような r個 の語 β1,･‑ ,βγを順 にαの右 に置 くことによ り,品詞がAになる｡即 ち αは Aの元 を値 とす る r変数 の関数 としての はた らきが あ る｡ tはAか らBへ
の関数 とみれ るので,taはその合成 関数 と見 なせ る.特 にC‑Eの場合 は前 の定義 と一致す る｡ 即 ち ta は関数 tによるαの像 とみなせ る｡
最後 にtとαが上記組 み合わせ以外 の品詞 を とる ときtaの品詞 はJLで あ る とす る｡
図 2
以上 で語列 の品詞が帰納的 に決 まる｡ 語列 はその品詞が Log(D)の元であ る とき,句 (phrase)と呼 ばれ る｡ 句 は品詞がDで あ る とき名 詞句 (noun phrase,substantive),Tで ある とき文 (sentence)と呼 ばれ る｡ また品詞 の
冒頭がDで ある とき指名語 (designate),Tで ある とき述語 (predicate)で ある とい う｡ 名詞句 は指名語 の一種,文 は述語 の一種 である｡
ここで [変数 l句]の形 の語 の品詞 を定 めてお こう｡ 変数 Ⅴの品詞 をA, 句 tの品詞 をBとす る とき,[vrt]の品詞 をBAJLとす るので ある. この形 の語 を合成語 (synthesis)と呼び, この ときtを合成語 の語幹 (stem),Ⅴを 接頭変数 (prefixedvariable)と呼ぶ ことにす る｡
前 に品詞の文法(〟以外 の品詞がT,D,〟を どの ように並べ て作 られ るか) をみた とき, 中 とい う関数 を導入 したが, これ と同様 に,今度 は語列 の文法 をみるために関数 4,1を導入 しよう｡品詞がAであるような語列 島の右 に語 列 tを置 いた ときの語列 もtの品詞 を ￠1(i,A)で表 し,語列 tのAに対 す る相対 品詞 (relativewordclass)と呼ぶ ことに しよう｡ 勿論,Aに対す る相 対 品詞 は,品詞がAで あ りさえすれ ば語列 もの とり方 によらない.
まず任意 の語列 tに対 して ￠ 1(i,A)∈ Log(D)となる品詞Aが存在 す る ことがわか るO なぜ な ら,tが語 α 1,･･･,α,の列
*)BC‑DまたはTの場合, この矢線 は@ または⑦ に入る｡
**)β′C′‑ DまたはT の場合, この矢線 は⑳ または⑦ に入 る｡
高階古典論理 の形式的体系の試作 Ⅰ 63
t‑ al･･･a,
で ある とき,Cl,･･･,C,を各々α1,･･･,α,の品詞,もを品詞が
A‑BC,JL･･･CIJL(BE Log(D)) であ るような句 とすれ ば,
∫
￠1(ちt,E)‑ ￠1(i,A)‑ B∈ Log(D) となるか らである｡
このように絶対 品詞 (Eに対 す る相対品詞,即 ち品詞)が〟であるような 語列 も無意味 とい うわ けで はない｡今 の場合 あの右 にtを置 くことによ り, 品詞がβ とな るか ら JにはβC㌦ ･‑ G〝か らβ‑の関数 としての働 きが ある｡即 ち tは もの右 に置かれ る とき,｢働 き｣ として は
ββC,〃･･･Cl/叫 の元 の ように振舞 う｡
この ような,語列 tの ｢働 き｣の型 はBを度外視 して も一意的 には定 まら ない｡例 をみ よう｡
f‑∀Px
とす る｡ ここに ∀ は品詞TTD仰 の定数,Pは品詞 TDJJの変数,Xは品詞 Dの変数で ある｡B∈ Log(D)とすれ ば,tはそれぞれ
1.Al‑BDFLTDJFJLTTDpJLJL,
2.A2‑BTFLTTDJFJFJL, 3.4 3‑月D〟T/J
に対 して相対 品詞が Bとなる.tl,ち,左をそれぞれの品詞がAl,A2,A3で あ るような句 とすれ ば,tl, ち, t3の右 に tを置 く ｢働 き｣ の型 はそれぞれ
1.BED/JTD〟JLTTDpFEFLJL,
2.BBTJLTTDFLjLFLP,
3.BBDJLTJJFL となる｡
AをLog(D)の元,tを品詞 Aの句で語 の列 α1･･･α,で出来 てい るもの としよう,い ますべての q< rに対 して,
￠1(α1･･･αq,E)‑ACq(E≠ Cq∈旦)
となってい る とき,=ま純正 (pure)で ある とい う｡ 純正 な句,指名語,述語 はそれぞれ純正句,純正指名語,純正述語 と呼 ばれ る｡ 語,名詞句,文 は純 正句 であ る｡
定理 1.1.A,AC,BをLog(D)の元 (C ∈ 里),tを品詞 ACの純正句 とす る｡ この ときtのBAFLに対 す る相対 品詞 はBCである｡
証明.語列 t‑ α1･･･α,を品詞 ACの純正句 とすれ ば,q< Yに対 して,
￠1(α1･･･αq,E)‑ACCq(E≠ Cq∈里) と置 ける｡ この ときCq̲1は
Cq̲1‑ HkjL･･･H2〟HIJL(Hl,･･･,Hk∈ Log(D),k≧ 1) の形 だか ら,Cq̲1‑ GHFE(H ∈ Log(D),G∈ 丑)と置 けば,
ACCq̲I ‑ACGHp(ACGE Log(D))
とな りαqはHJU∈旦)の形 の品詞 を もた な けれ ばな らない. この とき Cq‑GJで ある｡従 って,Sを品詞 BAFEの句 とす るとき
￠ 1(Sα1･･･αq̲1,E)‑BCCq̲1 を仮定 すれ ば,BCCq̲1‑ BCGHJLであるか ら
4･1(Sα1･･･αq,E)‑BCGJ‑BCCq を得 る ことがで きる｡ ￠1(Sα1,E)‑BCClは見易 いので,結局
41(Sα1･･･α,̲1,E)‑BCC,̲1
が得 られ る｡ また 4･1(i,E)‑ACであるか ら, C,̲1‑ KFE(K E Log(D)),
直 (α,,E)‑ K とな らね ばな らない｡ よって
4･1(t,BAIL)‑￠1(st,E)‑BC となる｡ 証明終 り｡
この定理 は ｢純正句 は文法上,語 の ように振舞 う｣ とい うことを意味 して
高階古典論理 の形式的体系 の試作 Ⅰ 65 い る. 即 ち tが純正句 な らば,任意 の句 Sにたい して,
(*)forallα∈ W ord,
4,1(α,E)‑ 4･1(i,E)implies ￠1(Sα,E)‑ ￠1(st,E) が成 り立 つ｡ ここにW ordは語全体 か らな る集合 を表 す｡ しか し
定理 1.2.tが純正 で ない句 の場合 は (*)が成立 しない句 Sが存在 す る.
これ を示 してお こう｡i‑ α1･･･α,が品詞 Aの純正 でない句 の ときは, あ るq< rに対 して
forsomeCl∈旦＼〈E), ill(α1,E)‑ ACl ;
forsomeCq̲1∈ 旦＼(E), ￠1(α1･･･αq̲1,E)‑ ACq̲1;
forallC ∈ 足＼〈E), 4,1(α1･･･αq,E)≠ AC とな るo この ときCq̲1‑ Kp(K∈ Log(D)),￠ 1(αq,E)‑K
と置 ける｡ さ もな くば
forsomeC ∈ 旦＼〈E), 4･1(αll･･αq,E)‑ AC となって しまうか らで あ る｡ そ こで前述 の定理 の証 明 と同様 に して
4,1(α1･･･αq̲1,TAIL)‑ TCq̲1‑ TKFL が得 られ るので,
在 (α1･･･αq,TAIL)‑T.
したが って 4 1(i,TAIL)‑ JL.αを品詞 Aの語,Sを品詞 TAJLの句 とすれ ば ￠1(Sα,E)‑Tで あ るが ￠1(st,E)‑ JLとな る. これで (*)が成立 し ない句 Sの存在 が示 され た｡
2.形式的体系.前節 で は意味 を考 えなが ら高階古典論理 の形式 を模 索 し て きたが, ここで は [,]の2つ の記号 の列 を考 える｡ 即 ち ([,]〉で生成 さ れ る自由半群 沢 の元 をあつか う｡ まず,
巨 [],〟‑ [[]],T‑ [[[]]],D‑ [[][]]
とす る｡ lは区切 り記号 (terminator)として,JJ,T,Dは前節 の uの元 として扱 うが,もはや その意味 は前面 に出 さない ことにす る｡ここで は 足 は
u‑ 〈JL,T,D)で生成 され る 沢 の部分半群 *)であ る｡ 即 ち 旦‑ くu〉.
*)本稿では単位元 をもつ半群 を単 に半群 と呼ぶ｡
高階古典論理の形式的体系の試作 Ⅰ 67
前節でLog(D)と書 いた ものを,以降Logと書 くことにす る｡ 即 ち Log‑ 〈X ∈足;4,(X,1)‑2).
定数 とは, ここで は
[A IB] (A∈ Log,B∈丑)
の形 の 9tの元で,Aでその品詞 を表 し,Bはコー ドとして使 うことにす る｡ 即 ち,定数全体 をConstで表せば,
Const‑ ([A IB];A∈ Log,B∈旦). 変数 も同様 で,
Var‑ (llA LB]:AE Log,B E A)
としてVarの元 を変数 と呼ぶ｡以下 Syn(合成語全体),Word(語全体), Wdsq(語列全体),wcf(品詞関数).I9t‑釈,phr(句全体)が次のように
して帰納的 に定 まる :
Syn ‑ (lXls];Ⅹ∈ Var,S∈ phr);
Word‑CollStUVarUSyn;
Wdsq‑ 〈Word);
ifAE LogandBEB,wcf(lA IB])‑ A : ifA∈ LogandB∈足,wcf([IA LB])‑A ;
ifx E VarandsE Phr,wcf(lxls])‑wcf(S)wcf(x)JL:
ifnot′∈ Wdsq,wcf(/)‑〟;
wcf(E) ‑E;
ifs∈ Wdsq＼(E〉andα∈ Word,
wcf(Sα)‑AC,ifforsomeA,B∈ LogandC∈里, wcf(S)‑ ABJLandwcf(α)‑ BC∈ Log;
‑〟, otherwise;
phr‑ 〈S∈況 ;wcf(S)∈ Log).
関数 wcfは前節で出て きたS∈ Wdsqの関数 ￠1(S,E)の定義域 を 9tに拡 張 した ものに他 な らない｡前節 の言い方 をすればwcf∈況況JLである｡
X ∈ Bの関数 ￠(X, 1)について も同様 な扱 いがで きる｡
[‑1, ]‑2
とし,沢 の元即 ち [,]の列 を数字 1,2による2進法展開 とみ る｡特 に空列 Eについて は,これ を 0とみ る｡従 って,右辺 で は通常 の10進法 を使 うこと
にすれ ば,
E‑ 0,[‑ 1,]‑ 2, [[‑ 3, []‑ 4, ][‑ 5,]]‑ 6, [[[‑ 7,[[]‑8,･･･
とな る. この ように して',沢 とGt‑〈0,1,2,‑ ･)を同一視 した上で, 関数 ￠(X,1)の定義域 を足か ら 沢 に拡張 し,notX ∈ 里の ときは,値 を E‑0とした ものを,trnと記せ ば,trn∈ 況DtFE,
Log‑ 〈X ∈ 況 ;trn(X)‑]〉
となる｡
2.1.推論.文全体 をSentとすれ ば
Sent‑ 〈6∈況 ;wcf(o･)‑T)
である｡Stsq‑ くSent〉とし,Stsqの元 を文列 と呼ぶ ことにす る｡今,文列
∫, 』に対 して
I'‑ Ill･･･Zl,,
4‑ 41Il1 A 2 Z12 ･ ･ ･A,I',A,+1
となるような
Ill,･･･,Il,, Al,･･･,A,.1∈ Stsq
が ある とき,IlをAの部分文列 と呼ぶ.空列 は任意 の文列 の部分文列 である.
また文列 rは文列 rの部分文列である｡部分文列が文 の とき,我々 はこれ を 部分文 と呼ぶ ことにす る｡
次 に
文 [文列]文 ･･･[文列]文 の形,即 ち
TlIll]61･I･lIl,]o･,
(Ill,･･･,Il,∈ Stsq,61,･･･,6,,f∈ Sent)
高階古典論理 の形式的体系の試作 Ⅰ 69
の形 の 沢 の元 を我 々 は推論 (inference)と呼ぶ｡ これ は次 の ように ｢解釈 で きる｣ ことを前提 としてデザイ ンされ てい る :
｢I11の部分文 たち を仮 定 す る と文 o･lが得 られ,
●●●●●●●●●●●●●●●●●●ナ
1㌦の部分文 たち を仮 定 す る と文 6,が得 られ るな らば ; それ らか ら文 Tが推論 で きる｣.
文列 F l,‑ ･,Zl,は空 (‑E)で あ る ことが許 され,r‑0で あ る ことも 許 され てい る｡ Ilq‑Eの場合,[zlq]6gの部分 は []6qと書 いて も,[]‑
[だか ら l6qと書 いて も同 じことで あ る｡ modusponensとい う推論 は Tl6I⇒ 67 (0･,T∈ Sent)
と書 くことがで きる｡ r‑0の場合,推論 は文 とな るが,文 Iの推論 として の解釈 は
｢前提無 しに文 Iが推論 で きる｣
で あ る｡
2.2.推論の 3変形 ･演轟軍国. まず推論 の3種類 の変形,合成推論 ･部分推 論 ･消去推論 について説 明す る｡
Ⅰ)合成推論. 2つの推論
L ‑7Tq lIll]61･･･[F,]o･,,
x‑V[A l]11･･･[Aq]Tq･･･[As]Ts が あ る とき,
入‑ V [Al]fl･･･[A qIll]0･1･･･[A qZl,]6,･･･[As]Ts
とす る｡この とき 1 は Lを上部,xを下部 とす る Lとxの合成推論 で あ る と い う｡ また文 7Tqは合成 のkeyと呼 ばれ る｡
A q‑ E の とき,｢推論 L,X が正 しけれ ば,推論 九 も正 しい｣ことを認 め るのに異存 はないで あ ろう｡△ q‑Eで ない ときを考 える｡ この とき, Lによ れ ば句を推論 す るのに,前提 として は
rI11 (Illの部分文 たち) を仮定す る とo･1｣,
････････,｢Il,を仮定 す るとo･,｣
しか要 らない｡ところが xの前提 の1つ として 7Tqを導 くのに△ qを仮定 して よいのだか ら,｢o･1‑ ･0･,を導 くのに△qも仮定 して よい｣ とい うのが合成 推論 を定義す る理 由であ る｡
II)部分推論.A l,･･･,A,が それぞれ Zll,･･･,Il,の部分文列で ある とき,
x‑ T [Al]61･･･[A,]6, を
Lエ ア [zll]61･･･[I',]6,
の部分推論 とu う｡ ｢推論 Lが正 しけれ ば,推論 xも正 しい｣ことは, もとも と Lにおいて｢qqを導 くとき,Ilqのすべての部分文 を使 わな くて もよい｣こ とか ら,承認 され なけれ ばな らない｡
ⅠⅠⅠ)消去推論.oTqが Ilqの部分文であ る とき,
x‑flz11]0･1‑ ･[F q̲1]oTq̲1[Ilq.1]qq.1‑ ･[Il,]6, を
L‑ T[Fl]0･1･･･[T,]o･,
の消去推論 とい う.｢推論 Lが正 しけれ ば,推論 xも正 しい｣ことは,Lにお いて [Ilq]oTqの部分が ｢自明な前提｣ となってい ることか ら,認 めざるを得 ないであ ろう｡ また,推論 上か ら消去 を繰 り返 して得 られ る推論 も ェの消去 推論 と呼ぶ ことに しよう｡
少 し例 をみる ことにす る｡
L(0･, I,V)‑⇒ 0･vl⇒ 0･Tl⇒ TV
≪三段論法≫
x(6, I)‑ ⇒ 0･T [0･]T
≪⇒ 導入≫
(6, I,V∈ Sent),
(o･,f∈ Sent),
高階古典論理 の形式的体系の試作 Ⅰ
^(o･)‑ 6l⇒ T o･
≪T除去≫
とす る｡
^(I)‑ IJ三二J
を下部,
L(T,.o･,I)‑ ≡ユJ l∋ T o･l∋ 61
を上部 として合成推論 を作れ ば,
Tln 6l⇒ o･T.
この推論 の上部 に
x(T,o･)‑ n o'[T]o･
を合成 すれ ば,
f[T]o･l ∋ o･T.
この部分推論 を とって
71
(♂∈ Sent)
[T]♂
=>T ql=>67 l⇒ T I
一r 方(0･,I)‑ 石 o･l⇒ o･T
即 ちmodusponensが得 られた｡ これ を図 にすれ ば右上 の ようにな る｡ また x≪⇒ 導 入 ≫ と 7r≪modusponens≫か ら
=>=>6 =>fV =>7 =>0'V
が次 の ように して得 られ る :
1. ⇒ ⇒ 6⇒ TV ⇒ 1 ∋ の′[⇒ 0･∋ TV ]⇒ f⇒ 飢′
2.う で ⇒ 0･V[T]∋ の ノ
蛋‑x(∋ o･⇒ TV , ⇒ 1 ⇒ 飢/)≫,
≪‑x(I, ⇒ のノ)≫, 3. ⇒ ⇒ o･∋ TV う で ⇒ 0･V[∋ 0･⇒ TV l]⇒ 0･V ≪1.と2. の合成≫,
4. ∋ の′[♂]γ ≪‑ 〟(♂,γ)≫, 5.⇒ ⇒ o･⇒ IVう で ∋ 0･V[⇒ 0･⇒ TV 1 O･]V ≪3.と4.の合成≫,
6.vl石 う でV ≪‑ 7T(1,V)≫,
部 はkeysentence.
7.⇒⇒ 6⇒ TV⇒ 1∋ 0･V[⇒ 6∋ TV I O･]JT[⇒ 0･⇒ TV T 6]∋ TV
8.⇒⇒ 6⇒ TV⇒ 7⇒ 0･V[∋ 6∋ TV 7 9.⇒ TVl6J⇒ 6⇒ TV
10.⇒⇒ o･∋ TVゴ ア⇒ 0･V[⇒ 6⇒ TV 7 Ttノ
ll.=>=>6=>TV=>7=>0'V
図 にす る と,右下 の ようになる｡ 図式 の中で極上部 にある文 は左隣 りか文 の 位置 よ り下部 の [ ]内 に同文が ある
とき消去 で きる｡ この ような図 を演揮 図あるい は証 明図 とい う｡
ここで演揮 図 とは何 か を定義 してお こう｡ 1)推論
TlTl]61･･･[Il,]o･,
が ある とき, これ に対応 す る図式
≪5.と6.の合成≫, 6]∋ IV ≪7. の消去推論≫,
≪‑ 2t(6,⇒ TV)≫, 6]6[∋ 6⇒ TV T 6]⇒ 0･∋
≪8.と9.の合成≫,
≪10.の消去推論≫.
消去 消去 l6 l⇒ o･∋ TV
[7]⇒ 6V
[∋ o･⇒ fV]⇒ T⇒ 6V
=>=>o'=>TV=>T=>6V
[rl]61･･･[zl,]o･,
7{
7T
〟
〟
〟
1
は演揮 図である｡[Ill]0･1,･･･,[11,]6,をこの演揮 図の極上部前提 とい う｡
極上部前提 には左 か ら順 に順位 をつ けることがで きる｡ 2)A が演揮 図で, A の極上部前提 を左 か ら順 に
[Al]11,･･･,[Aq]Iq,･･･,[As]Ts
とす る. この とき推論 7Tq[rl]61･･･[I',]o･,が あれ ば,Aの極上部前提[Aq]
1gの上 に図形
[I11]61･･･[Il,]6,
をつ け加 えてで きる図式 A′も演揮 図で ある｡演揮 図 A'の極上部前提 は左 か ら順 に
