高階古典論理 の形式的体系の試作

高階古典論理 の形式的体系の試作

兼 岩 龍

前 回 までの 目次

1.

( 無題)

形式的体 系

2.1

推論

2.2

推論 の

変形 ･演鐸 図 2.3 語列への定数,変数 の関連

( 以上 第

輯

2.4.

標 準木 .サブセ クシ ョン 2.2‑3において,演揮 図 ･構造図が定義 さ れた｡ そ こで上部,下部,極上部 な どの言葉が現れたが, それ らの意味 は浜 鐸 図 ･構造 図 を実際 に図 に書 いた ときは視覚的 に理解 で きるであ ろうが,釈 の元 として演揮 図 ･構造 図 をみる とき必 ず しも明快 とはい えないで あ ろう

ここで その ことに触 れてお こう

丑 ‑

^{J L ,T, D}

^{J L ,†,J〉 ) の元}

IT‑ Xl･･･X,(X

l ,･･･

が条件

1)Ⅹi(の ∈ (

† ;∫)

2)Xq

‑ †な らば

1 ,･･･ ,r) ,Xo

を満 たす とき,〟 は標準木

であ る とい う

また

Xl

,･･

の中に出て くる 〃 の個数 を標準木

の位数 とい う

空列

は位数 0の標 準 木で あ る

今,

変数 関数

現

p

Lを

ex(X,0) ‑E:

