項表現を定義する
一階述語で、定数とか関数の形とかの表現を定義してみる。
数理論理学の教科書などでは、普通はこういう定義だと思う。
定数記号をa,b,c,…とし、変数記号はx,y,z,…、関数記号をf,g,…とする。
このとき項は次のように定義される。
1) 定数記号は項である。
2) 変数記号は項である。
3) fを関数記号とし、t1,t2,…を項とするとき、f(t1,t2,…)は項である。
4) 1から3までで定義されるもののみが、項である。
まず、これを一階述語で書けないのは、いくつか原因があるので、ひとつずつ考えていく。
"a,b,c…"といった"…"表現は、書けない。しかし、ある論理式を書くために必要な定数記号(変数や関数も同じ)については書けるので、それを公理としておけばいいだろう。
例) +Const(a)、+Var(x)、+Func(f)などという具合。1にしたがって、特定の関数についての公理を書くとすると、"t1,t2,…"という書き方は不要になるだろう。
つまり、関数fが2引数の場合は、「t1,t2を項としたとき、f(t1,t2)は項である」と書けば良い。このように、項一般に対する定義は書けないが、必要な項(有限個)について個々の定義を書くことならできる。
そこで、項を表現と呼んで、述語 (Expr e)がeは「表現である」を意味するとする。これでS式的論理式に書き直すと
(1 () (+ Expr x)(- Const x))
(2 () (+ Expr x) (- Var x))
(3 (e1 e2) (+ Expr (f e1 e2)))(- Expr e1)(- Expr e2))
となるだろう。
(+ Symbol x) ≡ (+ Var x)∨(+ Const x)だが、それはここでは扱わない。
4の条件は、この定義から生成される表現のみという意味であり、もしもそれで反証を使いたいとすると、こういうnconjから□ができてほしい。
(a () (+ Expr c))
(b () (+ Expr (f a))
(c () (+ Expr ((a)(b))))
aは、1、2の定義に対しては符号が交わらないので、無理。また、-Exprが存在しないのでresolve対象もない。
3の定義に対しては交わるが、□のほうにはいかないので反証不可能。
Resolutionを使うとき、-Φの世界はうまくいくが、+Φの世界とはかすりもしない。あるいは証明の無限ループに陥るか。ということがよくある。
+Φと-Φを同時に証明器にかければうまくいくのかというとΣの書き方にもよるし、どうすればいいのかよくわからない。
cは、一階述語の論理式にならないので、記述しようとしている論理式として無功になり、うまくいく。記述される言語と記述していいる言語が同じになると、こういう空振りするような事象がよくある。これはなんなんだろう。
具体的な記号について、Exprではないということを明記しようとすると、こういう公理を追加することになるのだろう。でも、ルール4は、こういうことをいちいち書かずにすませようとしている。そういうメタな書き方は、証明論の教科書にはよくでてきていて、それをどう解釈するのかなどは、読者に委ねられている。メタな概念を説明なく使ってもよいとするのは、なにか欠陥なのではないだろうか。
(() (- Expr c))
((x) (- Expr x) (+ Symbol x))
((x) (- Expr (f x)))
((x y) (- Expr (g x y)))