二分木で一階述語論理を表現する

二分木で一階述語論理を表現する。

基本構造の葉の部分に、名前が入る。
基本構造の節の部分に、項と式がわりあたる。

• • • • ----

＜基本構造＞

Aは葉、Bは葉、ならば、(A,B)は節。
Aは節、Bは葉、ならば、(A,B)は節。
Aは葉、Bは節、ならば、(A,B)は節。
Aは節、Bは節、ならば、(A,B)は節。

• • • • ----

＜基本構文＞

Aは名前、ならば、
Aは述語、または、Aは関数、または、Aは変数、または、
Aは接続、または、Aは量化、または、Aは類化、または、Aは記号、のいずれかになる。

＄は記号。
％は記号。

＄は項リスト。
Aは項、Bは項リスト、AとBに含まれる束縛変数は重複しない、ならば、(A,B)は項リスト。
％は式リスト。
Aは式、Bは式リスト、AとBに含まれる束縛変数は重複しない、ならば、(A,B)は式リスト。

［リスト生成時の条件で、束縛変数は重複しないことを求めたのは、複雑さ回避のため］

Aは変数、ならば、Aは項、かつ、以後、Aは自由変数。
Aは述語、Bは項リスト、ならば、(A,B)は式。
Aは関数、Bは項リスト、ならば、(A,B)は項。
Aは接続、Bは式リスト、ならば、(A,B)は式。
Aは量化、Bは式、CはBに含まれる自由変数、ならば、(A,(C,B))は式、以後、Cは束縛変数。
Aは類化、Bは式、CはBに含まれる自由変数、ならば、(A,(C,B))は項、以後、Cは束縛変数。

• • • • ----

＜自由変数と束縛変数の厳密な遺伝の仕方＞

［変数が自由か束縛かは、どの式またはどの項の中にあるかに依存する］

Aは変数、ならば、Aは項Aに含まれる自由変数。

Aは述語、Bは項リスト、CはBに含まれる自由変数、DはBに含まれる束縛変数、ならば、
Cは式(A,B)に含まれる自由変数、Dは式(A,B)に含まれる束縛変数。

Aは関数、Bは項リスト、CはBに含まれる自由変数、DはBに含まれる束縛変数、ならば、
Cは項(A,B)に含まれる自由変数、Dは項(A,B)に含まれる束縛変数。

Aは接続、Bは式リスト、CはBに含まれる自由変数、DはBに含まれる束縛変数、ならば、
Cは式(A,B)に含まれる自由変数、Dは式(A,B)に含まれる束縛変数。

Aは量化、Bは式、CはBに含まれる自由変数、DはBに含まれる束縛変数、ならば、
Cは式(A,(C,B))に含まれる束縛変数、Dは式(A,(C,B))に含まれる束縛変数。

Aは類化、Bは式、CはBに含まれる自由変数、DはBに含まれる束縛変数、ならば、
Cは項(A,(C,B))に含まれる束縛変数、Dは項(A,(C,B))に含まれる束縛変数。

• • • • ----

＜特別な名前と属性を与えていく＞

¬は接続。
∨は接続。
∧は接続。
⇒は接続。
⇔は接続。

Aは式、ならば、(¬,(A,％))は式。
Aは式、Bは式、(A,(B,％))は式リスト、ならば、(∨,(A,(B,％)))は式。
Aは式、Bは式、(A,(B,％))は式リスト、ならば、(∧,(A,(B,％)))は式。
Aは式、Bは式、(A,(B,％))は式リスト、ならば、(⇒,(A,(B,％)))は式。
Aは式、Bは式、(A,(B,％))は式リスト、ならば、(⇔,(A,(B,％)))は式。

∃は量化。
∀は量化。

Aは式、BはAに含まれる自由変数、ならば、(∃,(B,A))は式。[以後、Bは束縛変数]
Aは式、BはAに含まれる自由変数、ならば、(∀,(B,A))は式。[以後、Bは束縛変数]

＠は類化。

Aは式、BはAに含まれる自由変数、ならば、(＠,(B,A))は項。[以後、Bは束縛変数]

∈は述語。
Aは項、Bは項、(A,(B,％))は項リスト、ならば、(∈,(A,(B,％)))は式。

