Can There Be Vague Objects?: Formal Proof II: Heck Version

もう一つ、Evans 論文 ''Can There Be Vague Objects?'' にある論証を書き下してみます。今度は次の論文

  • Richard G. Heck, Jr.  ''That There Might Be Vague Objects (So Far as Concerns Logic),'' in: The Monist, vol. 81, 1998, pp. 277-99, Pre-Pub. Version. Section 2: Evans's Formal Argument, and Section 4: Whence the Contradiction?, pp. 2-5, 9-11

の該当箇所を参照しました。ここでも Heck 先生の示唆に基づき、先生の証明を少し修正して、さらに当方で補足を多数加えて書き出しています。例によってかなりくどいです。いちいち細かいところまで書いているため、私の補足に間違いが含まれていましても、それがどこだか容易に特定できると思います。間違った論証を書いておりましたら、誠に申し訳ございません。*1


Heck 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)  ▽( a = b ) → 〜( a = b )   (1) から (5) が出たので。

(7)  △( ▽( a = b ) → 〜( a = b ) )   (6) と Necessitation: ⊢ α ならば ⊢ □α により*4。□を△と読み換える。α が定理として成り立つならば、α は必然的に成り立つ。

(8)  △▽( a = b ) → △〜( a = b )   (7) に対し T の公理A6: □( p → q ) → ( □p → □q ) を使って*5

(9)  ▽( a = b ) → △▽( a = b )   S5 の characteristic axiom A8: ◇p → □◇p *6 の◇を▽と読み換え、□を△と読み換えて、▽p → △▽p とし、p に ( a = b ) を代入。

(10)  ▽( a = b ) → △〜( a = b )   (1) ▽( a = b ) を再度仮定すれば、(8) と (9) から △〜( a = b ) が出るので。(仮定 (1) は (6) で一旦解除されているので、ここで再び仮定を立てている。Evans 論文では、▽( a = b ) が常に成り立つことが、実は何より前提されている。よって、繰り返し使うことができる。)

(11)  △p ≡ 〜▽p    仮定   ( p であるかどうかが確定しているならば、p であるかどうかが不確定であることはなく、逆も真。)

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

(13)  △p ≡ △〜p   (11) の p に 〜p を代入したもの △〜p ≡ 〜▽〜p と、(12) とで。( p であることが確定的ならば、p でないことも確定的なはずで、その逆も真。)

(14)  ▽( a = b ) → △( a = b )   (10) の後件の否定記号を (13) により消去して。

(15)  〜△( a = b ) → ▽( a = b )   (11) の p に ( a = b ) を代入し △( a = b ) ≡ 〜▽( a = b ), 両辺に否定記号を前置し 〜△( a = b ) ≡ 〜〜▽( a = b ), 二重否定を解くと 〜△( a = b ) ≡ ▽( a = b ). ここから → を得る。

(16)  〜△( a = b )   仮定   ( a と b が等しいかどうか、確定的である、ということはない。)

(17)  △( a = b )   (14), (15), (16) により。

(18)  △( a = b ) ∧ 〜△( a = b )   (16) と (17) により矛盾。

(19)  △( a = b )   仮定 (16) から (18) という矛盾が出たので、(16) を否定し 〜〜△( a = b ), 二重否定を消去して。

(20)  〜▽( a = b )   (19) と (11) により。

(21)  ▽( a = b )   仮定   (これは最初の仮定 (1) に同じ。(6) と (10) でこの仮定が解除されているので、改めてここで仮定を立てる。なお、仮定 (1) は Evans にとって、いわば公理のようなものとして意図されている。)

(22)  ▽( a = b ) ∧ 〜▽( a = b )   (20) と (21) により、矛盾。


† 双対 (duality) の説明*7

簡単な場合のみを具体例により、大まかに説明する。今、α を命題論理の式とし、α の中に命題結合子は、連言 ∧, 選言 ∨, 否定 〜 しかないものとする (これでも一般性は失われない)。この時、α と双対な式 α* とは、α の中のすべての命題変項に否定記号 〜 を前値し、かつすべての ∧ を ∨ に、すべての ∨ を ∧ に変えたものを言う。例えば、( 〜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 となるだろう。そしてこの今の式の両辺に、否定記号を一つずつ追加してやれば、▽p ≡ 〜△〜p となり、この式は、▽ の、△ による定義と考えることができる。
また、△p と双対な式を考えれば、▽〜p となり、双対の原理は 〜△p ≡ ▽〜p となるだろう。この両辺に否定記号を追加すれば、△p ≡ 〜▽〜p となって、△ の、▽ による定義になり、これは (12) の式と同じになっていることがわかる。

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


以上です。私による証明の補足が間違っているようでしたら、ごめんなさい。間違っている可能性がきわめて高いので、すらっと読み流して鵜呑みにすることのないようお願い致します。


PS
Evans 論文を読む時、最低でも踏まえておく必要のある基本事項を、今度の回に短く記す予定です。

*1:なお、Rasmussen Version の場合もそうでしたが、以下の証明の中では 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. 31, G. E. ヒューズ、M. J. クレスウェル、『様相論理入門』、三浦聰、大浜茂生、春藤修二訳、恒星社厚生閣、1981年、29ページ。

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

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

*7:この説明は Heck 先生によるものではなく、当日記著者によるものです。Rasmussen version の際に行った双対の説明と、以下はほとんど同じですが、説明の最後の方で少し異なっています。