2002年 5月31日 作成 | 広義の述語論理 | >> 目次 (作成日順) |
2007年 8月 1日 補遺 |
今まで述べてきた単項述語論理や多項述語論理は、量化記号が個体に適用されていました。
本稿では、量化記号が 「述語 (性質)」 に適用されることを扱ってみましょう。
量化記号が個体に適用されている述語論理のことを第一階の述語論理といい、量化記号が述語に適用されている述語論理のことを広義の述語論理 (第二階の述語論理) といいます。
(1) ∃x P(x).
∃x P(x) は、性質 P をもつ x が少なくとも 1つ存在することを記述しています (したがって、すべての x について成立しないことを記述しています)。
束縛された性質を使った典型的な例が 「同一性」 を記述することでしょう。 x id y ≡ def ∀P [ P(x) = P(y) ].
[ 参考 ] 関係の量化を扱ったときに、「遺伝的 (継承)」 を以下のように記述しました。 Erbl (P, R) ≡ def ∀x ∀y { P(x) ∧ [ R (x, y) ⇒ P(y) ] }.
この論理式は、文章を使って記述すれば、「性質 P は関係 R に関して遺伝的である」 ということです。
さて、ここまで説明すれば、もう、「クラス の クラス (性質の性質、あるいは、関数の関数)」--タイプ 理論を思い出してください--を理解することができるでしょう。 f (x) = { a, b, c }.
さて、F (f) を考えてみましょう。F (f) は { f } のことですね。
f (x) = { a, b, c }.
つまり、F は f の高階にある、ということです。
[ 注意 ]
さて、ここまで説明すれば、空集合が 「一者集合」 であることも、以下のように考えれば理解できるでしょう。 ちなみに、第一階の述語論理 [ たとえば、P (x) ] に対して、一階の性質全体に言及していれば、1つ上の階と同じになることを覚えておいてください。一階の性質全体に言及する、ということは ∀P ∀x P(x) のことですから、第二階の述語論理と同じことです。束縛された述語変数をふくむ論理式は高階の論理式とみなすことができます。 さて、以下の論理式を読んで、きょうの説明を終わりにしましょう。
∀P ∀x { p1(x) ⊃ P(x) ⊃ P(x1)}. この式を文章を使って記述すれば、「佐藤正美には優秀な システム・エンジニア のすべての性質が備わっている」 ということです。ただし、この判断は 「偽」 かもしれない(笑)。 □ |
[ 補遺 ] (2007年 8月 1日)
ロジック の専門書によれば(参考)、20世紀の初め、形式論理の中核は (ホワイトヘッド・ラッセル が示した) タイプ 理論だったそうです。「第一階の述語論理」は、ヒルベルト が タイプ 理論を制限して、1917年-1918年の講義のなかで導入したそうです。その考えかたは、のちに、アッケルマン との共作 「記号論理学の基礎」 (1954年) として出版されました--小生は、この書物を (翻訳で) 読みました。当時は、まだ、「述語論理」 という用語は使われておらず、「述語」 を 「関数」 というふうに言っていました。「第一階の述語論理」 は 「制限された関数計算」 と言われていました。「1階」 という ことば は、19世紀末に、すでに、パース が使っていましたが、それを形式論理の体系のなかで意識した人物は ヒルベルト だそうです。そして、その公理系 (ヒルベルト・アッケルマン が示した公理系) が 「完全」 であることを証明したのが 「ゲーデル の完全性定理」 です (1930年)。すなわち、「恒真命題は、すべて、証明可能である」 が証明されました。ただし、ゲーデル の証明法は対偶を使ったのであって、「証明可能でない命題には、反例の モデル が存在する」 ということでした。この証明法を、もっと一般的・具体的にした人物が ヘンキン です (1949年)。現代では、「タブロー 法」 が導入され、「証明と モデル」 が連係されて、「第一階の論理」 が見通し良くなりました。 いっぽうで、実数論を 2階自然数論のなかで形式化する やりかた も進められてきました。2階自然数論は、1階の ペアノ 算術に対して、自然数の 「関係 (述語、集合)」 の 2階量化を導入した体系です。デデキント が導入した 「切断」 を使う やりかた です。すなわち、有理数を自然数と 「1-対-1」 に対応させて、「切断」 を使って、実数を有理数の集合として定義する やりかた です。モデル どうしが 「同型」 になることを 「範疇的」 と云いますが、2階自然数論は、「範疇的」 です。ただし、2階自然数論の形式的体系の 1つとして、2階算術体系 Z2 がありますが、Z2 は、「範疇的」 ではないそうです。 |
<< もどる | HOME | すすむ >> | |
ベーシックス |