⊂は述語。
Aは項、Bは項、(A,(B,％))は項リスト、ならば、(⊂,(A,(B,％)))は式。

＝は述語。
Aは項、Bは項、(A,(B,％))は項リスト、ならば、(＝,(A,(B,％)))は式。

￥は関数。
Aは項リスト、ならば、(￥,A)は項。

• • • • ----

＜通俗表示＞

：の左側は正式表示、：の右側は通俗表示。

(¬,(A,％))　　　：　(¬A)
(∨,(A,(B,％)))　：　(A∨B)
(∧,(A,(B,％)))　：　(A∧B)
(⇒,(A,(B,％)))　：　(A⇒B)
(⇔,(A,(B,％)))　：　(A⇔B)

(∃,(B,A))　　　 ：　∃B(A)
(∀,(B,A))　　　 ：　∀B(A)

(＠,(B,A))　　　 ：　{B|A}

(∈,(A,(B,％)))　：　(A∈B)
(⊂,(A,(B,％)))　：　(A⊂B)
(＝,(A,(B,％)))　：　(A＝B)
(￥,A)　　　　　 ：　A

Pは述語、A、Bは項、のとき、
(P,(A,＄))　　　 ：　P[A]
(P,(A,(B,＄)))　 ：　P[A,B]
以下、同様。

Fは関数、A、Bは項、のとき、
(F,(A,＄))　　　 ：　F(A)
(F,(A,(B,＄)))　 ：　F(A,B)
以下、同様。

￥について：
(a,b)や(a,b,c)のような形式は何かというと、関数である。
関数ではあるが、名前が省略されている。
そこで一時的につけた名前が、￥。

興味あることの覚書

興味あることの覚書

minix:小さくて、カーネルの学習を始めるのに、ちょうど良いらしい。
netbsd:移植性がめちゃ高くて、コードがきれいなのでは？、と想像。
(freebsdはいまのところあんまり興味なし)
debian:パッケージ管理システムがとてもよさそう。
centos:安定感ありそう。でも古めかしい。
lfs:一度手を出した。やっとのことで起動させただけで終わった・・・。

cygwin:普段よく使ってるので、どういう仕組なのか興味ある。
gcc:C/C++のお勉強に。
gdb:使い方。
clang:。gccのライバル。gccにとって代わるかも。
llvm:clangの縁の下の力持ち。

x11:デスクトップ環境の最下層システム。どういう仕組になってるのか。
gnome:有名なデスクトップ環境。どういう仕組になってるのか。
kde:有名なデスクトップ環境。どういう仕組になってるのか。
gtk:gnomeの基礎。
qt:kdeの基礎。

sagemath:数学処理システム
maxima:同じく
R:統計処理システム

prolog:論理型
kl1:論理型
smalltalk:オブジェクトにメッセージを送る方式らしい。squeakという実装あり。
lisp:リスト表現のプログラム。
scheme:同上
haskell:関数型
sml:関数型
ocaml:関数型
erlang:関数型

pascal:言語仕様がなんとなく気になる。よく整理され、よく考えられてるイメージがある。
modula2:同上
eiffel:同上

postgresql:データーベース管理システム
mysql:同上

python:やっとくとよいらしい。sagemathのコマンドラインはpythonなのでとても興味あり。
ruby:pythonのライバル
perl:レガシー

集合論（その３）

　Set という述語を与える。Set［A］と書いて、「Aは集合」と読ませる。１項の原始的述語。このとき、Aは個体。

　Set に関して、公理を与える。

[10] ∀A（Set［A］⇒∀B（（B⊂A）⇒Set［B］））
[11] ∀A（Set［A］⇒Set［Pow［A］］）
[12] ∀A（Set［A］⇒Set［∪A］）
[13] ∀A∀B（（Set［A］∧Set［B］）⇒Set［A×B］）

　これでは、「集合が存在すれば」という仮定の話で終ってしまうので、始まりの集合を与えねばならない。

[14] ∃x（∀y（¬（y∈x）））

　[14]から新しい個体が生み出される。φと書いて、「空集合」と呼ぶことにする。

[15] Set［φ］