ex(

x

十

沢,

‑ex(X,Y),otherwise

で

況

L D

Lを

exx(X,0) ‑ E ;

exx

( X,Y

Z

Z

ex(X,Y+1)‑ ex(X,Y)Z

で定義す る. X が

の とき

( X

は

を

の列 と考 えた ときの第

番 目の

である.従 って,

H

l ,･･･

な ら

exx

( H

X

( 1 ,･･･

‑E,otherwise

で あ る｡ また

が 語 列 の と き

( i

は 日にお け る第

番 目 の語,

( i

は第

番 目までの語 を順 にな らべてで きる語列である

次 に,関数

況

F L

況D

F L

〝

Lを

E

ifXE Prng,

plength(X)‑minmum ofpsuchthatX ‑ ex(X,p);

ifnot(X E PrngandYE Pprng),app(X,Y,Z)‑0:

ifX E PrngandYE Pprng,app(X,Y,0)‑0;

if

X

Y

app

( X,Y,Z

q>app(X,Y,Z)andexx(X,q)^‑ Y

,

‑plength(X)+1,otherwise

で定義す る

が

の とき

は

を

の列

と考 えた ときの長 さである｡

Iが標準木 の とき

( H

J J

は

の元 の 列 としての

の中で第 ♪番 目の

が第何番 目に現れ るか を表 してい る

た だ し少が ∬ の位数 よ り大 きい ときは

app(

〟

〟

( の

となるように定義 してある

また標準木

の位数 は

orde

r

で定義 され る関数

況

を用 いて

( l l ) で表 され る

ここに

は

X ェ Y

X ‑ Y,i f X

Y ;

‑0,otherwise

で与 え られ る もの とす る｡しか しなが ら,上記 の

の定義 において

gth(Ⅹi(X)

)が

を越 える ことはない｡

さて今,位数

の標準木

Iが与 えられ ると集合

1 ,‑ ･

にある種 の 順序が導入 され る

即 ち p

1 ,‑ ･

に対 して , Pが

の下部 にあ

る ( また は

が pの上部 にある) とは,

ex(

H

H

H

/ L

)

†

J,

Ⅹi(Ⅳ )∈ (

I ;J)

app(l

l

F E

I

J L

<

となる

足,

沢 が存在す ることをい う

この とき †

Jは

の 元 の列 として

の一部分 であるか ら

exx(W,q)

‑

が成立 し

もまた標準木でなけれ ばな らない｡

Nt

を標準木全体,即 ち

Nt

‑i H

B ;

I ;J)

Dt,

‑

とす る.また

況 ( 況F E )3 ‑ 況 況 p 況 F L 況J Jを｢ 標準木

1において Pが

即 ち,値

H , P

を

か

つH

において Pが

lowe

r

H , P

1,

forallr∈

訳

H , P

H

が成 り立 つ とき,

において P は

の親

u pの子)とい う

H

^{A, Yの}

3

変 数 述 語

に お い て P は

の 親 で あ る｣ の 特 性 関 数 を

∈

釈 (

.とす る

次 に

Tにおいて P は極上｣( 特性関数 :

況 (

を定義す る

∬

において カ は極上, とは

〝

∈

forallq

∈ gt

H , P

,

exx(

〟

〟

〟

十

〟

〟

〟

≠ †∫

が満 た され る ことをい う｡言い換 えれ ば

が標準木 で , 少が上部 ( 或 い は子) を もたず,

の元 の列 H において 9番 目の

Lのす ぐ後 ろに列 †Jが現れ な い とき

〟

の値 を

とし, そ うでない ときは 0とす るのである

演揮 図全体 を

としよう｡即 ち,く

の元

で

† ;J)

とサブセ クシ ョン

の条件

を満 たす ものの全体 を

とす る

関数

∈ 況

を定義 してお く

即 ち

muchange

( X)

X

X ∈ 日 ,J〉;

‑〟,otherwise, ifnot

X

i ( X)

pi(E)‑E;

ifX E (Radical)andYE Radical, pi

( XY)

( X)

Y).

この とき,A

な らば

は標準木であ る

即 ち,

さ らに

pi(Ddctm)‑ 〈∬ ∈ Nt;

ex(

〟

〟†

〟

)‑ 1〉

が成 り立つ

が清輝図の とき

を浜揮 図

の型 とい う｡また関数

∈ 況沢

ifnotX E (Radica12),pi2(X)‑E,' pi2(E)‑E;

if

X

Y

( XY)

( X)

Y).

で定義すれ ば,

pi2(Strm)

‑ (H

exx

(

‑

(

となる

A が構造 図の とき p i 2( A) を構造図

の型

とい う

次 に関数

現

lchange(X)‑E

,i f X ∈ 日 ,J〉;

‑LrX],otherwise, ifnotX E (Radical),list(X)‑E;

list(E)‑E;

if

X

Y

l i s t( XY)

ifnotX

E

list2(E)‑E;

i f X

Y

list2

( XY)

( X)

Y)

で定義す る

が演揮図の とき

を,

'が構造図の とき

' )を それぞれ

,

'の内容

とい う

例 えば,

A‑^{7日 ∋} T^l†

J⇒

の とき,演揮図 A の型 は

1 2 3 3

pi

(

‑J

†j

†

† JJ J JL

1 2 3 4 5

he

h t: 0 1 2 3 2

の内容 は

list(A)‑ [1][1∋ Tl][l⇒ T6][[T]o･][

l∋

となる.

6

T^,=>∈ Const;

wcf(T)‑T,wcf(

ラ)

とす る

この例 において,標準木

にお ける ( 親,千,･･･,チ) の組 をすべ て書 き出せ ば,

(1,2)

,

,

となる

一般 に標準木

i

にお ける ( 釈,千,･･･,千)の組 の

つを (Y, X

･･

,X

( ただ し Y は

において極上でない もの, Xl < ‑ ･<

,は Y のす べての子) とし, これか ら

o T q

か ら左端 の [と,右端 の] を除 いた もの),

1 ‑ (exx(list

( A) ,Y) か ら左端 の [と,右端 の]を除 き, もしその冒頭 に [ 文列] の形があれ ばそれ も除いた もの)

とおいて列

O ･ 1‑

･ ,を作 ることがで きる. この操作 を,標準木

に お ける ( 親, 千,･‑ , 千) の組 ( 家族

とい う) のすべてについて 行 えば,演揮 図 A に使 われたすべての推論 を得 ることがで きる.この例 につ

いていえば,家族

(1,2)

,

,

に対応 す る推論 は, それぞれ

I

l⇒

7, ⇒

とな り, これ らが演緯図 A に使 われたすべての推論

の使用推論 とい う)

である

また この例 で

において極上 な るもの は

と

である｡ これに対応 して

の極上部前提 は (

か ら左端 の [と,右端 の]を除い た もの )

♂ と(

か ら左端 の [と,右端 の] を除いた もの )‑ l⇒

Tの

つで ある.一般 に

が演揮図

の極上部前提で あ るための条件 は

α‑ (exx(list(A ),P)

か ら左端 の [と,右端 の] を除いた もの) かつ

において Pが極上で あるような

沢 が存在す ることである｣

が

の元 の列

に含 まれ る †の数 に関す る帰納法で得 られ る

今

において極上 な るもの Pが与 えられ る と,その親 その親 と辿 っ て親 を もたな くなる まで遡 ることがで きる

そ こでそれ らの数 を逆 にな らべ

( 〜,･･･

とす るQ ここに

)鞄 は親 を もたない,

1 ,･･･

)に対 して

は

uq̲1

の子, 3)

‑ Pが成 り立 つ もの とす る

一般 に標準木

において

‑ 3

)が満 た され る とき( 狗,‑ ･

を

にお けるPの系譜

とい う. さらに

1 ,･･･ ,r)に対 して

αq‑ (exx(list(A ),uq)

か ら左端 の [と,右端 の] を除 いた もの),

p q‑ (exx(α^q

,1 ) か ら左端 の [と,右端 の] を除 いた もの) ,

γ‑ (α,∈ Prng

か ら冒頭 の

を除 いた もの),

♂‑ ♂(♪)‑ [A

･･

の様 にして前提

を作る ことがで きる

i

において極上 な るものが 小 なる順 にPl ,･･･, Psの とき

8‑ (exx(list(A )

,1 )か ら左端 の [と,右端 の] を除いた もの) とおいて,

conclusion(A )‑ e 6(Pl)

･･

を作れ ば, これ は演揮 図 A の最終合成推論 ( 結論 とい う)である

例

^ ‑

7

^⇒

^{f† I⇒}

^q

でいえば

と

の系譜 はそれ ぞれ

,

で,

6‑

1,

6( 5 )

6

conclusion(A)‑ TlT]6l ラ

67

とな る

もう 1 つの例

^ ‑ うう o ･ ⇒

Vう で⇒

V†[ ⇒

⇒ T⇒

V

†[

6]

l⇒ 6∋

VJJJJJ についてい えば,

list(A)

‑ [ ⇒⇒ o ･ ⇒

V

T⇒

[[ ⇒ 0 ･ ⇒

⇒ T⇒

[[7]

⇒

J

[

^F ⇒

1

2

3

1

pi

( A

‑

† f L †

FE † J L

F L

∫ J

1 2 3

56 78

0 ^{1 2}

で

にお ける家族 は

(1,2),(2,3),(3,4),(4,5,6)

,

極上者 の系譜 は

(1,2,3,4,5)

, ( 1 ,2, 3,4,6, 7), ( 1 ,2,3,4,6, 8);

A

の結論 は

conclusion(A)‑ ⇒ ⇒ o･⇒ Ty ⇒ f ⇒

0 ･ y[⇒

ア

[ ⇒ o ･ ⇒

⇒ o ･

⇒ 0 ･ ⇒

となる｡一般 に推論 上か ら消去推論 に よって ｢ 無駄 な前提｣をすべて取 り去 っ た もの を

で表せ ば, この例 の場合,

simp(conclusion

( A) )‑⇒

o ･ ⇒

V∋ f⇒

とな る

また例 A ‑ o ･†Jについてい えば,家族 は( 1)のみ,極上者 はない｡従 っ て,使用推論 は o ･のみ,結論 も

6 とな る.

標準木 H にお ける家族 ,標準木 H にお ける Pの系譜等 は gtの元 の組 ( 狗,･

^{9 t)}

で あ るが, これ を再 び 沢 の元 として扱 うことは容易 であ る.我 々 は

(狗,･

･･, ur )

[

I; ^J

(

^{･ ･}

^†

と定義

に

例

ば

( ^{0 ,}

^[

^J]

‑

[ ]

[[ ^] ]

‑ 4･

1

+ ²

0･ ² 8

78

‑

3

5

である

語列 における原始語 の真 の関連 について も触 れてお こう

^{｢ 語列}

^において

原始語

q 番 目で真 に関連 す る

を言い換 えれ ば ｢

1)

2)exx(list2(lambda

( i ))

3)pi2(lambda(i)

kお ける

の系譜 を

ul ,･･･

とす る とき

≠ [

exx(list2(lambda

( i ))

+

が成立 す る｣ となる｡

語列

において真 の関連 をす る原始語 を

の元 の列

( i )の 中で出て くる順 に ( 1度 出て きた語 は次 に リス トア ップ しない)

α1

ナ●●●

とす る とき列

α1

･･

を

( i )で表す ことにす る

が語列で ない ときは

( i ) ‑E

と約束 す る.また語列

( t )の中の定数 だけを選 び出 して作 った部分語列 を

C( i ),変数 だけを選 び出 して作 った部分語列 を

で表す こと にす る｡我々 は部分文列,部分文 をサブセ クシ ョン

で定義 したが, これ

と同様 に

を定義す ることがで きる｡ ここで

は語列 の

をそれぞれ部分語列,部分語 と呼 ん

でいる

語列

と語列

( i )の部分語

について

において

る番号 を順 に

,･･･

,とす るとき組

(

〟1 ,･･･

を

( i

で表す ことにす る

が語列でない場合や,

( i )の 部分語でない場合即 ち,

not

(

andforsomeq

∈ 沢

( i )

の場合 は

i , α)‑E と約束す る

例 をみよう,

t

l…

の とき,

lambda

( i ) ‑ラ

†…

pi2(lambda

( i )

list2(lambda

( i )

‑ [ ⇒]

][ ∃]

[Iy

][ …][

( i )‑ 3 >

j=･ ,

list21

C( i )

ラ

∃≡･ ,

( 〜 )

α

ラ .>

∃ ≡ .

となる

標準木

1にお ける

の高 さ

につ い て も述 べ て お こう

高 さ

H

を以下 に定義する :

ifq‑0ornot

H E

if∬ ∈ Nt,

lheight(

H,q+1

l

,i

H,q+1

‑1height(

H

H,q+1) ‑

‑ lheight

(

heigh t

( H,q)

( H

( H

j L

この とき次 の定理 が成 り立 つ ( 証明 は容易であろう):

定理

標準木

1において Pが

の親

が pの子)であるための条件 は

1)0<

^P

≦ or der( H)

2)

( H

( H

+1 ,

3)

p < r

な らば

(

(

,r) が成 り立つ ことで ある｡

このサブセ クシ ョンの最後 として,標準木 と ｢内容｣か ら浜揮 図,構造 図 を再生 させ る関数 を導入 してお く｡ まず 自然数

gtの [と]による

進 法展開 の長 さ

length(X)‑ (minimum ofq∈ g^{tsuchthatX+2≦2q)‑ 1}

とな る

に対 してその一番外側 の [ ] を取 り去 って得 られ る

( X)

core(X)‑ quot(X ‑ 2'ength(X⁾エ 1ェ 2,2)

と表せ る

ここに

quot(Y,Z)‑ (minimum ofq∈ 況 suchthatZ･q>Y)‑i1,

ifZ≠0;

‑ 0,ifZ ‑ 0

即 ち y

を

で割 った商 ( ただ し

の ときは

を

y

とす る

また

沢 に対 して,

,

とな るような

沢 がただ

つ 存 在 す る の で, これ を

と表 す こ とにす る. そ こで

D t(

を以下 の ように帰納的 に定義す る :

( X

Y

order(X)‑ plength(Y)),

comp(X

,Y)

ifX ∈ 旦 andorder(X)‑0,

comp(X,E)‑ X :

ifX ∈ A and

Y

〉

order(X)^‑ plength(Y)>0,

comp(X,Y)‑

comp(ex(X,app(X,

p

^{) ‑}

^‑

, J L

Y' )

, J L

,

whereX^′‑coex(X,app(X,

p

Y'

Y

‑ 1 ).

このようにすれば,

が演揮図,

'が構造図の とき

,

)

,

が成立す る

2.5.

代入.

を語列

を原始語

Sを

となる純正句,

( i

,･･･

,

,

1T‑pi2(lambda

( i )),

,

vq‑ app(

H

F L

( 1,･･･

, とす る

そこで関数

況 (

を

ex2(X

, p

, p)

で定義 し,

H2‑eX(H,V1‑i1)^H leX2(H,vl,V2‑ Vl

エ 1

････ex2(1

T

H

,

, L

L

( L

L

････ex2

( L

1

L

X( L

とす る

この とき

, L 2) を

( i

で表 し,代入

lt]la]

l s]

の結果 とい う｡特 に

i

の ときは

( t

a

とす る｡この ことは r‑ 0の とき u

‑ 0

‑ 0と約束 してお け ば,特 にいわ な くて も自動 的 にそ うなる

また

(*) tE WdsqandaE PrimitiveandsE Pphrand

wcf(S)‑wcf(a)

が成立 しない ときは

( i

α

としてお く｡ この よ うにすれ ば

∈ Dt(況JL)3

とな る

ここに

は純正句全体 とす る.我 々 は ｢(*)が成立 すれ ば,

sub

( i

( i ,a

f( i )

が成立 す る｣ ことを確 かめる ことがで きる

X

が代入

で＼ ある とは

が集合

Subst

‑ ( X

( X)

core(exx(X,2))E Primitiveand

core(exx(X,3))E Pphrand

wcf(core(exx(X,2)

)

の元 であ るこ とをい う

代入 [ t ]

[ S] ( i

α

S

が適正

であ る とは,

が

に真 に関連 しない｣か また は 2)

が

番 目で

に真 に関連 し,

,

u,)

が標準木

( i ) )にお ける

の系譜 で,

が

に真 に関連 す る変 数 で

( 1,･･･

1)の ときは, いつで も

exx(list2(lambda(i))

,up )≠ [

で ある

が成立 す る ことをい う

例 をみ よう ｡i‑

l…

の とき,

51

‑ [ t ]

5 2

‑ [ t ]

23‑[

t ]

[

2 4

[ t ] [ ･ ][

] ,

55‑[t]

[ ･ ]

l十 十

26

‑ [ t ] [ ･ ]

2 7

‑ [ t ] [ ･ ] [ …]

とすれば,

であるが

は

の元 で はない｡ また

の うち

と

を除 けば適正で あるが,

と

は適正で はない｡

sub2

( X)

( X

core(exx(X,2)),

core(exx(X,3)))

とすれば,

sub2(∑1)‑∃[y^{l …} ･yy+Xz],

S血2(∑2)‑∃[yI^… ･yy+Xy],

sub2(E3)‑∃[y^{l …} ･yyx]‑i,

S血2(三｡)‑∃[yI

^≡

sub2(25)‑∃[y^l…[

XI

l

sub2(26)‑∃[y^l…[

Ⅹt[

J++

sub2(∑7)‑E

となる

2.6.

高階古典論理

の公理系.今 までの議論 で

つの形式的体 系 を与 える準備がで きた｡ ここで

なる体 系

‑ 公理系 を導入す る

ま ず若干 の定数 を予約 してお く｡即 ち,

T ‑ [ T IT] ,⊥ ‑ [ T ID] ,> ‑ [ TTJ J T〟 lTT]

… (A)

‑ [ TA pAF El]( A

⇒ (U)

‑ [ TU J L

p I J L ]( U

とす る｡ ここに

は述語 品詞 の全体 で

Plog

‑ (U

exx(U,i

で与 え られ る もの とす る｡ また

= = =^(D)I〜 =^{= (T)}

^I

^>

としてお く

1

)等号公理 . S, i ,uを品詞

の純正句 とす る とき,

equZ(S,i)^{‑ I (}A)tSI=(A)St,

equ3(S,i^,

u)

) t ^u

とす る

l

は引 き数が同品詞 の純正句でない とき,値

を とる関数である｡集合

Equ‑ (equl(∫);∫∈ Pph

r

(equ2(S,i):

S

E

,

(equ3(

S

i

S

i

,

‑ wc f( i )‑ wcf( u)) の元 は

の等号公理 であ るといわれ る｡

2)

順序公理 . f

, hを品詞 U の純正述語 (U

とす る とき,

/

‑

L

^l

ord2

( ′

ニ

^l

^f,

ord3

V

‑

,

/

‑

とす る｡ これ らが作 る集合

の元 は

の順序公理 であ るといわれ る

3

)等号導入公理. S

を品詞 AC

Lの純正句,Xを品詞

の変数 ( A ,

とし,Xは S,

に真 の関連 をしない もの とす る とき,

equin(S,i,Ⅹ)‑ ≡(ACP)SiI≡ (A)SXtX

としこれ を HL の等号導入公理 と言 う｡ HL を設定 す る際 に想 定 した解 釈

の標準解釈,第

節参照)によれ ば

S

は ｢ 集合

か ら ｢ 集合

へ の ｢ 関数｣で, この公理 は ｢ 集合 C の不特定 の元

について各々の ｢ 像｣

s

x ,t x が ｢ 等 しい｣ことが言 えれ ば

S, t が ｢ 関数 として等 しい｣ことを主

張す る ものである