Alfred North Whitehead (1861-1947) と Bertrand Russell (1872-1970) による Principia Mathematica, 3 vols. (1910-13)(以下 'Principia' と略記) では、dot を使って式が表現されています。以下で、この dot を使った式の読み方、より正確には、dot をカッコに書き換える大体の方法を記してみます。参考にした文献は以下のものです。
- Alfred North Whitehead and Bertrand Russell Principia Mathematica to *56, Cambridge University Press, Cambridge Mathematical Library, 1997, pp. 9-11, The use of dots.
なお、私は Principia に精通しているという訳ではありませんので、以下の記述に一切間違いがないとは保証できません。また、以下の方法が、Principia に出てくるあらゆる式に普遍的に適用できる完全無欠の algorithm だと言うものでもありません。ただ、大体のところは以下に記述する方法で対処できるのではないかと推測しています。また、下記の方法で説明するのは、Principia の初等的な式に限ります。命題論理と述語論理と確定記述句を含んだ式のみの読み方、方策を記します。Principia では、独自の記号が多数出てきますが、そのような記号を含んだ式の理解も、初等的な式の読みが前提としてあり、初等部分を理解すれば、その応用として、なじみのない難しい式も、読み解くことができるのではないかと思います。いずれにしましても、正確にはご自分で Principia をお読みいただくか、Russell を勉強している方は比較的おられると思いますので、身近にいらっしゃる Russell 読みの方にご確認下さい。それでは、まず dot をカッコに変換する大体の方法、方策を記します。
大まかな基本方針
Principia における dot を使った式を目の前にした時、何をどこからどう読めばよいのかわからないということがあるかもしれません。そこで初めに、式を読み解くための基本方針、基本的な戦略を述べます。
Dot の、カッコ・連言への変換方針大略
初めに方針の大略を掲げておきます。
式中で最大 dot 数のところを探す。→ その dot がどんな記号の横にあるかを確認。→ 記号の右横か左横かを確認。→ 右横なら右へ、左横なら左横へ式を走査。→ 何点の dot が出てくるかに注意し、出てくる dot を無視して走査を進めるか、あるいはカッコなり連言なりに変換して行く。
この方針をもう少し噛み砕いた説明を掲げます。
まず、以下の 1. から 6. の説明は、その大筋を理解していただくだけで結構です。細部は後で七つの実例を使って解説しますので、最初は大体のところを把握し、後の実例で詳細を理解して、それから再び 1. から 6. に戻って読み直し、理解を深めて下さい。
- Principia における dot を使った式を読み解く際、まず、目の前にした式の、dot が最も多く打たれているところを確認します。そこがその式で最も大きな切れ目となるところです。さて、その dot の数が n 点だとしましょう。もしも他に n 点の dot が打たれているところがなければ、この n 点のところから式の解析を始めます。(しかし n 点の dot が打たれている箇所が複数あるかもしれません。その場合は以下に掲げる具体例でその対処法を記します。)
- さて、式の解析の始めとなるこの n 点を「基点」と呼ぶことにします。1. で基点を確認したら、今度は基点における dot の数 n を記憶しておき、この基点がどのような記号の横に打たれているかを確認します。Dot にはカッコを表す機能と連言を表す機能がありますが、どのような記号の横にあるかによって、その dot がカッコであるのか、連言であるのかがわかるので、基点とその数を記憶したら、その基点がどのような記号の横にあるのかを確認します(どの記号の横にある時にカッコで、どの記号の横にある時に連言であるのかは、以下の実例で説明します)。
- さて、基点がカッコなのか連言なのかがわかったとします。ここでは仮に基点がカッコであるとわかったとしましょう(連言の場合については、以下の実例で説明します)。カッコであったなら、そのカッコがどこで閉じるかを確認しなければなりません。今、そのカッコが右に開いたカッコだとしてみましょう(そのカッコがどのような場合に右に開いているのか、どのような場合に左に開いているのかについても、以下の具体例で明らかにします)。その場合、右に開いたカッコを表すこの基点から、式を右へと読み進みながら、どこでこのカッコが閉じるのかを確認する必要があります。この時、基点の数 n を頭の片隅に置きながら、(1) n より大きい数の dot が出てくるか、(2) n と同数の dot が出てくるか、(3) n より小さい数の dot が出てくるか、(4) 0 個の dot が出てくるかを注意しながら、基点より右へと式を走査して行きます。
- もしも、(1) n より大きい数の dot が出てくるところがあれば、そこでカッコが閉じます。もしも、(2) n と同数の dot が出てくるところがあれば、そこでカッコが閉じることもあれば閉じないこともあります。その出会った同数の dot がどのような記号の横に打たれているかによって、閉じたり閉じなかったりするのです(同数の dot と出会った時、カッコがいつ閉じていつ閉じないかは以下の実例で解説します)。また、もしも、(3) n より小さい数の dot が出てくるところがあれば、そこではカッコは閉じません。その dot は無視してさらに式の走査を右へと進めます。また、もしも、(4) 0 個の dot が出てくるところがあれば、あるいは言い換えると、基点以降にもはや dot が全く出てくることなく、式の終端に至ったならば、その終端でカッコは閉じます。
- さて、基点から始めて、式を走査し、どこかでカッコが閉じたとしましょう。この時、カッコで括られた中に、もはや dot が何もなかったとしたら、式中の基点より右側では、すべて dot がカッコへと書き換えられたことになります。しかしもしも基点から始めて、式を走査し、どこかでカッコが閉じた時、そのカッコ内にさらに dot があったとしましょう。その時は 1. に戻って、このカッコ内で最も大きな数の dot が打たれているところを確認し、その後は、再び 2., 3., 4. と続けて行って、次々カッコを閉じて行き、最後に dot が打たれているところがないところまで、走査を繰り返し続けて行きます。そうすると最後には、2. における基点より右側では dot はなくなり、すべてカッコに書き換わったことになります。
- さて、5. までで式中の 2. における基点の右側では、dot はすべてカッコへと書き換わりました。今度は、その基点の左側に、dot がないか調べます。もしも左側に dot がなければ、この時点で 1. から始めた最初の式はすべてカッコ付きの式に書き換わったことになります。しかし 2. における基点の左側に dot があれば 1. から始めて、式の右側でしたのと同じことを左側で繰り返します。これが終われば式中最初の基点の両側にあった dot がすべてカッコに書き換わります。以上の process を経ると、式に元あった dot はすべてカッコ (または連言記号) へと変換できたことになります。
以上が、式を読み解く際の大体の方針です。ここまで読まれて、詳細はわからなかったかもしれません。それで構いません。ここまでは大まかにお分かりいただければ充分です。Point となるのは次のことです。常に最大 dot 数の箇所を確認し、それがどのような記号のどちら側に付いており、それに従って式の右なり左なりに走査を進め、最大 dot 数よりも多くの数の dot が出てくるか、同数のものが出てくるか、少数のものが出てくるか、もはや全く出てこないか、これらを順に確認しながら、一つ一つ dot をしらみつぶしにカッコ (または連言記号) へと書き換えて行く、というのが大まかなイメージです。こうして大体の感じをつかんでいただければ、この後は、実例を使って具体的に詳細を詰めて行きましょう。
なお、以下での実例を使った解説では、非常にくどく dot のカッコへの書き換えを説明しています。その説明はものすごくくどく感じられることと思います。しかしそれについてはこのようにお考えいただければと思います。例えば、英語を母語としていない者が、大きくなってから、'This is a pen.' を理解するのに、次のように説明されることがあります。'This is a pen.' では 'This' が指示代名詞で主語となっており、'is' が動詞で、特に be 動詞の現在形三人称単数を表す補語を取る動詞であり、'a' は不定冠詞でこの後に続く語が子音で始まっているので 'an' ではなく 'a' であり、'pen' は一般名詞であって、'a pen' で補語となっている、等々というようにです。英語がある程度読めるようになってからは、このような説明は、非常にくどく感じられますが、母語以外の言語を大きくなってから効率的に習得、理解したい場合には、最初の段階では必要なくどさだと思われます。以下の説明もひどくくどいですが、初めの段階では必要なくどさだと考えて、お付き合いいただければと思います。特に Principia の式を全く読んだことのない方や、全く読めない方は、省略することなく読まれることをお勧め致します。そして、できるだけ、三回ぐらいは繰り返してゆっくりと読み直されるとよいと思います。一回だけあわてて読んでも充分呑み込めない可能性が大きいです。
実例 (I) *1
- ⊢ : p ∨ q .⊃. q ∨ p (Ia)
(この式の右端の '(Ia)' は、この式の名前で、便宜的に私が付けたものです。以下同様です。)
さて、この式の dot をカッコに変換する際、最初にこの式のどこに着目すればよいでしょうか。それは dot が最も多く打たれているところです。この式では三箇所、dot が打たれているところが出てきます。式を左から見た時、第一番目に出てくるのが2点 dot, 第二番目に出てくるのが1点 dot, 第三番目に出てくるのが1点 dot です。したがって第一番目に出てくる dot がこの式で最大 dot 数の箇所です。ここがこの式を解析するための基点となります。以下では式中の dot を指示する場合、左から/先頭から「第 n 番目の dot 」という言い方をします。
今、基点がわかりました。Principia ではdot はカッコか連言を表します。それではこの基点は、カッコでしょうか、連言でしょうか。それはその dot がどのような記号の横に置かれているかを見ればわかります。この基点を見ると、それは '⊢' という主張記号の横、および 'p' という変項の横に置かれています(主張記号は、その記号の後の式が真であることを表すための記号です)。Dot がカッコか、連言かを決める条件を一般的に言うと、次のようになります。但し、大変ややこしいので、ここの部分は初めはさらっと読むだけにして、深く考え込まないようにして下さい。最初はよくわからないと思いますが、慣れると違いがわかってきます。
Dot がカッコの場合と連言の場合
- Dot の右横にしろ左横にしろ少なくとも一方の側に選言 ∨、同値 ≡、含意 ⊃、定義の等号 ＝ … Df が来ていれば、その dot はカッコ。
- また dot の左横に量化子 (x), (∃x), (x, y), (∃x, y), …, 確定記述句の scope indicator [ ( ιx )( φx ) ], 主張記号 ⊢ が来ていれば、その dot はカッコ*2。
- それに対し、右横にしろ左横にしろどちら側にも選言、同値、含意、定義の等号が来ておらず、かつ左横に量化子、確定記述句の scope indicator, 主張記号が来ていない場合には連言。
- また左横に選言、同値、含意、定義の等号、主張記号、量化子、記述句の scope indicator のどれもが来ておらず、かつ右横に量化子、否定記号、記述句の scope indicator, 変項のいずれかが来ていれば、連言。
- 左横に自由変項か量化子に束縛された変項か否定記号を前置した変項があり、かつ右横に自由変項または量化子または記述句の scope indicator, または否定記号が来ていれば連言。
- 両横に自由変項があれば連言。
一部重複した記述になっています。何のことかわからないと思います。取り合えず詳細を記したまでですので、この後、長く続く様々な解説中で、よくわからなかったり、詳しく理解したい場合に、ここに戻ってきて確認してみて下さい。普段はこのような複雑なことは覚えなくても構いません。覚えなくても慣れるとこのような複雑なことを逐一思い出さずに、自然と簡単に式が読めるようになります。そこで今の表をもう少し覚えやすいよう簡略化したものを掲げてみます。
簡略版: Dot がカッコの場合と連言の場合
(ア) 否定を除く命題結合子が横にあればカッコ。
(イ) 定義の等号、主張記号という特殊な記号が横にあればカッコ。
(ウ) 左横に量化子、記述句の scope indicator があればカッコ。
(エ) 両横に変項があれば連言。
(オ) 左横に変項があって、かつ右横に変項または量化子または記述句の scope indicator または否定記号があれば連言。
大よそを簡単に言えば以上の通りです。
だいぶ横道にそれましたが、式 (Ia) に戻ります。
- ⊢ : p ∨ q .⊃. q ∨ p (Ia)
この式の第一番目の2点 dot が基点であり、これがカッコか連言か、どちらを表しているのかを調べているのでした。今、この基点を見ると、横に主張記号があります。これは先ほどの簡略版の表の (イ) に当たります (以下、簡略版の表を「簡略表」と略記します)。そのためこの点はカッコを表します。
ではこれは右に開いたカッコでしょうか。左に開いたカッコでしょうか。そのことは基点が今の主張記号の右横に置かれているのか、左横に置かれているのかによってわかります。今、基点は主張記号の右側に置かれています。ということは、この基点は右に開いたカッコだということです。そこで先ほどの式は以下のように書き直されます。
- ⊢ ( p ∨ q .⊃. q ∨ p (Ib)
次に、この右に開いたカッコはどこで閉じるでしょうか。カッコに書き直される前の dot は2点 dot でした。カッコから右へと走査を進める中で、2点より大きい数の dot に出会えば、そこでいわば自動的にカッコは閉じます。2点と同数の dot が出てくれば、そこで閉じたり閉じなかったりします。1点の dot しか出てこなければ、そのような1点 dot の箇所ではカッコは閉じないので、1点 dot が出てきても、それは無視して走査を進めます。そしてもしももはや全く dot が出てこなければ、式の終端でカッコは閉じられます。
(Ib) を見ると、右に開いたカッコの後に出てくるのは、1点 dot だけです。これらを無視して走査を進めると、式の終端に至ります。したがって、(Ib) の右に開いたカッコは、その式の終端で閉じられます。
- ⊢ ( p ∨ q .⊃. q ∨ p ) (Ic)
次に (Ic) 中の 'p ∨ q .⊃. q ∨ p' を見てみましょう。ここではどこに最大の dot 数の箇所が出てくるでしょうか。それは1点 dot が第一番目と第二番目に複数箇所出てきます。この場合、どちらの dot を新たな基点に取っても構いません。そこで第一番目の dot を基点に取りましょう。それではこの dot はカッコでしょうか、連言でしょうか。この基点の横には含意記号があります。そのため上記の簡略表の (ア) に当たります。よってこの基点はカッコを表します。
ではこの基点は右に開いたカッコでしょうか。左に開いたカッコでしょうか。この基点は含意記号の左に置かれていますから、左に開いたカッコです。したがって、(Ic) は以下のように書き換えられます。
- ⊢ ( p ∨ q ) ⊃. q ∨ p ) (Id)
さて、今書いた左に開いたカッコはどこで閉じるでしょうか。この左に開いたカッコを左へと走査して行くと、最初の (Ia) に見られるように、元2点 dot があった箇所に至ります。カッコを表す基点は、その基点より大きな数の dot に出会ったならば、そこでいわば自動的に閉じるのでした。(Id) の左に開いたカッコは、1点 dot の基点だったので、この左に開いたカッコは元2点 dot があった箇所で閉じます。したがって (Id) は次のように書き直されます。
- ⊢ ( ( p ∨ q ) ⊃. q ∨ p ) (Ie)
それでは、(Ie) の残った1点 dot はカッコでしょうか、連言でしょうか。この基点の横には含意記号があります。そのために上記簡略表の (ア) に当たるため、この基点はカッコを表しています。では、どちらに開いたカッコでしょうか。この基点は含意記号の右側に打たれています。したがってこの基点は右に開いたカッコを表します。そこで、(Ie) は次のようになります。
- ⊢ ( ( p ∨ q ) ⊃ ( q ∨ p ) (If)
今、右に開いて書いたカッコはどこで閉じるでしょうか。元々の式 (Ia) を見ると、今右に開いて書いたカッコの後には dot はありませんでした。したがってこの右に開いたカッコは文末で閉じます。よって (If) は以下のように書き換えられます。
- ⊢ ( ( p ∨ q ) ⊃ ( q ∨ p ) ) (Ig)
以上で dot からカッコへの書き換えはすべて終了しました。
この後、六つの実例を通じて dot による式の、カッコへの書き換えを解説し、最後に練習問題を掲げています。日記の項目としては、非常に長い記述が続くので、さらに続けてお読みになりたい方は、お時間の余裕を取ってから読み進めて下さい。
実例 (II) *3
- ⊢ :: p ∨ q .⊃:･ p .∨. q ⊃ r :⊃. p ∨ r (IIa)
さて、この式の dot をカッコに書き換えるには、まずどこに注目すればよいでしょうか。それは式中で最大数の dot があるところです。それは式中の第一番目の dot です。それではこの dot はカッコでしょうか、連言でしょうか。これは主張記号の横にあります。簡略表によるならば、これはその表の (イ) に当たります。したがってこの dot はカッコです。では右に開いたカッコでしょうか、左に開いたカッコでしょうか。それは、主張記号の右側に置かれているので、右に開いたカッコです。
- ⊢ ( p ∨ q .⊃:･ p .∨. q ⊃ r :⊃. p ∨ r (IIb)
では何点の dot でしょうか。4点です。それではこの dot を基点にして、右側へと式の走査を進めます。基点は4点でしたので、4点より大きい dot が出てくるか、4点と同数の dot が出てくるか、4点より少数の dot が出てくるか、あるいはもはや dot は全く出てこないか、いずれの場合が生じているのかに注意しながら、走査してみます。すると dot は出てくるものの、どれも4点より少数のものしか出てきません。基点より大きい数が出てきたら、そこでカッコは閉じます。同数のものが出てきたら、その dot がどんな記号の横にあるかに応じてカッコは閉じたり閉じなかったりします。基点より少数の dot が出てくる場合は、そこではカッコは閉じませんので、その dot は無視して走査を続けます。そしてそのまま文末へと至ってしまったならば、文末でカッコは閉じられることになります。今の場合、4点より少数の dot しか出てこないまま、文末へと至っています。したがって (IIb) は、その基点以降、文末でカッコが閉じられます。
- ⊢ ( p ∨ q .⊃:･ p .∨. q ⊃ r :⊃. p ∨ r ) (IIc)
次に (IIc) 中のカッコ内を見てみましょう。ここにはまだ dot が残っていますので、これらをカッコに書き換えねばなりません。まずはどこに注目すべきでしょうか。最大の dot 数のところです。それは第二番目の dot です。これはカッコでしょうか、連言でしょうか。今の場合、横に含意記号があります。簡略表では、これはその (ア) に当たります。したがってこの dot はカッコです。では右に開いたカッコでしょうか、左に開いたカッコでしょうか。この dot は含意記号の右に置かれているので、右に開いたカッコです。
- ⊢ ( p ∨ q .⊃ ( p .∨. q ⊃ r :⊃. p ∨ r ) (IId)
それでは、この右向きのカッコはどこで閉じるでしょうか。ここを基点にして右側に走査を進めます。この基点は何点だったでしょうか。3点です。そのため、3点よりも大きいものが出てくるか、同数のものが出てくるか、3点よりも小さいものが出てくるか、あるいはまったく出てこないか、これらに気を付けながら走査します。3点よりも大きいものがあれば、そこでカッコは閉じます。同数のものがあれば、横に何が置かれているかによって閉じたり閉じなかったりします。小さいものしか出てこなければ、それを無視して走査を進めます。基点以降、dot が全く出てこない場合は文末でカッコを閉じます。今の3点基点以降、右側では3点よりも小さいものしか出てきません。したがってそれらを無視して文末まで行ってそこでカッコを閉じます。
- ⊢ ( p ∨ q .⊃ ( p .∨. q ⊃ r :⊃. p ∨ r ) ) (IIe)
次に、今閉じたカッコ内を見てみましょう。今度はどこに注目すべきでしょうか。最大 dot 数のところです。それは今閉じたかカッコ内で第三番目のところです。それではその dot はカッコでしょうか、連言でしょうか。それは含意記号の横にあります。よって簡略表の (ア) によりカッコです。では右向きのカッコでしょうか、左向きのカッコでしょうか。含意記号の左に打たれていますので、左向きのカッコです。
- ⊢ ( p ∨ q .⊃ ( p .∨. q ⊃ r ) ⊃. p ∨ r ) ) (IIf)
それでは今の左向きのカッコはどこで閉じるでしょうか。このカッコは2点 dot です。したがって2点より大きいか、同数か、より少ないか、全く出てこないか、いずれなのかに注意しながら、左に走査を進めます。するとより少ない1点 dot に二回出会った後、最初の式 (IIa) に戻って見てみるならば、元3点 dot があった地点に至ります。したがってここで左向きのカッコは閉じます。
- ⊢ ( p ∨ q .⊃ ( ( p .∨. q ⊃ r ) ⊃. p ∨ r ) ) (IIg)
さて、今閉じたカッコの中 'p .∨. q ⊃ r' を見てみます。どこに注目すべきでしょう。最大の dot のところです。この場合、最大は1点で、それが二箇所出てきます。どちらを先に取り扱っても差し当たり構いません。第一番目の dot から行きましょう。これはカッコでしょうか、連言でしょうか。横に選言記号があります。これは簡略表によると、その (ア) になります。よってこの dot はカッコです。さらに選言記号の左にあるので、左に開いたカッコです。
- ⊢ ( p ∨ q .⊃ ( ( p ) ∨. q ⊃ r ) ⊃. p ∨ r ) ) (IIh)
この左カッコはどこで閉じるでしょうか。今の基点は1点です。何点の dot が出てくるか注意しながら左へ走査します。すると、最初の式 (IIa) に戻って見てみるならば、元3点の dot があったところに至ります。よってここで左カッコは閉じます。
- ⊢ ( p ∨ q .⊃ ( ( ( p ) ∨. q ⊃ r ) ⊃. p ∨ r ) ) (IIi)
続いて '( p ) ∨. q ⊃ r' の1点 dot です。これは選言記号の横に置かれているのでカッコです。また右横に置かれているので右カッコです。
- ⊢ ( p ∨ q .⊃ ( ( ( p ) ∨ ( q ⊃ r ) ⊃. p ∨ r ) ) (IIj)
右に走査を進めると、最初の (IIa) を見るならば、元2点 dot があった含意記号の左横に行き着きます。したがってここで右向きのカッコは閉じられます。
- ⊢ ( p ∨ q .⊃ ( ( ( p ) ∨ ( q ⊃ r ) ) ⊃. p ∨ r ) ) (IIk)
次に、(IIk) 中、第二番目の dot を見てみましょう。それは含意記号の右横にある1点 dotです。よってこれは右カッコです。
- ⊢ ( p ∨ q .⊃ ( ( ( p ) ∨ ( q ⊃ r ) ) ⊃ ( p ∨ r ) ) (IIl)
これを基点に右へ走査します。すると最初の (IIa) を見るならば、そのまま文末へと至ります。したがって文末でカッコは閉じられます。
- ⊢ ( p ∨ q .⊃ ( ( ( p ) ∨ ( q ⊃ r ) ) ⊃ ( p ∨ r ) ) ) (IIm)
最後に残った dot を見てみましょう。これは1点の dot で、含意記号の左にありますから、左に開いたカッコです。
- ⊢ ( p ∨ q ) ⊃ ( ( ( p ) ∨ ( q ⊃ r ) ) ⊃ ( p ∨ r ) ) ) (IIn)
そこで左へと走査しますと、元4点あった主張記号の右横に至ります。したがってそこでカッコは閉じます。
- ⊢ ( ( p ∨ q ) ⊃ ( ( ( p ) ∨ ( q ⊃ r ) ) ⊃ ( p ∨ r ) ) ) (IIo)
以上ですべての dot を書き換えることができました。
実例 (III) *4
- ⊢ :･ p . q .⊃. r :≡: p . ~r .⊃. ~q (IIIa)
まず、最大 dot 数のところを確認します。それは第一番目の dot で3点です。横に主張記号が来ているので、この dot はカッコであり、しかも主張記号の右に置かれているので、右に開いたカッコです。
- ⊢ ( p . q .⊃. r :≡: p . ~r .⊃. ~q (IIIb)
この基点となる3点 dot から右に走査し、3点より大きい dot も、同数の dot も出てこないので、文末でカッコを閉じます。
- ⊢ ( p . q .⊃. r :≡: p . ~r .⊃. ~q ) (IIIc)
次にカッコ内で最大の dot を確認すると、2点 dot が二箇所出てきます。この場合、どちらを先に取り上げてもいいのですが、初めに出てくる方から処理しましょう。その2点 dot は同値記号の横に出てきます。簡略表によると、これはその (ア) に相当するので、これはカッコです。しかも左横に来ているので左向きのカッコです。
- ⊢ ( p . q .⊃. r ) ≡: p . ~r .⊃. ~q ) (IIId)
この左カッコは2点 dot であり、左に走査すると、最初の (IIIa) を見れば主張記号横の3点 dot に突き当たりますので、そこでこの左カッコを閉じます。
- ⊢ ( ( p . q .⊃. r ) ≡: p . ~r .⊃. ~q ) (IIIe)
今閉じたカッコ内を見てみましょう。最大の dot は1点で三箇所出てきます。この場合、命題結合子の横にある dot から処理することが得策です。否定を除く命題結合子 (や定義を表す等号) の横にある dot の方が、一般的により広いカッコを表しているからです。より広いカッコから、その中のより狭いカッコへと変換を順次処理して行きましょう。そうすると、今のカッコ内にある命題結合子の横の dot とは、第二番目と三番目の dot です。そこで二番目から行きましょう。この dot は含意記号の左横にあるので左カッコです。
- ⊢ ( ( p . q ) ⊃. r ) ≡: p . ~r .⊃. ~q ) (IIIf)
そこから左に走査して行くと、同数の1点 dot に出会います。より多くの dot に出会った時は、そこでカッコは閉じます。より少ない dot に出会った時は、そこではカッコは閉じません。同数の dot に出会ったなら、そこでカッコが閉じたり閉じなかったりします。閉じるか閉じないかは、基点となっている dot がどのような記号の横にあるのかということと、その出会った dot がどのような記号の横にあるのかということを、見比べることによって決まります。この比較には次の法則があります。
Dot の強弱を表す不等式
連言 ＜ 量化子または記述句の scope indicator ＜ (否定を除く) 命題結合子または定義のための等号
基点と、出会った dot を比べてみて、例えば基点が連言の dot であり、出会った点が 量化子の (左横ではなく) 右横にある dot ならば、そこで基点から開いているカッコは閉じます。この場合は、「連言 ＜ 量化子または記述句の scope indicator 」の不等式における左辺と右辺との比較に相当し、この左辺が基点で右辺が出会った点ならば、左辺より右辺の方が強いとして、右辺の点の箇所でカッコを閉じるということです。
また例えば基点が量化子の (左横ではなく) 右横にある dot であり、出会った dot が (否定を除く) 命題結合子のどれかの横であったならば、そこで基点から開いているカッコは閉じます。この場合は、「量化子または記述句の scope indicator ＜ (否定を除く) 命題結合子または定義のための等号」の不等式における左辺と右辺の比較に当たり、左辺より右辺の方が強いので、量化子右のカッコは命題結合子の dot の箇所で閉じるということです。
また、基点と、出会った点の関係が、上記不等式の左辺と右辺との関係ではなく、例えば基点が命題結合子の点で、出会った点も命題結合子の点というように、不等式中の一辺に終始している関係ならば、あるいは言い換えると同じ強さの点同士ならば、出会った点のところでカッコは閉じます。
これに対し、例えば基点が命題結合子の点で、出会った点が連言を表す点ならば、命題結合子の点の方が強く、連言の点の方が弱いので、出会った連言の点の箇所ではカッコは閉じません。
つまり以上を手短にまとめると、
同数の dot 同士については、基点から、出会った点に向かって、弱い方から強い方へ至る場合と、同等から同等へと至る場合はカッコは閉じます。強い方から弱い方は閉じません。
ここで式 (IIIf) に戻ってみましょう。
- ⊢ ( ( p . q ) ⊃. r ) ≡: p . ~r .⊃. ~q ) (IIIf)
今問題にしていたのは、最初に出てくる含意記号左横の左カッコがどこで閉じるのかでした。このカッコを左に走査して行くと同数の1点 dot に出会い、ここで閉じるのかどうかを考えていました。さて、この出会った1点 dot はカッコでしょうか、連言でしょうか。両脇から変項によって挟まれています。この場合、簡略表の (エ) によると連言です。したがってこの dot は連言です。よって次のように書かれます。
- ⊢ ( ( p ∧ q ) ⊃. r ) ≡: p . ~r .⊃. ~q ) (IIIg)
この連言のところで先ほどからの左カッコは閉じるのでしょうか。Dot の強弱を表す不等式
連言 ＜ 量化子または記述句の scope indicator ＜ (否定を除く) 命題結合子または定義のための等号
によると、今の場合、含意記号という命題結合子横の dot から連言を表す dot へと至っています。したがって dot の強弱を表す不等式中で
連言 ＜ …＜ (否定を除く) 命題結合子または定義のための等号
この右辺から左辺へと至る関係が成り立っているということです。この右辺の方が強く、左辺の方が弱いのでした。そして強い方から弱い方へ至っている場合は、そこではカッコを閉じないのでした。したがって含意記号左横の左カッコは連言を表す dot の箇所では閉じません。閉じずに左へと走査を進めます。すると、元3点 dot のあった主張記号の右横へと至ります。3点の方が1点よりも大きいので左カッコはここで閉じます。
- ⊢ ( ( ( p ∧ q ) ⊃. r ) ≡: p . ~r .⊃. ~q ) (IIIh)
ところで、連言を表す dot は、連言のみを表しているのではなく、カッコをも表しています。そこで連言であるこの1点 dot のカッコもきちんと記す必要があります。連言を表す dot は、その両側へカッコが開いている点が異なるだけで、その他は通常のカッコだけを表す dot と同様の方法でカッコに直せば構いません。そうすると今の連言の1点 dot はその両側の 'p' と 'q' に向かって開いていることになります。'∧' の両側へ開いているカッコを、まず同時に二つ記してみましょう。
- ⊢ ( ( (p) ∧ (q ) ⊃. r ) ≡: p . ~r .⊃. ~q ) (IIIi)
'∧' の左に追記した左カッコはどこで閉じるでしょうか。(IIIa) に戻ると、その左カッコは主張記号横の3点 dot に突き当たります。1点の連言 dot より、3点の方が大きいので、そこでカッコを閉じます。
- ⊢ ( ( ( (p) ∧ (q) ⊃. r ) ≡: p . ~r .⊃. ~q ) (IIIj)
今度は '∧' の右に追記した1点 dot であった右カッコはどこで閉じるでしょうか。この1点 dot を基点として右へ走査しますと、(IIIa) を見るなら、含意記号の左横の同数の dot に行き当たります。同数の dot に出会ったなら、そこでカッコが閉じたり閉じなかったりしたのでした。閉じるか閉じないかは、基点となっている dot がどのような記号の横にあるのかということと、その出会った dot がどのような記号の横にあるのかということを、見比べることによって決まりました。(IIIj) の式を見てみますと、この式の1点 dot であった連言記号 '∧' の右横で、右に開いたカッコを右に走査すると、同数の dot に含意記号の左横で出会ったのでした。さて今、基点となった dot は両側に変項のみが来ている連言を表す dot でした。そして出会った dot は含意記号の横にありました。したがってこの同数同士の dot は、dot の強弱を表す不等式中の左端の辺と右端の辺の関係に当たります。
連言 ＜ … ＜ (否定を除く) 命題結合子または定義のための等号
そうするとこれは弱い方から強い方への関係なので、出会った dot である含意記号の左横で閉じることになります。
- ⊢ ( ( ( (p) ∧ (q) ) ⊃. r ) ≡: p . ~r .⊃. ~q ) (IIIk)
次に、この式の同値記号の左側にある1点 dot を片付けましょう。この dot は含意記号の右横にあるので、右に開いたカッコです。
- ⊢ ( ( ( (p) ∧ (q) ) ⊃ ( r ) ≡: p . ~r .⊃. ~q ) (IIIl)
この右カッコは初めの (IIIa) によれば、右に進んで同値記号の左横で2点 dot と出会いますので、そこで閉じます。
- ⊢ ( ( ( (p) ∧ (q) ) ⊃ ( r ) ) ≡: p . ~r .⊃. ~q ) (IIIm)
今度は同値記号の右側を処理しましょう。この右側で最大の dot は第一番目に出てくる2点 dot です。これは同値記号の右横に出てくるので、右カッコです。
- ⊢ ( ( ( (p) ∧ (q) ) ⊃ ( r ) ) ≡ ( p . ~r .⊃. ~q ) (IIIn)
今の右カッコは2点 dot でした。右に進んでも2点以上の dot は出てきません。したがって文末で閉じます。
- ⊢ ( ( ( (p) ∧ (q) ) ⊃ ( r ) ) ≡ ( p . ~r .⊃. ~q ) ) (IIIo)
今度は今閉じたカッコ内の最大 dot を見てみましょう。それは1点 dot で三箇所あります。否定記号を除いた命題結合子の隣にある dot の方から処理するのがよいのでした。そこで第二番目の dot から行きます。これは含意記号の左にあるので左カッコです。
- ⊢ ( ( ( (p) ∧ (q) ) ⊃ ( r ) ) ≡ ( p . ~r ) ⊃. ~q ) ) (IIIp)
そこでこの1点 dot を基点に左へ走査しますと、同数の dot に出会います。同数の場合は先の不等式に従って閉じたり閉じなかったりするのでした。つまり基点から出会った点に向かって、弱い方から強い方へ至る場合と、同等から同等へと至る場合は閉じたのでした。強い方から弱い方は閉じないのでした。今の場合は含意記号から連言記号へという、強い方から弱い方への関係が成り立っています。ということはこの出会った dot のところでは閉じないということです。そのためこの出会った1点 dot は無視して走査を進めます。すると同値記号の右横で元2点であった箇所に行き着きます。したがってここでカッコが閉じます。
- ⊢ ( ( ( (p) ∧ (q) ) ⊃ ( r ) ) ≡ ( ( p . ~r ) ⊃. ~q ) ) (IIIq)
次に今閉じたカッコ内を見ましょう。この1点 dot は連言でしょうか、カッコでしょうか。先にも述べた通り、これは連言でした。と言うのも、その左横に変項があり、右横に否定記号があります。これは前に掲げた簡略表の (オ) に当たります。そのためこの dot は連言となるからです。
- ⊢ ( ( ( (p) ∧ (q) ) ⊃ ( r ) ) ≡ ( ( p ∧ ~r ) ⊃. ~q ) ) (IIIr)
そして連言の dot はカッコも両側へ向かって伴っているのでした。今の dot は1点でしたので、この連言から左に向かって開いているカッコは、同値記号の右側の2点 dot に出会ってそこで閉じます。
- ⊢ ( ( ( (p) ∧ (q) ) ⊃ ( r ) ) ≡ ( ( (p) ∧ ~r ) ⊃. ~q ) ) (IIIs)
そして連言の右に開いたカッコは、
- ⊢ ( ( ( (p) ∧ (q) ) ⊃ ( r ) ) ≡ ( ( (p) ∧ (~r ) ⊃. ~q ) ) (IIIt)
右に行くと含意記号の左横で同数の1点 dot に出会います。先ほどからの不等式によると、ここでは「連言 ＜ … ＜ 命題結合子」が成り立ちます。つまり弱い方から強い方へと至っていますので、含意記号の左で出会った dot のところでカッコは閉じます。
- ⊢ ( ( ( (p) ∧ (q) ) ⊃ ( r ) ) ≡ ( ( (p) ∧ (~r ) ) ⊃. ~q ) ) (IIIu)
最後に残った1点 dot を処理しましょう。これは含意記号の右横にあるので、右に開いたカッコです。このカッコはもはや dot に出会うことなく文末に至ります。よってこの右カッコは文末で閉じます。
- ⊢ ( ( ( (p) ∧ (q) ) ⊃ ( r ) ) ≡ ( ( (p) ∧ (~r ) ) ⊃ ( ~q) ) ) (IIIv)
これで完成しました。
実例 (IV) *5
- ⊢ :･ (x).φx : (x).ψx :⊃. (x).φx .ψx (IVa)
続いて量化子が含まれる式を見てみましょう。
最大 dot 数の箇所は第一番目の3点 dot で、主張記号の右にあることから右に開いたカッコであり、
- ⊢ ( (x).φx : (x).ψx :⊃. (x).φx .ψx (IVb)
3点以上の dot は、もはや式中に含まれていないことから、式の終端でカッコは閉じます。
- ⊢ ( (x).φx : (x).ψx :⊃. (x).φx .ψx ) (IVc)
この式中の最大 dot 数は 2 で、それは二箇所あり、その二箇所中後者の方が命題結合子の横にあるので、この後者の dot を処理するならば、それは含意記号の左にあるから左カッコであり、
- ⊢ ( (x).φx : (x).ψx ) ⊃. (x).φx .ψx ) (IVd)
この2 点 dot である左カッコは左に行くと、同数の2点 dot に出会います。出会った2点 dot を見ると、左に変項があり、右に量化子があります。ということは、この2点 dot は簡略表によると、その (オ) に当たり、連言だとわかります。
- ⊢ ( (x).φx ∧ (x).ψx ) ⊃. (x).φx .ψx ) (IVe)
同数の dot に出会った場合は、基点と出会った点を比べて、カッコを閉じるか閉じないかを判断するのでした。今、基点は含意記号の横にあり、出会った点は連言でした。そうすると、dot の強弱を表す不等式によると、強い方から弱い方へと至っており、その場合はカッコを閉じないのでした。したがって、(IVd) または (IVe) 中の、含意記号の左で左に開いたカッコは、その左の連言を表す2点 dot の箇所では閉じず、そのまま左へ走査を進めればよいということです。そしてそのまま走査して行くと、(IVa) において元3点 dot のあった主張記号右横に至り、そこでカッコは閉じます。
- ⊢ ( ( (x).φx ∧ (x).ψx ) ⊃. (x).φx .ψx ) (IVf)
さて、連言にもカッコが伴われているのでした。今の連言の両側に、それぞれ開いたカッコを付けましょう。
- ⊢ ( ( (x).φx ) ∧ ( (x).ψx ) ⊃. (x).φx .ψx ) (IVg)
この連言は2点 dot でした。今、左に開いて書いたカッコは、どこで閉じるでしょうか。左に走査しますと、元3点あった主張記号の右横に至ります。したがって、今、左に開いて書いたカッコはここで閉じます。
- ⊢ ( ( ( (x).φx ) ∧ ( (x).ψx ) ⊃. (x).φx .ψx ) (IVh)
一方、今しがた、右に開いて書いた連言横のカッコはどこで閉じるでしょうか。その連言は2点でした。ここから右に走査しますと、元2点であった同数の dot に含意記号左横で出会います。同数の dot に出会った場合は、それぞれの dot がどのような記号の横にあるかを見て、その強さを比べればよいのでした。今の場合、基点は連言で、出会った点は含意記号の横にあります。そうすると以前に掲げた不等式によると、弱い方から強い方へと至っていることがわかります。その場合はカッコを閉じるのでした。よって今の出会った dot の箇所で、連言の右に開いたカッコは閉じるということです。
- ⊢ ( ( ( (x).φx ) ∧ ( (x).ψx ) ) ⊃. (x).φx .ψx ) (IVi)
次に、この式の含意記号の左辺には1点 dot が二箇所ありますが、第一番目から処理しますと、この dot は左に量化子があるので、簡略表の (ウ) に相当するため、カッコです。しかも量化子の右にあるため右カッコです。
- ⊢ ( ( ( (x)( φx ) ∧ ( (x).ψx ) ) ⊃. (x).φx .ψx ) (IVj)
このカッコは1点 dot であり、右に進むと2点の連言 dot に出会います。出会った dotの方が大きいので、カッコをこの箇所で閉じます。
- ⊢ ( ( ( (x)( φx ) ) ∧ ( (x).ψx ) ) ⊃. (x).φx .ψx ) (IVk)
そしてこの式の第一番目の1点 dot は先ほどと同じく量化子の右横にあるので右に開いたカッコであり、
- ⊢ ( ( ( (x)( φx ) ) ∧ ( (x)( ψx ) ) ⊃. (x).φx .ψx ) (IVl)
右に進むと元2点 dot であった含意記号の左の箇所に至りますので、そこでカッコを閉じます。
- ⊢ ( ( ( (x)( φx ) ) ∧ ( (x)( ψx ) ) ) ⊃. (x).φx .ψx ) (IVm)
次に、残った1点 dot 三箇所のうち、第一番目のものが命題結合子の横にあるので、これを処理するならば、含意記号の右にあるので右カッコであり、
- ⊢ ( ( ( (x)( φx ) ) ∧ ( (x)( ψx ) ) ) ⊃ ( (x).φx .ψx ) (IVn)
この右側に出てくる1点 dot は量化子右横のカッコを表す dot と、変項に挟まれた連言を表す dot であり、同数の dot の強弱を表す不等式によるならば、命題結合子横の dot の方が、量化子横や連言の dot よりも強いので、含意記号右横の右カッコは式の終端で閉じます。
- ⊢ ( ( ( (x)( φx ) ) ∧ ( (x)( ψx ) ) ) ⊃ ( (x).φx .ψx ) ) (IVo)
そして今述べたように、残りのそれぞれの dot は量化子横の右カッコと連言なので、
- ⊢ ( ( ( (x)( φx ) ) ∧ ( (x)( ψx ) ) ) ⊃ ( (x)( φx ∧ ψx ) ) (IVp)
となり、今付けた量化子右横の右カッコは、同数でありながら最も力の弱い連言の 1点 dot を越えて式の終端で閉じます。
- ⊢ ( ( ( (x)( φx ) ) ∧ ( (x)( ψx ) ) ) ⊃ ( (x)( φx ∧ ψx ) ) ) (IVq)
次に、今の連言の両側に伴う開いたカッコを付けます。
- ⊢ ( ( ( (x)( φx ) ) ∧ ( (x)( ψx ) ) ) ⊃ ( (x)( φx ) ∧ ( ψx ) ) ) (IVr)
左側に付けた開いたカッコは、左に行って元同数の1点 dot に量化子の右横で出会います。同数の場合、以前からの不等式によると、連言よりも量化子横の点の方が強いのでした。したがって出会った点の箇所で、今のカッコは閉じます。
- ⊢ ( ( ( (x)( φx ) ) ∧ ( (x)( ψx ) ) ) ⊃ ( (x)( ( φx ) ∧ ( ψx ) ) ) (IVs)
最後に、今述べている連言右の右に開いたカッコは、その右側にもはや dot がないので、式の終端で閉じます。
- ⊢ ( ( ( (x)( φx ) ) ∧ ( (x)( ψx ) ) ) ⊃ ( (x)( ( φx ) ∧ ( ψx ) ) ) ) (IVt)
これで終了です。
実例 (V) *6
- φx .≡x. ψx :=: (x):φx .≡. ψx Df (Va)
今度は定義式、定義のための等号を含む式をやってみましょう。
式の右側に 'Df' とあれば、それは定義を行っている式です。そのため式中には等号があるはずで、その等号の左の記号を右の記号で定義しています。したがって定義式では、この等号が式中で最も大きな切れ目となっていますから、定義式が現れたら、まず等号を探します。上記の式を見ると真ん中辺りに等号が出てきます。これが式中で最も大きな切れ目です。この等号の両脇には、この式中で最も大きな数の2点 dot があります。まずは左の2点 dot から処理しましょう。これは等号の左にあることから、簡略表の (イ) により、カッコでしかも左カッコです。
- φx .≡x. ψx ) =: (x):φx .≡. ψx Df (Vb)
この左カッコの左側にはもう2点以上の dot はないので、式の端でカッコを閉じます。
- ( φx .≡x. ψx ) =: (x):φx .≡. ψx Df (Vc)
このカッコ内を見ますと1点 dot が二箇所あります。第一番目から処理しますと、同値記号の左にあるので左カッコであり、その左には dot はないので式の端でカッコを閉じます。
- ( ( φx )≡x. ψx ) =: (x):φx .≡. ψx Df (Vd)
カッコ内のもう一つの1点 dot を処理しますと、その左に下付きの変項が見えます。下付きの変項はカッコを付ける際はないものとして無視して下さい。これは便宜的な省略記号なので、式にとって差し当たり本質的ではないことから無視してしまい、その上でこの1点 dot を見ますと、dot は同値記号の右にあることから右に開いたカッコであり、右に走査すると元2点であった等号左の箇所に至るのでそこでカッコを閉じます。
- ( ( φx )≡x( ψx ) ) =: (x):φx .≡. ψx Df (Ve)
これで等号の左辺はできました。今度はその右辺を見ますと最大 dot に2点のものが二箇所あります。等号横の方が広いカッコを表しますので、等号右横の2点 dot を見ると等号の右側にあるので右カッコであり、同数の dot が右の方に出てきますが、以前からの不等式に基付くと、等号横の dot の方が量化子横の dot よりも強いので、量化子横ではカッコは閉じず、そのまま式の終端まで行って閉じます。
- ( ( φx )≡x( ψx ) ) = ( (x):φx .≡. ψx ) Df (Vf)
このカッコ内の最大 dot は2点で量化子の右横にあるから右カッコであり、その右には2点以上は出てこないので、式の終端でカッコを閉じます。
- ( ( φx )≡x( ψx ) ) = ( (x)( φx .≡. ψx ) ) Df (Vg)
今閉じたカッコ内の最大 dot である1点 dot 二箇所は、ともに同値記号の右と左に配されているので、右と左に開いたカッコであり、
- ( ( φx )≡x( ψx ) ) = ( (x)( φx )≡( ψx ) ) Df (Vh)
左に開いたカッコは左に行って量化子前の2点 dot に当たってそこで閉じ、右に開いたカッコは式の終端で閉じます。
- ( ( φx )≡x( ψx ) ) = ( (x)( ( φx )≡( ψx ) ) ) Df (Vi)
これでできました。
この式は等号右の普遍量化子を使って、等号左の式を定義しています。等号左の式の方が少し短めになっています。つまり等号左の式が右の式の省略表現で、等号左の式中の下付きの変項が普遍量化子の簡略な印となっています。等号右の式が出てきたら左の式と、あるいは等号左の式が出てきたら右の式と、入れ替えが可能なことを表しています。
実例 (VI) *7
- ⊢ :･ E! ( ιx )( φx ) .≡: (∃c).φc : φx . φy .⊃x,y. x=y (VIa)
次に確定記述の operator 'ι' を含んだ式に取り組んでみましょう。
(なお、この式の 'E! ( ιx )( φx )' は、φ を満たすただ一つの x が存在する、ということをいみしています。)
さて、この式の最大の dot は3点で一箇所ですからまず
- ⊢ ( E! ( ιx )( φx ) .≡: (∃c).φc : φx . φy .⊃x,y. x=y ) (VIb)
となります。次に最大の dot は2点で二箇所あり、最初の方が同値記号の右にあるので右カッコであり、後の方は連言なので
- ⊢ ( E! ( ιx )( φx ) .≡ ( (∃c).φc ∧ φx . φy .⊃x,y. x=y ) ) (VIc)
となります。
閉じたばかりのカッコ内の元2点 dot は連言で、カッコ内で最も大きい dot なので、ここがこのカッコ内の大きな切れ目であり、ここで連言記号によって左右に式が分かれます。連言記号の左右には、両側に開いたカッコがありましたから、それらのカッコを記します。
- ⊢ ( E! ( ιx )( φx ) .≡ ( (∃c).φc ) ∧ ( φx . φy .⊃x,y. x=y ) ) (VId)
この元2点の連言の左に行くと、同じく元2点の同値記号右にある dot に当たります。連言の方が同値記号よりも弱いので、同値記号の前でカッコを閉じます。
- ⊢ ( E! ( ιx )( φx ) .≡ ( ( (∃c).φc ) ∧ ( φx . φy .⊃x,y. x=y ) ) (VIe)
今度は今の連言の右側へ行くと、二点 dot はもう見当たらないので、文末でカッコを閉じます。
- ⊢ ( E! ( ιx )( φx ) .≡ ( ( (∃c).φc ) ∧ ( φx . φy .⊃x,y. x=y ) ) ) (VIf)
次に '( (∃c).φc )' の dot を見ると、これは右カッコで、この表現の右端にある元2点 dot である連言の箇所で閉じます。
- ⊢ ( E! ( ιx )( φx ) .≡ ( ( (∃c)( φc ) ) ∧ ( φx . φy .⊃x,y. x=y ) ) ) (VIg)
続いて連言の右側の '( φx . φy .⊃x,y. x=y )' を見ると、下付きの変項を無視するなら、含意記号の両横に dot があるので、これらのうち最初の方から処理すると、これは左に開いたカッコで、連言である同数の dot に左で出会いますが、含意記号横の dot の方が連言の dot よりも強いので、連言の箇所では閉じず、左に進んで元2点であった連言の箇所でカッコを閉じます。
- ⊢ ( E! ( ιx )( φx ) .≡ ( ( (∃c)( φc ) ) ∧ ( ( φx . φy ) ⊃x,y. x=y ) ) ) (VIh)
そして下付きの変項横の dot は含意記号の右にあるので右カッコで、これはそのまま右に行って式の終端で閉じます。
- ⊢ ( E! ( ιx )( φx ) .≡ ( ( (∃c)( φc ) ) ∧ ( ( φx . φy ) ⊃x,y ( x=y ) ) ) ) (VIi)
さて、この式の同値記号の右辺には1点 dot が一つ残っています。これは変項に挟まれているので連言です。
- ⊢ ( E! ( ιx )( φx ) .≡ ( ( (∃c)( φc ) ) ∧ ( ( φx ∧ φy ) ⊃x,y ( x=y ) ) ) ) (VIj)
連言は両側に開いたカッコを伴っているのでした。
- ⊢ ( E! ( ιx )( φx ) .≡ ( ( (∃c)( φc ) ) ∧ ( ( φx ) ∧ ( φy ) ⊃x,y ( x=y ) ) ) ) (VIk)
今書き込んだ左に開いたカッコは、左に行って元2点である連言の箇所で閉じます。
- ⊢ ( E! ( ιx )( φx ) .≡ ( ( (∃c)( φc ) ) ∧ ( ( ( φx ) ∧ ( φy ) ⊃x,y ( x=y ) ) ) ) (VIl)
残った右に開いたカッコは、右に行って含意記号左横の同数の元1点 dot に行き着き、連言の方が含意記号よりも弱いので、ここでカッコを閉じます。
- ⊢ ( E! ( ιx )( φx ) .≡ ( ( (∃c)( φc ) ) ∧ ( ( ( φx ) ∧ ( φy ) ) ⊃x,y ( x=y ) ) ) ) (VIm)
あとは最後の dot が一つ残っています。これは同値記号の左にあるので左カッコであり、左には元3点 dot が主張記号の右にありましたから、そこで閉じます。
- ⊢ ( ( E! ( ιx )( φx ) ) ≡ ( ( (∃c)( φc ) ) ∧ ( ( ( φx ) ∧ ( φy ) ) ⊃x,y ( x=y ) ) ) ) (VIn)
これで出来上がりました。
なお、同値記号の右辺の '( ( φx ) ∧ ( φy ) ) ⊃x,y ( x=y )' は、以前に取り組んだ実例 (V) にあるように、普遍量化子から成る式の簡略表現です。そこでこの簡略表現を普遍量化子を明示的に含んだ元の式に戻すと、次のようになることを確認しておきましょう。
- ⊢ ( ( E! ( ιx )( φx ) ) ≡ ( ( (∃c)( φc ) ) ∧ ( ( x, y )( ( φx ) ∧ ( φy ) ) ⊃ ( x=y ) ) ) ) (VIo)
実例 (VII) *8
- [ ( ιx )( φx ) ]. f ( ιx )( φx ) .=: (∃c): φx .≡x. x=c : fc Df (VIIa)
最後に、確定記述の scope indicator '[ ( ιx )( φx ) ]' を含んだ式を、やってみましょう。
この式には 'Df' とありますので、定義式であり、等号を含んでいるはずですからそれを探すと、二つ含んでいます。後に出てくる等号を見ると、'x=c : fc' とあって、この2点 dot は連言ですから、'x=c ∧ fc' となります。これを見ると、ここの等号はその横に dot がなく、その 'x' ないしは 'x' を含んだ左側と、'c ∧ fc' とで分けることができませんので、これは定義のための等号ではないと考えられます。ですから、(VIIa) 式の最初に出てくる等号を、定義のための等号だと踏んで、この最初の等号で式が前後に大きく分かれると判断し、まずその等号に着目します。
さて、式の最初の等号を見ると、その右に2点 dot があります。これは右カッコで、右に走査すると、同数の2点 dot に二箇所で出会います。初めに出会った dot は、量化子横の dot で、後で出会う dot は、先ほど述べたように、連言です。定義の等号と、量化子および連言を比べると、定義の等号の方が強いので、出会った量化子および連言である2点 dot のところではそれぞれカッコは閉じず、式の終端まで行ってカッコを閉じます。
- [ ( ιx )( φx ) ]. f ( ιx )( φx ) .= ( (∃c): φx .≡x. x=c : fc ) Df (VIIb)
今も述べたように、閉じたばかりのカッコ内の二箇所の二点 dot は量化子横のものと連言のもので、量化子横のものは右に開いたカッコです。
- [ ( ιx )( φx ) ]. f ( ιx )( φx ) .= ( (∃c)( φx .≡x. x=c ∧ fc ) Df (VIIc)
この右に開いたカッコは右に行って同数の元2点 dot である連言に出会いますが、量化子の方が連言よりも強いので、連言のところではカッコは閉じず、式の末端で閉じます。
- [ ( ιx )( φx ) ]. f ( ιx )( φx ) .= ( (∃c)( φx .≡x. x=c ∧ fc ) ) Df (VIId)
そして連言の両側にカッコを付け、
- [ ( ιx )( φx ) ]. f ( ιx )( φx ) .= ( (∃c)( φx .≡x. x=c ) ∧ ( fc ) ) Df (VIIe)
左側のカッコを左に行くと、同数である元2点 dot に量化子の右で出会いますので、量化子の方が連言よりも強いことから、そこでカッコを閉じます。
- [ ( ιx )( φx ) ]. f ( ιx )( φx ) .= ( (∃c)( ( φx .≡x. x=c ) ∧ ( fc ) ) Df (VIIf)
そして連言右の右に開いたカッコは式の終端で閉じます。
- [ ( ιx )( φx ) ]. f ( ιx )( φx ) .= ( (∃c)( ( φx .≡x. x=c ) ∧ ( fc ) ) ) Df (VIIg)
さて、最初の等号右辺に1点 dot が二箇所あります。最初の dot を見ると、左に開いたカッコであり、左に行って、元2点 dot のあった量化子の右横で閉じます。
- [ ( ιx )( φx ) ]. f ( ιx )( φx ) .= ( (∃c)( ( ( φx ) ≡x. x=c ) ∧ ( fc ) ) ) Df (VIIh)
もう一つの1点 dot は、その左の下付きの変項を無視すれば、右に開いたカッコであり、右に行って、元2点 dot のあった連言のところで閉じます。
- [ ( ιx )( φx ) ]. f ( ιx )( φx ) .= ( (∃c)( ( ( φx ) ≡x ( x=c ) ) ∧ ( fc ) ) ) Df (VIIi)
続いて、定義の等号の左辺を見ます。その等号の左横の dot は左カッコで、
- [ ( ιx )( φx ) ]. f ( ιx )( φx ) ) = ( (∃c)( ( ( φx ) ≡x ( x=c ) ) ∧ ( fc ) ) ) Df (VIIj)
左に走査すると、同数の1点 dot に出会います。これは scope indicator 横の dot で、実例 (III) で挙げたdot の強弱を表す不等式
連言 ＜ 量化子または記述句の scope indicator ＜ (否定を除く) 命題結合子または定義のための等号
の、
量化子または記述句の scope indicator ＜ (否定を除く) 命題結合子または定義のための等号
における右辺から左辺への関係が成り立っており、強い方から弱い方へ至っているので、scope indicator 横の dot ではカッコは閉じず、そのまま左へ進んで式の端でカッコを閉じます。
- ( [ ( ιx )( φx ) ]. f ( ιx )( φx ) ) = ( (∃c)( ( ( φx ) ≡x ( x=c ) ) ∧ ( fc ) ) ) Df (VIIk)
残った1点 dot を処理すると、これは scope indicator 横の dot で、実例 (I) の簡略表によると、その (ウ) に相当することから、カッコであり、scope indicator の右にあることから、右カッコです。
- ( [ ( ιx )( φx ) ] ( f ( ιx )( φx ) ) = ( (∃c)( ( ( φx ) ≡x ( x=c ) ) ∧ ( fc ) ) ) Df (VIIl)
そしてそこから右に進むと、同数の1点 dot に等号の左で出会います。私たちの不等式によるならば、
量化子または記述句の scope indicator ＜ (否定を除く) 命題結合子または定義のための等号
が成り立って、この左辺から右辺へと至っていますから、弱い方から強い方へ至っていることになり、したがって、scope indicator 横の右カッコは定義のための等号左側で閉じます。
- ( [ ( ιx )( φx ) ] ( f ( ιx )( φx ) ) ) = ( (∃c)( ( ( φx ) ≡x ( x=c ) ) ∧ ( fc ) ) ) Df (VIIm)
これで出来上がりました。
終りに、この式では普遍量化子の簡略表現が用いられていますので、念のために元の表現に戻しておきますと、
- ( [ ( ιx )( φx ) ] ( f ( ιx )( φx ) ) ) = ( (∃c)( (x)( ( φx ) ≡ ( x=c ) ) ∧ ( fc ) ) ) Df (VIIn)
となります。ちなみに、この定義式は、確定記述句を含んだ文を定義しているもので、大変有名な式と言えます。
練習問題
以上で解説が終わりましたので、理解を確かめるために、よろしければ練習問題をやってみて下さい。
次の1) と 2) では、dot 一つ違うだけで、式全体の構造がどのように違ってくるかに注意しながら dot をカッコなり連言なりに変えてみて下さい。3) と 4) も同様です。
1)*9
- (x): φx .⊃. ψx
2)*10
- (x). φx .⊃. ψx
3)*11
- [ ( ιx )( φx ) ]. f ( ιx )( φx ) .⊃. p
4)*12
- [ ( ιx )( φx ) ]: f ( ιx )( φx ) .⊃. p
5)*13
- ⊢ : x=y . y=z .⊃. x=z
6)*14
- ⊢ :･ p ⊃ q .≡: p .≡. p . q
7)*15
- ⊢ :･ p .∨. q . r :≡: p ∨ q . p ∨ r
最後の総仕上げとして、次の三つの式をやってみて下さい。いずれも有名な由緒ある式です。長くてかつ見慣れない記号が出てきますが、今までのやり方を応用すれば、できると思います。
8)
- [ p q ]:: p ≡ q .≡:･ [ f ]:･ f ( p f ( p [ u ].u ) ) .≡: [ r ]: f ( q r ) .≡. q ≡ p
この式は Lesniewski の Protothetic の公理です。Protothetic の公理には色々とあるようですが、この式はこれ一つだけで Protothetic の公理となる式です。1945年に Sobocinski が見つけました*16。式中の '[ ]' は普遍量化子を表しています。Lesniewskian は普遍量化子を '( )' ではなく '[ ]' で表します。'[ p q ]' は現在では '∀p∀q' と表します。なお言い添えておきますと、Lesniewskian の間では、'[ ]' に対し、微妙な解釈の違いを付与している可能性があります*17。Lesniewskian は '[ ]' を使うことで、普遍量化子に対し、現在とは異なった解釈を与えていると思われますが、Lesniewski の量化子をどのように解釈すべきかは、研究者の間で以前からしばしば問題とされてきた事柄です。ここではそのことに深入りすることはできません。今はさしあたって '[ ]' はただ普遍量化子のことだと考えて下さい。また、先の式中の関数 f は、二変数関数です。'f ( p f ( p [ u ].u ) )' の最初の f は、argument に p と f ( p [ u ].u ) を取っています。そしてこの 'f ( p [ u ].u )' における f は、argument として p と [ u ].u を取っています。さらに '[ u ].u' は、偽を表す式、偽の名前です。
9)
- ( A, a ):: ε{ Aa } .≡:･ ~( ( B ). ~(ε{ BA } ) ) :･ ( B, C ): ε{ BA } . ε{ CA } .⊃. ε{ BC } :･ ( B ): ε{ BA } .⊃. ε{ Ba }
この式は Lesniewski の Ontology の公理です。Ontology の公理にも色々あるようですが、これは Ontology に固有な公理として最初に発見されたもので、これ一つで Ontology の公理になっています*18。Lesniewski 本人が1920年に発見しました*19。この式の 'ε{ Aa }' は、今では 'Aεa' と書かれ、「A は a である」と読まれます。'ε{ Aa }' でひとまとまりと考えて下さい。
10)
- [ A B ]:::: Aεel( B ) .≡:::･ BεB :::･ [ f a ]::: [ C ]:: Cεf ( a ) .≡:･ [ D ]: Dεa .⊃. Dεel( C ) :･ [ D ]: Dεel( C ) .⊃. [ ∃E F ]. Eεa . Fεel( D ) . Fεel( E ) ::･ Bεel( B ) . Bεa ::･⊃. Aεel( f ( a ) )
この式は Lesniewski の Mereology の公理です。Mereology の公理にもやはり色々とあるようですが、この式一つで Mereology に固有な公理になっています。Mereology の単一の公理として (かつ Lesniewski の方法論上の要求を満たすものとして) 最初に発見されたのがこの式で、1948年に Sobocinski が見つけました*20。なお 'Aεel( B )' は、大まかながら、「A は B の要素である」と読まれます。'Aεel( B )' で、ひとまとまりと考えて下さい。また '[ ∃E F ]' は、今では '∃E∃F' と書かれます*21。
以上の練習問題については、可能ならば、後日、当日記で解答を掲載するかもしれません。あるいはしないかもしれませんが…。
終りに当たって。
以上の記述に対して、誤解、無理解、誤字、脱字等がありましたらお詫び申し上げます。間違っておりましたら、大変すみません。内容の最終確認は、記載しました文献に当たり、裏を取っていただきたく思います。
*1:Alfred North Whitehead and Bertrand Russell, Principia Mathematica to *56, Cambridge University Press, Cambridge Mathematical Library, 1997, p. 10. 邦訳、A・N・ホワイトヘッド、B・ラッセル、『プリンキピア・マテマティカ序論』、岡本賢吾、戸田山和久、加地大介訳、叢書思考の生成 1、哲学書房、1988年、43ページ。
*2:確定記述句の scope indicator [ ( ιx )( φx ) ] とは、確定記述句の作用域を示す装置です。確定記述句のいわゆる primary occurrence と secondary occurrence にかかわってくるものです。例えば 'It is false that the King of France exists who is bald' のような文の場合、少なくとも二通りの解釈が可能です。一つ目は、'The King of France exists and is not bald' であり、二つ目は、'There is no such person as the King of France who is bald' です。確定記述句が primary に現われているのは前者の解釈の場合であり、secondary に現われているのは後者の解釈の場合です。前者はフランス王がいて、その者は薄毛ではないということを言っており、後者は薄毛であろうがあるまいが、そもそもフランス王なる者はいないと言っています。このような二通りの読み方の違いを明示的に表す装置が、確定記述句の scope indicator です。なお確定記述の operator 'ι' は、Principia ではこの記号を反転させたようなものが使われていますが、そのような font が今はないので、iota 記号をそのまま代わりに使います。
*3:Principia, p. 10. 邦訳、45ページ。
*4:Principia, p. 14. 邦訳、55ページ。
*5:Principia, p. 20. 邦訳、74ページ。
*6:Principia, p. 22. 邦訳、80ページ。
*7:Principia, p. 31. 邦訳、107ページ。
*8:Principia, p. 70. 邦訳、222ページ。
*9:Principia, p. 17. 邦訳、64ページ。
*10:Principia, p. 17. 邦訳、64ページ。
*11:Principia, p. 70. 邦訳、223ページ。
*12:Principia, p. 70. 邦訳、223ページ。
*13:Principia, p. 22. 邦訳、82ページ。
*14:Principia, p. 14. 邦訳、56ページ。
*15:Principia, p. 14. 邦訳、57ページ。
*16:Boleslaw Sobocinski, ''On the Single Axioms of the Protothetic. I,'' in: Notre Dame Journal of Formal Logic, vol. 1, no. 1-2, 1960, p. 67.
*17:Czeslaw Lejewski, ''Reply to Comments,'' in Stephan Körner ed., Philosophy of Logic, Basil Blackwell, 1976, p. 52.
*18:Stanislaw Lesniewski, ''On the Foundations of Ontology,'' translated by M. P. O'Neil, in S. J. Surma, J. T. Srzednicki, D. I. Barnett ed., with an Annotated Bibliography by V. Frederick Rickey, S. Lesniewski Collected Works, Volume II, PWN-Polish Scientific Publishers and Kluwer Academic Publishers, Nijhoff International Philosophy Series, vol. 44, 1992, p. 609. This paper was first published in 1930.
*19:この公理の発見の経緯につきましては、当日記の2011年4月17日の項目 'Where Did Lesniewski Discover the Axiom of Ontology? And When He Discovered It, Was He Munching Bars of Chocolate?' をご覧下さい。
*20:Boleslaw Sobocinski, ''Studies in Lesniewski’s Mereology,'' in Jan T.J. Srzednicki, V.F. Rickey and J. Czelakowski ed., Lesniewski's Systems: Ontology and Mereology, Martinus Nijhoff / Ossolineum, Nijhoff International Philosophy Series, vol. 13, 1984, p. 222. これとは別に参照しやすい文献としては、例えば、Czeslaw Lejewski, ''A Note on a Problem Concerning the Axiomatic Foundations of Mereology,'' in: Notre Dame Journal of Formal Logic, vol. 4, no. 2, 1963, p. 135. この公理発見の経緯に関しては、簡略ながら、Sobocinski, ''Studies …,'' pp. 221-222 を参照。
*21:'[ ∃E F ]' を、'∃E∀F' とする向きもありますので、注意が必要です。See Jerzy Slupecki, ''S. Lesniewski’s Calculus of Names,'' in Jan T.J. Srzednicki, V.F. Rickey and J. Czelakowski ed., Lesniewski's Systems: Ontology and Mereology, Martinus Nijhoff / Ossolineum, Nijhoff International Philosophy Series, vol. 13, 1984, p. 63.