[16] ∃x（（φ∈x）∧∀y（（y∈x）⇒∀z（（z∈y）⇒（z∈x））））

　[16]から新しい個体が生み出される。Ｎと書いて、「自然数全体」と呼ぶことにする。（何か足りない気がする。カントルの超限順序数全体になりそうな気がするが、強行する）

[17] Set［Ｎ］

　後、数学的帰納法とか、選択公理などを公理に追加して、終わりたいが、なんだか、能力の限界に達したような気がするので、これでおしまい。

　では。またの機会に。

集合論（その２）

　A、Bを個体とする。
・A⊂B は、∀x（（x∈A）⇒（x∈B））の短縮形である。もちろん、これは派生的命題。⊂は派生的述語と言える。あくまでも、便宜上のもの。意味は、「AはBの部分」。
・A＝B は、（A⊂B）∧（B⊂A）の短縮形。派生的命題。＝は派生的述語。同様に便宜上ののもの。意味は、「AとBは等しい」。
・｛A, B｝は、｛x｜（x＝A）∨（x＝B）｝の短縮形。２パラメタの派生的個体。意味は、「AとBを含む個体」。派生的個体の短縮形は、記号≡の左辺で表すことにする。この場合は、｛A, B｝≡｛x｜（x＝A）∨（x＝B）｝。
・A∪B≡｛x｜（x∈A）∨（x∈B）｝。２パラメタの派生的個体。意味は、「AとBの合併」。
・A∩B≡｛x｜（x∈A）∧（x∈B）｝。２パラメタの派生的個体。意味は、「AとBの共通」。
もっと一般的な合併と共通を与える。
・∪A≡｛x｜∃y（（x∈y）∧（y∈A））｝。
・∩A≡｛x｜∀y（（y∈A）⇒（x∈y））｝。
両方とも、１パラメタの派生的個体。
∀A∀B（∪｛A, B｝＝A∪B）、
∀A∀B（∩｛A, B｝＝A∩B）、
これらは、定理。

・Pow（A）≡｛x｜x⊂A｝。１パラメタの派生的個体。意味は、「Aの部分の集まり」。
・（A、B）≡｛A、｛A、B｝｝。２パラメタの派生的個体。意味は、「AとBの対という個体」。
このとき、∀A∀B∀C∀D（（（A、B）＝（C、D））⇒（（A＝C）∧（B＝D）））は、定理。
・A×B≡｛x｜∃y∃z（（x＝（y、z））∧（y∈A）∧（z∈B））｝。２パラメタの派生的個体。意味は、「AとBの直積」、または「AとBの元の対の最大の集まり」。
・（f（x）＝y）は、（（x、y）∈f）の短縮形。３項の派生的述語の命題。「・（・）＝・」という形自体が、派生的述語を表していることに注意。また、その命題は派生的命題ではなく、れっきとした原始的命題の部類に入る。意味は、「yはxにおけるfの値」。
・（f：A〜B）は（∀x（（x∈A）⇒∃y（（y∈B）∧（f（x）＝y））））の短縮形。３項の派生的述語の命題。これも、「・：・〜・」という形自体が、派生的述語を表していることに注意。この命題は派生的命題の部類。意味は、「fはAからBへの関係？」。
・Single_Val［A、B、f］は、∀x∀y∀z∀w（（（x∈A）∧（y∈A）∧（z∈B）∧（w∈B）∧（f（x）＝z）∧（f（y）＝w）∧（x＝y））⇒（z＝w））の短縮形とおく。（３項の派生的述語。意味は、「fは１価」。）
・（f：A→B）は（（f：A〜B）∧Single_Val［A、B、f］）の短縮形。３項の派生的述語の命題。これも、「・：・→・」という形自体が、派生的述語を表していることに注意。この命題は派生的命題の部類。意味は、「fはAからBへの写像」。写像というとき、１価を前提にすることにした。多価のときは、原始的写像とでも呼ぼう。
・Map0（A、B）≡｛f｜f：A〜B｝。２パラメタの派生的個体。意味は、「AからBへの原始的写像の集まり」。
・Map（A、B）≡｛f｜f：A→B｝。２パラメタの派生的個体。意味は、「AからBへの写像の集まり」。
∀A∀B（Map（A、B）⊂Map0（A、B）⊂Pow（A×B））、
∀A∀B（∪｛x｜∃y（x＝Map0（y、B））∧（y⊂A）｝＝Pow（A×B））、
は定理（かな？）。

