A Derivation of the Contradiction in Frege's Grundgesetze System: Professor Michael Resnik's Property Version

酔狂なことではありますが、前回は、Frege の Grundgesetze 体系から矛盾が出てくる様子を、Michael Resnik さんの証明に従いながら見てみました。その証明では所属関係が使われていましたが、今回は所属関係を使わず、性質、属性、概念を使った証明の例を、やはり Resnik さんに従いつつ、示してみたいと思います。参考にするのは、次の文献です。

  • Michael D. Resnik  Frege and the Philosophy of Mathematics, Cornell University Press, 1980, p. 213.

ここに掲載されている証明を、大幅に補足しつつ以下で記します。原則的に Resnik さんの証明をなぞっただけのものですが、Resnik さんは色々と証明の step を省いておられるので、当方で考えて、かなり補っています。前回同様、ひどく細かく、くどく記しています。かなりくどすぎますが、その方が私が間違いを犯していても、どこで間違っているのか、簡単に見て取れるでしょうし、論理学の初歩の初歩さえ知っておれば、証明を容易に追うことができると思いますので、普通は自明すぎて示されない step も明示しております。なお、以下に私が記した証明には、誤りが含まれている可能性が高いので、絶対にそのまま信用してしまわず、読まれる場合は正しいかどうか、一行一行、確認しながら読んでください。間違っておりましたら謝ります。大変すみません。


以下では引用符を省き、Use / Mention distinction についても、あまりこだわらずに記します。各種の記号について説明します。F, G を任意の述語、または性質とし、x, y, z を変項とします。また ≡ を双条件法、⊃ を実質条件法、・ を連言記号、¬ を否定、∃ を存在量化子、(z) や (F) のように、丸カッコ内に変項や述語がある表現は普遍量化子、'xFx のように apostrophe を伴う表現は、性質 F を満たすもの x からなる class を表すとします。式のなかには、その式の名前を式の先頭に掲げているものもあります。Resnik さんの付けている名前をそのまま利用するとともに、Resnik さんが名前を付けていない場合には、こちらで名前を付けた場合があります。


