Can There Be Vague Objects?: Formal Proof I: Rasmussen Version

次に Gareth Evans の論文 ''Can There Be Vague Objects?'' に見られる論証を、full で記してみます。まず、次の文献

  • Stig Alstrup Rasmussen  ''Vague Identity,'' in: Mind, New Series, vol. 95, no. 377, 1986, pp. 87-88

の該当箇所に書かれている示唆をもとに書き下します。なお、Evans 論文の論証は、以下で記すような形式化しかあり得ない、ということではございません。以下のものは一つの例にすぎません。そもそも Evans 論文にある論証は、正確に言って、どのようなものなのか、専門家の間でも意見の相違があるようです。Evans 本人の頭の中でどのような証明が思い描かれていたのか、これも今となっては誰にもわかりません。Evans 論文にあるような sketch が残されているだけなので、どのようにその細部を埋めるかは、各哲学者の抱いている見解によって違ってきます。
それでは Rasmussen 先生の考える Evans の論証を記します。先生の示唆に基づき、細部を私の方で大幅に補足します。かなりくどく証明の各 step を書き込みます。くどすぎるとは思いますが、その一方で、私の記述が間違っていれば、どこで間違っているかわかると思いますので、細かく記します。誤ったことを書いておりましたら、大変申し訳ございません。*1


Rasmussen Version


(1)  ▽( a = b )   仮定  ( a が b と等しいかどうか、不確定としてみよう。)

(2)  x[▽( x = a )]b   (1) の Lambda Abstraction*2  ( b は性質 x[▽( x = a )] を満たす。)

(3)  〜▽( a = a )   仮定  ( a が自分自身に等しいかどうか、不確定である、などということはない。)

(4)  〜x[▽( x = a )]a   (3) の Lambda Abstraction  ( a は性質 x[▽( x = a )] を満たさない。)

(5)  〜( a = b )   (2), (4) と Leibniz's Law ( Indiscernibility of Identicals ): a = b → [ Φ(a) ≡ Φ(b) ] の対偶より*3。Φ を性質 x[▽( x = a )] として。

(6)  △〜p ≡ 〜▽p   仮定 (Dual)†

(7)  ▽p → △▽p   S5 の characteristic axiom A8: ◇p → □◇p より*4。◇を▽と、□を△と読み換える。

(8)  △▽( a = b )   (7) の p に ( a = b ) を代入して、(1) により。

(9)  △p → △△p   S5 の定理A7: □p → □□p より*5。(この定理は S4 の公理A7.) *6

(10)  △〜p → △△〜p   (9) の p に 〜p を代入。

(11)  〜▽p → △△〜p   (10) の左辺を (Dual) により。

(12)  〜▽( a = a ) → △△〜( a = a )   (11) の p に ( a = a ) を代入。

(13)  △△〜( a = a )   (12) と (3) から。

(14)  △〜▽( a = a )   (13) と (Dual) で。

(15)  a = b → [ ▽( c = a ) → ▽( c = b ) ]   Leibniz's Law ( Indiscernibility of Identicals ): a = b → [ Φ(a) ≡ Φ(b) ] より。Φ を ▽( c = x ) として。

(16)  〜[ ▽( c = a ) → ▽( c = b ) ] → 〜( a = b )   (15) の対偶。

(17)  [ ▽( c = a ) ∧ 〜▽( c = b ) ] → 〜( a = b )   (16) の前件を同値変形。

(18)  △[ [ ▽( c = a ) ∧ 〜▽( c = b ) ] → 〜( a = b ) ]   (17) と Necessitation: ⊢ α ならば ⊢ □α で*7。α が定理として成り立つならば、α は必然的に成り立つ。

(19)  △[ ▽( c = a ) ∧ 〜▽( c = b ) ] → △〜( a = b )   (18) と T の公理A6: □( p → q ) → ( □p → □q ) より*8

(20)  [ △▽( c = a ) ∧ △〜▽( c = b ) ] → △〜( a = b )   (19) の前件に対し、T3: □( p ∧ q ) ≡ ( □p ∧ □q ) *9.

(21)  [ △▽( b = a ) ∧ △〜▽( b = b ) ] → △〜( a = b )   (20) の c は任意なので、その c を b に。

(22)  △▽( a = b ) ∧ △〜▽( a = a )   (8) と (14) より。

(23)  △▽( b = a ) ∧ △〜▽( b = b )   (22) の a と b は任意であるから、その a を b に、b を a にして。