　次は、２つ目の原始的述語が登場。それは、「Aは集合である」を意味する述語。次回へ。

集合論

　集合論では、原始的述語がまず１つ現れる。それは記号∈で表される。これは２項述語になる。a∈A と書いて、「a は A の元である」と読む。もちろん、a と A は何らかの個体である。他にもいろいろな読み方があるが、本質は、２項の述語であるということ。

　Pを述語、aを個体とする。P［... , a, ...］を a∈｛x｜P［... , x, ...］｝のように変形してみる。「...」には適当な個体が並んでいるとする。記号∈の右側に現れるのは、クラスと呼ばれる個体である。P［... , a, ...］が正しい命題なら、個体aはそれを満たしているので、｛x｜P［... , x, ...］｝の元である。つまり、a∈｛x｜P［... , x, ...］｝は、このように解釈できる。｛x｜で外に括り出されたxは、束縛変数である。命題を束縛して新しい命題を生み出すのとは異なり、命題を束縛して新しい個体を生み出すものである。この個体を、派生的個体と呼ぶことにする。もちろん、xの位置にある項は使用不可。「...」の中に個体があれば、クラスは、パラメタ化された個体になる。

　個体の生成規則を立てる。(3) Pを述語とする。｛x｜P［... , x, ...］｝は個体として扱うと取り決める。xは派生的個体を生成する束縛変数、派生的命題を生成する束縛変数とは区別する。

　述語論理の公理系に追加する。そして、それを集合の公理系とする。
！　[8] Pは任意の述語、aは任意の個体とする。
！　　　（P［... , a, ...］）⇒（a∈｛x｜P［... , x, ...］｝）、
！　　　（a∈｛x｜P［... , x, ...］｝）⇒（P［... , a, ...］）、
！　　　（P［... , a, ...］）⇒（∃x（P［... , x, ...］））、
　[8] Pは任意の述語とする。
　　　∀y（（P［... , y, ...］）⇒（y∈｛x｜P［... , x, ...］｝））、
　　　∀y（（y∈｛x｜P［... , x, ...］｝）⇒（P［... , y, ...］））、
　　　∀y（（P［... , y, ...］）⇒（∃x（P［... , x, ...］）））、
の形の命題はすべて、正しい命題と取り決める。
　[9] ∃x（P［... , x, ...］）は正しい命題とする。どの個体とも一致しない文字列aを作り出しておき、命題P［... , a, ...］を正しい命題とするような個体として取り扱う。この個体aを原始的個体と呼ぶことにする。
（ここら辺はオリジナルなので、かなりあやうい。[8]は、！の付いてる方と、付いてない方どちらを採用してもいい。統一感が決めてになると思うが…）

　さて、これでようやく公理論的集合論を始められる。それは、公理を追加する形で行われる。公理とは、[1][2][3][5][6][8]などのように、最初から正しいと取り決めた命題をさす。公理以外の正しい命題を、定理と呼ぶことにする。

　ここでちょっと、用語の整理。出て来た用語は、
　　原始的命題、派生的命題、命題、正しい命題、正しくない命題、
　　原始的述語、派生的述語、述語、
　　原始的個体、派生的個体、個体、
　　原始的記号、派生的記号、
　　公理、定理、
である。

　この時点で具体的なものが出てるのは次の通り。原始的述語は、∈のみ。派生的述語は、便宜上のもの、なので、存在せず。派生的個体は、クラスそのもの。原始的個体はまだ、なにも決めてない。これから、∃x（...）の形の公理を追加していくことで、増えていく。さて、原始的個体と原始的述語から構成される命題は、原始的命題と呼んでも違和感はないが、派生的個体が混じる個体と原始的述語から構成される命題は、原始的命題と呼んでいいだろうか。とりあえず、そうしていいとしておく。原始的記号は、∨、¬、∀。派生的記号は、Λ、⇒、∃。

　おまけ。ラッセルのパラドックスの話。

