finding a pattern of the infinitely long tableau. In order to transform the

査読論文

K4 タブローによる 妥当性判定と濾過法

高木 翼

� https://orcid.org/0000-0001-9890-1015

法政大学 文学部 哲学科

〒 102-8160東京都千代田区富士見 2-17-1

2019年 1月 26日原稿受付

Citation :高木 翼 (2019). K4タブローによる妥当性判定と濾過法 . Journal of Science and Philosophy, 2(1), 4–23.

Abstract

One of the diÿculties of modal logic K4 is that the tableau may be infinitely long and the validity of a formula cannot be determined.

However, an infinite counter-model of the formula can be constructed by

finding a pattern of the infinitely long tableau. In order to transform the

infinite counter-model into a finite counter-model, we should suppose

that reflexibility holds in the part of the same infinite prefixed formula

except for their prefixes. In this paper, I show that this transformation is

the special case of filtration method.

2 K

1 はじめに

タブロー法は論理式の妥当性の判定手続きであり

, 1950

Beth (1955)

Hintikka (1953, 1955)

,

Smullyan (1995)

,

,

(1976);

(1987);

(1995);

(1964);

(1999);

(2000),

, Fitting (1983, 1996); Smullyan (1995); d’Agostino (1999); Priest (2008)

タブロー法における一つの困難は

,

K

,

K4

,

,

,

,

,

(filtration method)

2 K における冠頭タブロー

§2

, Fitting (1972)

,

る様相論理式の妥当性を判定するタブロー法を紹介する。

空ではない正の整数の有限列

σ

(prefix) ,

ϕ

σ : ϕ

(prefixed formula)

, σ = (n

, n

, . . . , n

, n

)

σ

= (n

, n

, . . . , n

, n

)

,

(n

, n

, . . . , n

, n

, n

. . . , n

, n

)

σ.σ

, l = k + 1

σ.σ

σ.n

冠頭部

σ

,

n

σ.n

σ

/ / / /

名前の可能世界から到達可能な可能世界の名前を表している。この記法を 用いることによって

,

, σ = (n

, n

, . . . , n

, n

)

/ / / /

n

(n

, n

) (n

, n

, n

) · · · (n

, n

, n

, . . . , n

)

,

σ : ϕ

σ

ϕ

, σ : ϕ

, ϕ

σ

W

, R

W

, V

, M = (W, R, V)

Kripke

,

| =

, χ

, pre( χ)

χ

, w

∈ W

(serial)

,

w

∈ W

w

Rw

,

I : pre ( χ) → W

(interpretation)

, I(σ)

,

n

I (σ)R(I (σ.n))

,

σ : ϕ

Kripke

F = (W, R)

(satisfiable)

,

Kripke

M = (W, R, V)

(M, I(σ)) | = ϕ

, σ : ϕ

Kripke

F = (W, R)

(valid)

,

Kripke

M = (W, R, V)

(M, I(σ)) | = ϕ

1 : ϕ

1 : ϕ

(prefixed tableau)

2 K

α

β

ν

π

σ : α σ : β σ : ¬¬ϕ σ : ν σ : π

σ : α

σ : β

σ : β

σ : ϕ σ.n : ν

σ.n : π

σ : α

ただし

,

• ν

σ.n

,

• π

σ.n

,

とする。また

,

,

,

α, α

, α

, β, β

, β

, ν, ν

, π, π

1

2

α α

α

β β

β

ϕ

∧ ϕ

ϕ

ϕ

ϕ

∨ ϕ

ϕ

ϕ

¬(ϕ

∨ ϕ

) ¬ ϕ

¬ ϕ

¬(ϕ

∧ ϕ

) ¬ ϕ

¬ ϕ

¬(ϕ

→ ϕ

) ϕ

¬ ϕ

ϕ

→ ϕ

¬ ϕ

ϕ

1 α

β

ν

σ : ν

σ.n : ν

, π

σ : π

σ.n : π

,

まず

, π

, σ : π

,

ν ν

π π

ϕ ϕ ^ ϕ ϕ

¬ ^ ϕ ¬ ϕ ¬ ϕ ¬ ϕ

2 ν

π

うな

M = (W, R, V )

I

,

I(σ)R(I(σ.n))

I (σ.n)