(24)  △〜( a = b )   (21) と (23) により。(これは Evans 論文の (5') △〜( a = b ) に同じ。)

(25)  〜▽( a = b )   (24) に (Dual).

(26)  ▽( a = b ) ∧ 〜▽( a = b )   (1) と (25) により、矛盾。


† 双対 (duality) の説明*10

簡単な場合のみを具体例により、大まかに説明する。今、α を命題論理の式とし、α の中に命題結合子は、連言 ∧, 選言 ∨, 否定 〜 しかないものとする (これでも一般性は失われない)。この時、α と双対な式 α* とは、α の中のすべての命題変項に否定記号 〜 を前置し、かつすべての ∧ を ∨ に、すべての ∨ を ∧ に変えたものを言う。例えば、( 〜p ∧ q ) ∨ ( r ∧ 〜q ) と双対な式は、( p ∨ 〜q ) ∧ ( 〜r ∨ q ) となる。明らかに α は α** に一致する。このように考えられた式 α とその双対な式 α* との間には、次の関係が成り立つことが、一般に知られている。つまり、α とその双対な式 α* について、〜α ≡ α* が成り立つ (証明は略す)。すなわち、α と双対になっている式 α* は、α の否定 〜α と同値である。この事実を「双対の原理」と呼ぶ。
今度は命題論理から述語論理に移ると、普遍量化子 ∀ と存在量化子 ∃ が式に追加される。例えば、A を述語論理の式として、∀xA を考えた時、この式の双対 (∀xA )* は、∃xA* となる。ここでの A を最も単純な F(x) とすれば、∀xF(x) の双対 (∀xF(x) )* は、∃x〜F(x) となる。同様に、∃xA を考えた時、この式の双対 (∃xA )* は、∀xA* となり、A を F(x) とすれば、∃xF(x) の双対 (∃xF(x) )* は、∀x〜F(x) となる。
そして ∀xA とこの式の双対 (∀xA )* との間には、やはり先ほどと同様の双対の原理 〜∀xA ≡ (∀xA )* が成り立つ (証明略)。この時、A を F(x) とすれば、〜∀xF(x) ≡ ∃x〜F(x) となる。ここで両辺に否定記号を一つずつ追加してやれば、よく知られた普遍量化子の、存在量化子による定義式 ∀xF(x) ≡ 〜∃x〜F(x) ができる。
また、∃xA とこの式の双対 (∃xA )* との間にも、やはり 〜∃xA ≡ (∃xA )* が成り立つ (証明略)。ここで A を F(x) とすれば、〜∃xF(x) ≡ ∀x〜F(x) となる。そして両辺に否定記号を一つずつ追加してやると、周知の通り、存在量化子の、普遍量化子による定義式 ∃xF(x) ≡ 〜∀x〜F(x) ができ上がる。
以上の双対に関する基本事項と類比的に、▽p と双対な式を考えてみるならば、それは△〜p となり、▽ に関する双対の原理を考えてみれば、それは 〜▽p ≡ △〜p となるだろう。これは (6) の (Dual) と同じである。そしてこの今の式の両辺に、否定記号を一つずつ追加してやれば、▽p ≡ 〜△〜p となり、この式は、▽ の、△ による定義と考えることができる。
また、△p と双対な式を考えれば、▽〜p となり、双対の原理は 〜△p ≡ ▽〜p となるだろう。この両辺に否定記号を追加すれば、△p ≡ 〜▽〜p となって、△ の、▽ による定義となる。

ここでの双対に関する説明は、次を参照した。井関清志、『記号論理学 (命題論理)』、第2版、数学選書、槇書店、1971年、28-30ページ、井関清志、『記号論理学 (述語論理)』、第2版、数学選書、槇書店、1978年、367-369ページ。


以上です。私による証明の補足が間違っていましたら、誠にすみません。間違っている可能性が高いので、十分注意してください。

*1:なお、証明の中では indent していない行が多くあり、証明が見づらいと思います。それぞれ indent してもよいのですが、そうしてみるとまた別の面で見づらくなるので、indent せず、そのまま記させてもらいます。読みづらくてすみません。

*2:式 (2) の先頭の 'x' には頭に横棒が付いていますが、英語原文では '^' です。都合により横棒に代えてあります。以下同様。また、Lambda Abstraction については、Lambda 計算の入門書をご覧ください。その入門書の初めの方にいつも書いてあります。「関数抽象」と呼ばれることもあります。

*3:なお、おそらく通常は、Identity of Indiscernibles のことを 'Leibniz's Law' と呼ぶ。この法則について詳しくは、2013年1月4日の当日記項目 'What Problem Did Frege Argue in his "Über Sinn und Bedeutung"? More Precisely, What Problem Is a Great Part of his Most Famous Paper Devoted to? Part 3' の註10と、そこで上げられている文献を参照ください。

*4:G. E. Hughes and M. J. Cresswell, An Introduction to Modal Logic, Routledge, University Paperbacks Series, 1968, p. 49, G. E. ヒューズ、M. J. クレスウェル、『様相論理入門』、三浦聰、大浜茂生、春藤修二訳、恒星社厚生閣、1981年、48ページ。

*5:Hughes and Cresswell, p. 49, ヒューズ、クレスウェル、48ページ。

*6:Hughes and Cresswell, p. 46, ヒューズ、クレスウェル、44ページ。

*7:Hughes and Cresswell, p. 31, ヒューズ、クレスウェル、29ページ。

*8:Hughes and Cresswell, p. 31, ヒューズ、クレスウェル、29ページ。

*9:Hughes and Cresswell, p. 34, ヒューズ、クレスウェル、32ページ。

*10:この説明は Rasmussen 先生によるものではなく、当日記著者によるものです。