　｛x｜¬（x∈x）｝∈｛y｜¬（y∈y）｝は命題の形をなしている。だから命題である。だが、まだ正しい命題かどうかは決めていない。２つの個体が同じ、という性質はまだ定義してないが、個体｛x｜¬（x∈x）｝と個体｛y｜¬（y∈y）｝は同じと考えると、X∈X という形をしているので、Xは｛y｜¬（y∈y）｝に含まれない。つまり、
　　（｛x｜¬（x∈x）｝∈｛y｜¬（y∈y）｝）⇒（¬（｛z｜¬（z∈z）｝∈｛w｜¬（w∈w）｝））
は、正しい、と言えそうだ。同様に考えていく。¬（X∈X）が成立しているならば、Xは｛y｜¬（y∈y）｝に含まれる。つまり、
　　¬（｛x｜¬（x∈x）｝∈｛y｜¬（y∈y）｝）⇒（｛z｜¬（z∈z）｝∈｛w｜¬（w∈w）｝）
も、正しい、と言えそうだ。AはX∈Xの略としよう。これは、A⇒（¬A）⇒A⇒（¬A）⇒... と堂々巡りする命題となる。もし、最初のAが正しいと、¬Aも正しいことになってしまい、システムは矛盾している、ということになる。これが、ラッセルのパラドックスである。

　A、つまり、｛x｜¬（x∈x）｝∈｛y｜¬（y∈y）｝は、正しい命題にしてはいけないのだ。または、｛x｜¬（x∈x）｝という個体が公理系の中に現れなければいいとも言える。

述語論理

　「石は硬い」という原始的命題は、「石」と「〜は硬い」の２つの部分に分けることができる。「石」は、個体と呼ばれるグループにまとめられ、「〜は硬い」は、述語と呼ばれるグループにまとめられる。「太郎と次郎は兄弟だ」という原始的命題では、「太郎」、「次郎」は個体、「〜と〜は兄弟だ」は述語であり、特に、２項述語と呼ばれる。「〜は硬い」は１項述語。述語は、複数の項を持つ。

　記法として、PをN項述語、a_1、…、a_Nを、N個の個体とし、P［a_1, ... , a_N］と書いて、原始的命題を表しているとする。P［... , a, ...］と、項の数をあいまいにして表すこともある(もちろん、aは個体、「...」の部分にも個体が並んでいるとする)。

　P、Qを１項述語、a、bを個体とする。たとえば、（P［a］∨Q［b］）⇒P［b］は、派生的命題であるが、全体でみて、２項述語と見ることができる。よって、P［a］と書いても、それは原始的命題とは限らないことにする。原始的命題の述語は原始的述語、派生的命題の述語は派生的述語と呼ぶことにする。このとき、派生的述語は本当の述語ではなく、仮のもの、一時的なものであることに注意。原始的述語こそ、本当の述語。

　命題の生成規則を追加する。(2) P［... , a, ...］が命題のとき、∀x（P［... , x, ...］）はまた、命題であると取り決める。述語Pの個体aがおかれていた項は束縛されて、使用できなくなっているとみなす。項が１つ減った述語が新たに作り出されたとみなす。「...」の部分には個体があって、変形前後で変わっていないする。∃x（P［... , x, ...］）は ¬（∀x（¬P［... , x, ...］））の短縮形とする。記号∀で、外に括り出されたxは、束縛変数と呼ぶ。その位置にある項は使用不可能になったとみなす。ちなみに、記号∀は原始的記号、∃は派生的記号と呼ぶことにする。∀を適用してできた命題は派生的命題とみなす。

　意味的には、次の通り。命題∀x（P［... , x, ...］）が正しいとか正しくないなど、何らかの性質を持つとき、すべての個体aについて、命題P［... , a, ...］は正しいとか正しくないなど、同じ性質を持つ。命題∃x（P［... , x, ...］）が正しいとか正しくないなど、何らかの性質を持つとき、ある個体aで、命題P［... , a, ...］が正しいとか正しくないなど、同じ性質を持つ。