σ.n : π

, π

,

R

I(σ)R(I(σ.n))

σ.n

π

ϕ

, σ.n

ϕ

,

π

σ.n

,

, ϕ

, σ.n

π

次に

, ν

, σ : ν

,

M = (W, R, V )

I

, I(σ)R(I(σ.n))

I(σ.n)

σ.n : ν

, ν

,

R

I(σ)R(I(σ.n))

, π

,

I(σ)R(I(σ.n))

, ν

σ.n

ν

π

σ.n

, σ.n

ν

冠頭タブローの枝が閉じるとは

,

ϕ

, σ : ϕ

σ : ¬ ϕ

,

7

,

,

冠頭タブローの枝が完成するとは

,

,

,

3 K

,

,

1 : ¬ϕ

,

ϕ

例

2.1

(ϕ → ψ) → ( ϕ → ψ)

1 : ¬( ⇤ ( ' ! ) ! ( ⇤' ! ⇤ )) 1 : ⇤ ( ' ! )

1 : ¬( ⇤' ! ⇤ ) 1 : ⇤' 1 : ¬ ⇤ 1, 1 : ¬ 1, 1 : ' !

1, 1 : ' 1, 1 : ¬ '

7

1, 1 : 7

<latexit sha1_base64="NPE+46XEeHXygN0dakDU4YWqUxU=">AAAHrXiclVNLb9NAEJ42QIp5tIULEpeIpqiV0nSTNKVUKiqFAxKXvtJWikPlOJvErWO7a+fRWv4D/AEOnEDigPgZXPgDSPTOBXEsEhcOzK6dR93gCltez8583zezs7tlS9dsh5DTkdHYlavX4mPXpRs3b90en5i8s2ObTabSgmrqJtsrKzbVNYMWHM3R6Z7FqNIo63S3fPiMx3dblNmaaWw7xxYtNZSaoVU1VXHQtT85+l0uytuMUqmYdpOZZdmgtRl5zezMyC2FWXVNZlqt7iiMmW3ZsrXZgbnADYFxL4fOJj0pgbIyM8wKde1m+SDjiSQR+kkvIcuJwUoiMvAEoQzZXoaAd06wyxTEhFhyKoj0vCHBnBeAhtab9HxOiLRwntRDhWB5b6CAwXLlTkNhh11SaSh5sUsWZfyT5f/EyAf8SlJJQpJNHZcfm7ZWceorJJ23nJRYl62d0JUFy/G6KMWo6fTpSmaJpIS5xk2MGqraZC3qzj3xurvrd+xiKOsFfQlrPu5r5oZp5rygUyFiLt8j5iN4ixgqSfsTUyRNxJO4aGQCYwqCZ92cHPkGMlTABBWa0AAKBjho66CAjW8RMkDAQl8KUS3Q0K5AFZEdKIELB4hRgGFcEywKHkio2EQ/RayC3kMcazgr4tdBHxV4rkeR0UQfFVomeqsRfBd5VLCq+Jqi0qhsvtfAOV+XLXKoyNPxY8hMwDT5Sj6SM/KFfCI/yJ+IzFyD9+MY/2WfS6398df3tn5fymrg34F6nxVZM+/BkqhVw9ot4eGrUH1+6+TN2dby5rT7kLwnP7H+d+SUfMYVGK1f6ocNuvk2oh4DxzbqdYRm55L+tcTO1nCn/DXoYn8Zds8KutnX669RilAcdoLmoSCwDMd5jDZwfI452qjOd0pBNI+UEV9BbgfmRH4HGZpQtyPPTBg7JxQr/8WJwh4JJI08+VxRC51Zv3f8PDZE9wysyUW/30uGXE/MK+Ic1NDO4+uBh3c8E77RF42dbDqTS2c3slOra8FtH4P78ABm8EY/glV4AevYeTX2MnYUO4m58fl4IS7HX/nQ0ZGAcxfOPfHaXx1dAgw=</latexit>

ただし

,

,

,

3 K 以外の様相論理体系における冠頭タブロー

§2

R

K

K

,

ν

,

ν

, ν

, ν

• ν

σ

I(σ)R(I(σ))

• ν

σ.σ

I (σ)R(I (σ.σ

))

• σ

σ

2

, ν

σ

I(σ)R(I(σ

))

• ν

σ

I(σ.n)R(I(σ))

ν

ν

ν

ν

σ : ν σ : ν σ : ν σ.n : ν

σ : ν

σ.σ

: ν

σ

: ν

σ : ν

ただし

, ν

ν

, ν, ν

2

ν

, ν

, ν

, ν

, ν

ν

,

• τ

B

τ

:⇔ τ

= σ

τ

= (σ.n) ;

• τ

B

τ

:⇔ τ

= σ

τ

= σ

I(τ

)R(I(τ

)) ;

• τ

B

τ

:⇔ τ

= σ

τ

= σ.σ

I(τ

)R(I (τ

)) ;

• τ

B

τ

:⇔

2

τ

= σ

τ

= σ

I(τ

)R(I (τ

)) ;

• τ

B

τ

:⇔ τ

= σ.n

τ

= σ

I(τ

)R(I(τ

)) ;

様相論理体系

T

R

,

ν

,

KB

R

,

ν

/ / / /

** jj =

O E

3 K

,

,

K4

R

,

σ

σ.σ

ν

,

,

,

/ / / /

n

(n

, n

) (n

, n

, n

) · · · (n

, n

, n

, . . . , n

)

,

K

, §2

,

σ = (n

, n

, . . . , n

, n

)

,

σ

,

ν

,

θ

σ.n

,

σ

θ

ν

, θ

σ.σ

, σ

σ.σ

θ

,

,

pre ( χ)

(strongly generated)

,

n

(σ.n) ∈ pre ( χ)

σ ∈ pre ( χ)

最後に

,

w

Euclid

R

w

, w

, w

, . . .

,

,

2

σ

σ

ν

* *

•

•

•

w₂ O E w₃ w₄

w

•

従って

,

K5

ν

,

, w

,

論理体系

KT5

S5

, w

, Euclid

,

w

,

, S5

4 完全性定理

§3

,

,

,

,

,

例

4.1 ^ ϕ → ^ ϕ

K4

,

¬( ^ ϕ → ^ ϕ)

K4

,

1 : ¬(^ ' ! ^⇤' ) 1 : ^ ' 1 : ¬^⇤'

1, 1 : ' 1, 1 : ¬ ⇤' 1, 1, 1 : ¬ '

1, 1, 1 : ¬ ⇤' 1, 1, 1, 1 : ¬ ' 1, 1, 1, 1 : ¬ ⇤' 1, 1, 1, 1, 1 : ¬ '

.. .

<latexit sha1_base64="(null)">(null)</latexit><latexit sha1_base64="(null)">(null)</latexit><latexit sha1_base64="(null)">(null)</latexit>

このように

, 1 : ¬( ^ ϕ → ^ ϕ)

そこで

, Hintikka

,

成するということを再定義する。

4

S

Hintikka

,

(1)

p

, p ∈ S

¬p ∈ S

(2) σ : α ∈ S

σ : α

∈ S

σ : α

∈ S ; (3) σ : β ∈ S

σ : β

∈ S

σ : β

∈ S ; (4) σ : ¬¬ϕ ∈ S

ϕ ∈ S ;

(5) L ∈ {K, T, 4, 5, B}

τ

: ν ∈ S

, τ

B

τ

τ

∈ pre(S)

τ

τ

: ν

∈ S ;

(6) σ : π ∈ S

,

(σ.n)

σ.n : π

∈ S.

このとき

,

,

理式が

Hintikka

Hintikka

頭タブローの規則を適用することで構成されていくが

,

,

Hintikka

,

,

Hintikka

補題

4.2 (Hintikka

) Hintikka

S

証明 それぞれの冠頭論理式に含まれる論理結合子の数に関する帰納法 によって示す。まず

,

p

, σ : p ∈ S

,

σ : p < S

I(σ)

p

V(p, I(σ))

, S

,

0

, Hintikka

α ∈ S

α

∈ S

α

∈ S

,

α

α

,

| =

, α

, β, ¬¬ϕ, ν, π

冠頭タブローの枝が充足可能であるとは

,

,

,

θ

, θ

Hintikka

まれ

, Hintikka

Hintikka

可能であることが分かるので

, θ

,

定理

4.3 (

) 1 : ϕ

ϕ

る証明が存在する。

証明 長くなるので割愛する。詳しく知りたい読者は

Fitting (1983)

Theorem 6.2

5 反例モデルの構成

定理

4.3

,

1 : ¬ ϕ

1 : ¬ ϕ

,

,

1 : ¬ ϕ

1 : ¬ ϕ

,

1 : ¬ϕ

Kripke

M = (W, R, V) ,

ϕ

だろうか。

θ

σ

: ϕ

, . . . , σ

: ϕ

,

V (ϕ

, I (σ

)), . . . , V(ϕ

, I (σ

))

V

, θ

例えば

, 1 : ¬( ^ ϕ → ^ ϕ)

4.1

σ

, σ

/ /

/ / 7 +//

• • •

5

冠頭部 論理式

1 ¬( ^ ϕ → ^ ϕ), ^ ϕ, ¬ ^ ϕ

1, 1 ϕ, ¬ ϕ

1, 1, 1 ¬ϕ, ¬ ϕ

1, 1, 1, 1 ¬ϕ, ¬ ϕ . .

. . . .

この場合

,

θ

σ

S

, S

= S

= S

= · · ·

, W

{ I(1), I(1, 1), I(1, 1, 1), . . . } , R

, V

p

,

V(p, I(1)), V(p, I(1, 1)), V (¬ p, I(1, 1, 1)), V(¬ p, I (1, 1, 1, 1)), . . .

の全てが真になるように

V

M = (W, R, V )

/ / / /

• •

•

• · · ·

I(1) _p I(1,1) _p I(1,1,1) _¬p 7 I(1,1,1,1) _¬p

実 際 に

, (M, I(1, 1)) | = p

(M, I(1)) | = ^ p

, (M, I(1, 1, 1)) | = ¬ p, (M, I(1, 1, 1, 1)) | = ¬ p, . . .

(M, I(1, 1)) 6| = p, (M, I(1, 1, 1)) 6| = p, (M, I (1, 1, 1, 1)) 6|= p, . . .

, (M, I(1)) 6| = ^ ϕ → ^ ϕ

,

しかし

,

,

+/ /

I(1) I(1,1) I(1,1,1)

p p ¬p

としてみよう。実は

,

^ ϕ → ^ ϕ

このような「冠頭部の違いを除いて一致する無限個の冠頭論理式が現わ れる部分に反射性を仮定する」という方法は

,

例

5.1 ^^ ϕ → ^ ϕ

K4

,

¬ ( ^^ ϕ → ^ ϕ)

K4

,

1 :¬(^^'!^⇤') 1 :^^' 1 :¬^⇤'

1,1 :^' 1,1,1 :' 1,1 :¬⇤' 1,1,2 :¬'

1,1,1 :¬⇤' 1,1,1,1 :¬' 1,1,2 :¬⇤' 1,1,2,1 :¬' 1,1,1,1 :¬⇤' 1,1,1,1,1 :¬' 1,1,2,1 :¬⇤'

...

<latexit sha1_base64="(null)">(null)</latexit><latexit sha1_base64="(null)">(null)</latexit><latexit sha1_base64="(null)">(null)</latexit>

この冠頭タブローの冠頭部

σ

, σ

,/4: 8

/

• •

5

冠頭部 論理式

1 ¬( ^^ ϕ → ^ ϕ), ^^ ϕ, ¬ ^ ϕ

1, 1 ^ ϕ, ¬ ϕ

1, 1, 1 ϕ, ¬ ϕ

1, 1, 2 ¬ϕ, ¬ ϕ

1, 1, 1, 1 ¬ ϕ, ¬ ϕ

1, 1, 2, 1 ¬ ϕ, ¬ ϕ

1, 1, 1, 1, 1 ¬ϕ, ¬ ϕ . .

. . . .

そこで

,

/ ,

4

• •

: I(1,1,1) _p 8 I(1,1,1,1) _¬p I(1) /

** &&

I(1,1)

p p

I(1,1,2)

•

¬p

これは有限反例モデルになっている。

以上のように

,

K4

,

(filtration method)

§6

/

6 濾過法による有限反例モデルの構成

Σ

ϕ

w

∈ W

w

∈ W

∼

ψ ∈ Σ

(M, w

) | = ψ ⇔ (M, w

) | = ψ

となるように定め

,

w ∈ W

∼

[w] , ∼

W /∼

Kripke

M = (W, R, V )

(filtration)

,

Kripke

(W/∼, S, V

[ + w]

)

(1)

p ∈ Σ

, V (p, w)

w ∈ W

,

{[v] : V

(p, v)は真 }

;

(2)

w

, w

∈ W

, w

Rw

[w

]S[w

] ;

(3)

w

, w

∈ W

ψ ∈ Σ

, (M, w

) | = ψ

[w

]S[w

]

(M, w

) | = ψ .

ϕ

n

,

n

[w ]

, W/∼

2

,

, (W/∼, S, V

[

+ w]

)

濾過の条件

(2)

w

Rw

[w

]S[w

]

, [w

]S[w

]

w

Rw

,

,

• •

w₁ w₂

(p)

•

•

w₁ 0 w₂ ⁰ (p) p

というモデルを考えてみよう。ただし

, w

∼ w

w

∼ w

6

, w

Rw

, w

Rw

,

(2)

[w

]S[w

]

, (M, w

) | = p

1

で

,

2

濾過の条件

(3)

(M, w

) | = p

つまり

, w

Rw

,

w

Rw

w

また

,

,

S ⊂ (W/∼) × (W /∼)

S = {([w

], [w

]) :

w

, w

∈ W

w

∼ w

, w

∼ w

, w

Rw

} ,

S ⊂ (W /∼) × (W/∼)

S = {([w

], [w

]) :

ψ ∈ Σに対して (M, w

) | = ψ

(M, w

) | = ψ }

, (W /∼, S, V

[

+ w]

)

(finest)

, (W /∼ , S, V

)

(coarsest)

M = (W, R, V)

ϕ

, M

(W /∼, S, V

[ + w]

)

ϕ

,

定理

6.1 Σ

ϕ

, M

= (W/∼ , S, V

)

M

w ∈ W

ψ ∈ Σ

(M, w ) | = ψ ⇔ (M

, [w]) | = ψ

となる。

証明

ψ

,

0

,

(3)

,

k

k + 1

¬ , ∧ , ∨ , →

,

∼

,

,

ψ = χ

( ⇒ ) (M, w

) | = χ

[w

]S[w

]

,

(3)

(M, w

) | = χ

,

(M

, [w

]) | = χ

,

[w

]S[w

]

(M

, [w

]) | = χ

( ⇐ ) (M

, [w

]) | = χ

w

Rw

w

,

(2)

[w

]S[w

]

, (M

, [w

]) | = χ

よって

,

(M, w

) | = χ

, w

Rw

(M, w

) | = χ

一般に

, R

S

,

[w

]S[w

]

[w

]S[w

]

, [w

]S[w

]

,

R

M = (W, R, V )

,

S b = {([w

], [w

]) :

n

([w

], [w

]) ∈ S

}

という特殊な

S

, S

n

S

, M

= (W/ ∼ , S b , V

)

まず

,

(2)

R

,

(3)

(M, w

) | = ψ

[w

]S b [w

]

, S b

[w

], [w

], [w

], . . . , [w

]

[w

]S[w

], [w

]S[w

], . . . , [w

]S[w

]

となるので

, S

,

w

, w

∈ W

w

∼ w

, w

∼ w

, w

Rw

R

, (M, w

) | = ψ

1

∧ ψ

, (M, w

) | = ψ ∧ ψ

w

, w

, . . .

,

(M, w

) | = ψ ∧ ψ

, (M, w

) | = ψ

このようにして

,

R

M = (W, R, V)

こで

, M = (W, R, V)

K4

ルとすれば

, M

M

= (W /∼ , S b , V

)

,

M

(3)

, (M, w

) | = ψ

[w

]b S[w

]

(M, w

) | = ψ ∧ ψ

, §5

,

(M, w

) | = ψ ∧ ψ

, (M, w

) | = ψ → ψ

/ /

/ / 7 +//

• • •

注 あり

,

w

,

以上の内容を例

4.1

, 1 : ¬ ( ^ ϕ →

^ ϕ)

K4

,

/ / / /

• •

•

• · · ·

I(1) _p I(1,1) _p I(1,1,1) _¬p 7 I(1,1,1,1) _¬p

という反例モデル

M = (W, R, V )

, I(1, 1, 1, 1), I(1, 1, 1, 1, 1),

· · · ∈ [I(1, 1, 1)]

, M

M

= (W /∼, S b , V

[

+ w]

)

+/ /

[I(1)] [I(1,1)] [I(1,1,1)]

p p ¬p

従って

, K4

b S

,

,

謝辞

本研究を遂行するにあたって

,

「あかでみあ」を提供してくださった齋藤曉さんに

,

注

1より詳細なタブロー法の歴史に興味のある読者は Fitting (1999)を参照せよ。

2特に, Fitting (1983);神野･内井 (1976);菅原 (1987)には様相論理のタブロー法に関する記 述もある。

3本稿にある例 4.1や例 5.1など。

4 従って,冠頭タブローでは規則を適用する前後の冠頭論理式が離れた位置に現われること があるので,この点においては自然演繹と同じような特徴をもっている。Hilbert流やシークエント 計算のように,遠隔的な(推論) 規則を許さないようにするためには,規則を適用するたびに,その

規則による論理式の変化の履歴を残すようなタブローをつくればよい。このようなタブローはブ ロックタブロー(Smullyan (1995)) として知られている。

5 この定義によれば,無限に長い枝をもつ冠頭タブローは永久に完成しないということになる。

しかし,それでは不便なので,後により扱いやすいような定義に改善する。

6π 規則には特に手を加える必要はない。

7R が同値関係であれば,w ∈W から任意の w⁰ ∈W に到達可能であるということを思い出 そう。

8記号 Bは §3で既に定義している。

9もしも 1 : ¬ϕの冠頭タブローが完成していなければ,その時点で閉じていないからといって,

ϕの冠頭タブローによる証明が存在しないと言い切ることはできない。

10単に反例モデルが存在するかどうかだけでなく,有限反例モデルが存在するかどうかを調べ ることは,論理の決定可能性を調べる上で重要である。詳しくは Goldblatt (1992)の §4などを参 照せよ。

11濾過法については, Goldblatt (1992)の §4や Chagrov (1997)の §5.3などを参照せよ。特に, 本稿を執筆するにあたり,後者を大いに参考にさせてもらった。

参考文献

Beth, Evert Willem (1955) Semantic entailment and formal derivability. , Med- edeelingen der Koninklijke Nederlandsche Akademie van Wetenschappen, Afd. Letterkunde ; nieuwe reeks, d. 18, no. 13: Noord-Hollandsche Uitg.

Mij.

Chagrov, Alexander (1997) Modal logic , Oxford logic guides ; 35: Clarendon Press ; Oxford University Press.

d’Agostino, Marcello (1999) “Tableau methods for classical propositional logic,”

in Handbook of tableau methods : Springer, pp. 45–123.

Fitting, Melvin (1972) “Tableau methods of proof for modal logics,” Notre Dame Journal of Formal Logic , Vol. 13, No. 2, pp. 237–247.

(1983) Proof Methods for Modal and Intuitionistic Logics : Reidel.

(1996) First-order logic and automated theorem proving , Graduate texts in computer science (Springer-Verlag New York Inc.): Springer, 2nd edition.

(1999) “Introduction,” in Handbook of tableau methods : Springer, pp.

1–43.

参考文献

Goldblatt, Robert (1992) Logics of time and computation , CSLI lecture notes ;

no. 7: Center for the Study of Language and Information, 2nd edition.

Hintikka, Jaakko (1953) A new approach to sentential logic : Societas scientiarum Fennica.

(1955) Two papers on symbolic logic : form and content in quantification theory and reductions in the theory of types , Acta philosophica Fennica ; fasc.

8: Acta philosophica fennica.

Priest, Graham (2008) An introduction to non-classical logic : Cambridge Uni- versity Press, 2nd edition.

Smullyan, Raymond R (1995) First-order logic : Dover.

神野慧一郎･内井惣七

(1976)

斎藤哲郎

(1964)

菅原道明

(1987)

丹治信春

(1999)

戸田山和久

(2000)

リチャードジェフリー

(1995)

This work is licensed under a Creative Commons

“Attribution 4.0 International” license.

©

2019 Journal of Science and Philosophy