"Proof Theory for First Order Lukasiewicz Logic" (Mathias Baaz and George Metcalfe)
今年3月にもらった論文、やっと読み終わりました。Metcalfe氏ののweb siteはこちら、論文ファイルはこちら。
ファジイ論理の代表例といえる Lukasiewicz 無限値述語論理 ∀L は、通常は真理値から定義されるせいか、証明論的には非常に複雑で、帰納的に公理化不可能であることが知られています。だから証明論的性質がよくわかっていない。この論文はそこの解明が目的です。
近似版Herbrandの定理とSkolemization
論文の前半はHerbrandの定理とSkolem化について。まず、 ∀L ではHerbrandの定理は成立しないそうです（すぐ反例が作れます）。しかし、Herbrandの定理の近似版：
任意の c<1 と論理式 ∃xP(x) について、あるHerbrand 項 t0,・・・,tn が存在し、論理式 P(t1) ∨・・・∨P(tn)の真理値は c より大きくなる。
が成立することを証明しています（証明はcompactnessを使っている）。驚きました。それだけではなく、Skolemization も実は可能なのです！！証明は、new function symbol を使ってSkolem form （存在冠頭式でprenex form）に変換した後、上記の近似版Herbrandの定理を適用して両者の真理値が一致することを示します。すごい。
Hypersequent 計算 G∀L
さて、論文の後半は ∀L の形式化について。 ∀L を証明論的に形式化する場合、∀L より少しだけ証明力が弱いが、その代わりに帰納的に公理化可能な部分的体系をまず定義して、それに縮約規則の断片にあたるような無限的なルールを付け加えるというのが、通常のやり方です。Hay による公理化(1963)が代表例でしょう。
帰納的に公理化可能な ∀L の部分的体系の現代における代表例がHajekの L∀ で、Hilbert styleで公理化されています。 ところで、L∀のGentzen styleでの公理化は無理なんだそうです。でも証明論をやるには、sequent calculusっぽいスタイルの方がやりやすい気がします。という訳で、著者らは Hypersequent を使った形式化を提案しています。Hypersequent とは Γ⇒Γ'|Δ⇒Δ'・・・|θ⇒θ' の形をしているmultisetです。簡単な場合 A,B⇒C,D | E,F⇒G,H の意味は (A*B→C*D)∨(E*F→G*H) を意味するものです*1。Hypersequent は、ファジイ論理で重要な役割を果たす Preliniarity *2を含む部分構造論理を形式化する際によく使われるようです。これによると、hypersequentがよく使われる理由は、
since the multiple components of the hypersequent allow several alternative hypotheses to be processed in parallel. (p.8_10)
だそうです。prelinearityの証明を考えてみるとわかるように、split rule と (右∨) の導入ルールが「平行プロセス」の表現のために重要です。
さて、Hypersequent を使って、彼らは Hypersequent calculus G∀L を提案しています。このとき
L∀=G∀L+cut rule
という等式が成立します。また Hay の導入した真理値を任意の精度で近似するような無限的ルール
任意の自然数 n について、A+(A*・・・*A) （ただしAがn個）がG∀Lで証明可能なとき、G∀Lで A を証明してよい
をG∀L に導入すると、この拡張された体系は∀L と同値になります。