　正しい命題の生成規則も追加する。命題論理の公理系に次のを追加して、述語論理の公理系とする。
　[5] aは適当な個体とする。Pは適当な述語とする。
　　　∀x（P［... , x, ...］）⇒P［... , a, ...］
の形の命題はすべて、正しい命題であると取り決める。もちろん、xとaは同じ位置にあって、「...」の部分には適当な個体が並んでて、記号⇒の前後で変わっていないとする。
　[6] Qは適当な述語で、束縛変数xによる束縛とは関係がないとする。
　　　（∀x（Q［...］⇒P［... , x, ...］））⇒（Q［...］⇒∀x（P［... , x, ...］））
の形の命題はすべて、正しい命題であると取り決める。
　[7] どんな個体aに対しても、P［a］が正しい命題であるとする。∀x（P［x］）は正しい命題として扱う。
（参考「記号論理学」清水義夫　東京大学出版会）

　次、ようやく、集合論。

命題論理

　命題とは、事実を述べようとする文のこと。たとえば、「石は硬い」とか、「鉄は硬い」、「空気は硬い」など。そして、最初の２つは正しい命題、最後のは間違いで正しくない命題、とかのように評価される。これらを原始的命題と呼ぶことにする。

　原始的命題から新しい命題を生成する手段を与える。(1) A、Bを命題とする。このとき、A∨B、¬A、を命題であると取り決める。続いて、A∧B、A⇒B、をそれぞれ、¬（（¬A）∨（¬B））、（¬A）∨B、の置き換え（または、短縮形）とする。取り決め通り、明らかに、A∧B、A⇒B、は命題である。(1)で生成された命題を派生的命題と呼ぶことにする。派生的命題も原始的命題もどちらも、命題であることに変わりはないことに注意。派生的命題からさらに派生的命題を作ってもよい。記号∨、¬、は原始的記号、∧、⇒、は派生的記号と呼ぶことにする。

　意味的には、A∨Bは「AまたはB」、¬Aは「Aの否定」、A∧Bは「AかつB」、A⇒Bは「AならばB」、のように解釈される。

　文字列（文字の並びのこと）と命題はきちんと区別される。命題は文字列の一種だが、命題とはならない文字列が存在することに注意。何かしらの文字列が存在して、それが命題かそうでないかの区別は簡単につく。まず、(i)記号¬が付いているかどうかチェックし、付いてたら、¬を取り除いたものが命題かどうかチェックする。(ii)記号¬が付いてなかったら、記号∨が含まれているかどうかチェックし、含まれていたら、∨を挟む両方の文字列が命題かどうかチェックする。(i)と(ii)を繰り返していき、最後に残った文字列が、原始的命題であるかチェックする。すべてのチェックが通れば、問題の文字列は命題だったと判断できる。

　命題論理の公理系について取り決める。公理系とは、正しい命題の集まりのこと。

　A、B、Cを適当な命題とする。このとき、
　[1] A⇒（B⇒A）、
　[2] （A⇒（B⇒C））⇒（（A⇒B）⇒（A⇒C））、
　[3] （（¬B）⇒（¬A））⇒（（（¬B）⇒A）⇒B）、
という形をした命題はすべて、正しい命題であると取り決める。さらに、
　[4] Aを正しい命題とし、また、A⇒B という形をした命題も正しい命題とする。このとき、Bは正しい命題として取り扱うと取り決める。
（参考「記号論理学」清水義夫　東京大学出版会）

　こうして、正しい命題から成る公理系が構成される。たとえば、適当な命題Aに対して、A⇒A という形の命題はすべて正しい命題となることが示される。また、正しい命題はすべて恒真命題になるし、恒真命題もすべて正しい命題になる。つまり、正しい命題と恒真命題はきれいに一致する。恒真命題とは、中に含まれる原始的命題の真偽によらず、必ず真になる命題のこと。

　Aが正しい命題のとき、¬Aは正しくない命題と呼ぶことにする。同時に、Aが正しくない命題であることを確認するには、¬Aが正しい命題として確認できることとしなければいけないかも。これは示せるものか、決めなければいけないものか、ちょっと判断つかない。申し訳ない。また、たぶん、Aが正しくない命題のとき、¬Aは正しい命題となるのは示せそう。

　次は、述語論理。その後は、集合論を展開したい。