さて、R という性質と r という class を次のように定義します。 そして、Frege の基本法則 V に相当する公理 (V) を掲げます。

    • (Df 1)  Rx ≡ (∃F)( x = 'yFy ・ ¬Fx )
    • (Df 2)  r = 'xRx
    • (V)  'xFx = 'yGy ≡ (z)( Fz ≡ Gz )

(Df 1) は、例えば以下のように読まれます。R という性質を持つとは、次の時かつその時に限る、すなわち、ある性質 F があって、その F を有するもの y からなる class を x とし、かつその x は自身の有する性質 F には当てはまらない。ここでは読み方よりも、式のいわば内容を把握するようにしてください。
(Df 2) は、例えば以下のように読まれます。r は性質 R を持つもの x からなる class に等しい。ここでも読み方よりも、その内容を捉えるようにしてください。

以下では、これら (Df 1) と (Df 2) とから、(V) を使って、Rr と ¬Rr が帰結し、矛盾が出てくることを証明します。


まず、Rr を証明します。ここでは (V) は使いません。


(Df 1) の x に r を代入し、y を x に付け替えると、

    • Rr ≡ (∃F)( r = 'xFx ・ ¬Fr ).

これは

    • Rr ⊃ (∃F)( r = 'xFx ・ ¬Fr ) ・ (∃F)( r = 'xFx ・ ¬Fr ) ⊃ Rr

のことだから、

    • (∃F)( r = 'xFx ・ ¬Fr ) ⊃ Rr.

そしてこの対偶を取ると、

    • ¬Rr ⊃ ¬(∃F)( r = 'xFx ・ ¬Fr ).

今、¬Rr と仮定します。すると、すぐ上の式と Modus ponens により、

    • ¬(∃F)( r = 'xFx ・ ¬Fr ).

この式は、r = 'xFx ・ ¬Fr を成り立たせるような性質 F はない、と言っているから、それは、どの性質 F についても、r = 'xFx ・ ¬Fr を満たすことはないということ故、

    • (F)¬( r = 'xFx ・ ¬Fr ).

これは任意の F について、r = 'xFx と ¬Fr の両方がともに成り立つことはないと言っているから、それはつまり、r = 'xFx でないか ¬Fr でないこと故、

    • (F)( r ≠ 'xFx ∨ ¬¬Fr ).

ここに見られる二重否定¬¬「~でないことはない」は、肯定「~である」だから、

    • (F)( r ≠ 'xFx ∨ Fr ).

これは、「任意の F について、~でないか、または−である」という形をしています。「~でないか、または−である」ということは、「~であり、かつ−でない」ということはない、ということです。これは「~でありながら、−でない」などということはない、ということです。かくかくが成り立っていながら、しかじかが成り立たないということはない、ということであり、かくかくが成り立つならば、しかじかも成り立つ、ということです。ということは、振り返ってみると、「~でないか、または−である」ということは、「~ならば、−である」ということです。つまり、「~でないか、または−である」は、実質条件法を表しています。よって上の式は、

    • (F)( r = 'xFx ⊃ Fr )

のことだとわかります。

こうして、先ほど ¬Rr と仮定したことから、今の (F)( r = 'xFx ⊃ Fr ) が出てきたので、この仮定を落として条件法を導入すれば、

    • (4)  ¬Rr ⊃ (F)( r = 'xFx ⊃ Fr ).

さて今度は、(F)( r = 'xFx ⊃ Fr ) と仮定します。F は任意なので F を R で普遍例化すれば、

    • r = 'xRx ⊃ Rr.

ところで、

    • (Df 2)  r = 'xRx

だったから、

    • r = r ⊃ Rr.

ここで、一旦、条件文というものについて考えます。条件文は、前件が真で後件が偽の時に、偽です。もしもある条件文の前件が常に真ならば、その条件文の真偽は、その条件文の後件の真偽に依存します。つまりその条件文の後件が真の時、条件文全体でも真で、その条件文の後件が偽の時、条件文全体でも偽となる、ということです。要するに、前件が常に真である条件文の真偽は、その条件文の後件の真偽に一致する、ということです。したがって、ある条件文の真偽だけが問題であるならば、かつその条件文の前件が常に真であるならば、その条件文で重要なのは後件だけであり、前件は冗長であって、前件を消去しても差し支えない、ということになります。

さて、条件文 r = r ⊃ Rr が真であるとして成り立つか、あるいは偽であるとして成り立たないかが、私たちの関心事です。そして、この条件文の前件は常に真となります。ということは、このような条件文については、前件 r = r を消去し、後件 Rr のみに注意を限っても不都合は生じない、ということです。よって、上記 r = r ⊃ Rr から前件の r = r を略すと、

    • Rr

です。

こうしてこの Rr は、仮定 (F)( r = 'xFx ⊃ Fr ) から出てきたので、この仮定を落とし条件法を導入すれば、

    • (F)( r = 'xFx ⊃ Fr ) ⊃ Rr

となります。

ここで再び ¬Rr と仮定します。すると、上記の

    • (4)  ¬Rr ⊃ (F)( r = 'xFx ⊃ Fr )

により、Modus ponens を使って、

    • (F)( r = 'xFx ⊃ Fr )

が出ます。そして今度は出てきたこの式と、既に導出されていた三つ前の式

    • (F)( r = 'xFx ⊃ Fr ) ⊃ Rr

とで、Modus ponens により、

    • Rr

が出ます。これは ¬Rr と仮定することから出てきたから、この仮定を落として条件法を導入すれば、

    • (6)  ¬Rr ⊃ Rr

です。

さて、三たび ¬Rr と仮定します。これと (6) により、Modus ponens を使うと、

    • Rr

です。今、¬Rr と仮定していたから、これと出たばかりの Rr とで、連言記号を導入すれば、

    • Rr ・ ¬Rr

となって矛盾です。したがって、背理法により、仮定 ¬Rr は否定されねばならず、¬¬Rr です。これはつまり、

    • Rr

です。こうして Rr を証明できました。



次に、¬Rr を証明します。ここでは (V) を使うことになります。


まず、

    • (Df 1)  Rx ≡ (∃F)( x = 'yFy ・ ¬Fx )

の x に r を代入し、y を x に付け替えると

    • Rr ≡ (∃F)( r = 'xFx ・ ¬Fr ).

今、Rr を仮定します。これに直前の Rr ≡ (∃F)( r = 'xFx ・ ¬Fr ) とで、Modus ponens により、

    • (8)  (∃F)( r = 'xFx ・ ¬Fr ).

(8) の F を G で存在例化すると、

    • (9)  r = 'xGx ・ ¬Gr.
    • (Df 2)  r = 'xRx

だったから、(9) の r を 'xRx に変えると、

    • 'xRx = 'xGx ・ ¬Gr.

故に、

    • 'xRx = 'xGx.

ところで、

    • (V)  'xFx = 'yGy ≡ (z)( Fz ≡ Gz )

により、F を R に代えて

    • 'xRx = 'yGy ≡ (z)( Rz ≡ Gz ).

この式の左辺 'xRx = 'yGy は、「任意の x からなる R の class と、任意の y からなる G の class は等しい」と述べており、y は任意であるから、y が x であってもよく、その場合、

    • 'xRx = 'xGx ≡ (z)( Rz ≡ Gz )

が成り立つ。

こうして今の式と、上記 (V) の直前に記した 'xRx = 'xGx とで Modus ponens により、

    • (10)  (z)( Rz ≡ Gz ).

この z は任意なので r で普遍例化すると

    • Rr ≡ Gr.

先ほど Rr と仮定していたから、この仮定と今の Rr ≡ Gr とで Modus ponens により、

    • Gr.

ところで、上記の (9) r = 'xGx ・ ¬Gr からは

    • ¬Gr

が出ます。するとこれら Gr と ¬Gr とで、連言記号を導入すれば、

    • Gr ・ ¬Gr.

これは矛盾です。したがって、背理法により、先ほどから仮定してきた Rr は否定されねばならず

    • ¬Rr

が帰結します。こうして ¬Rr が証明できました。


以上です。今回の説明に、間違いがありましたら、お詫び申し上げます。誠にすみません。無批判に受け取らず、正しいかどうか、読み返して確認してただきますよう、よろしくお願い致します。
次回は、M. Giaquinto さんによる矛盾の簡略化された証明を記そうと思います。