二分木で一階述語論理を表現する
二分木で一階述語論理を表現する。
基本構造の葉の部分に、名前が入る。
基本構造の節の部分に、項と式がわりあたる。
-
-
-
- ----
-
-
＜基本構造＞
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)のような形式は何かというと、関数である。
関数ではあるが、名前が省略されている。
そこで一時的につけた名前が、￥。
