考える坂本

坂本は生命維持と認識と価値判断と行動をします

超圧縮論理学 01.命題論理

密度を極限まで高めたい。適宜更新

命題論理

統語論

要素命題(以下素数)の集合 PV={p1,p2,…}が存在する。結合子¬∧∨が存在する。括弧()が存在する。論理式を以下で定義する(1)素数は論理式(2)α,βを論理式とすると(¬α)と(α∧β)と(α∨β)は論理式。以下括弧は適宜省略する。また論理式全体の集合をFとする。さて、その他の結合子を以下で定義する α→β:=¬(α∧β)、α↔β:=(α→β)∧(β→α)。また、以下でシグニチャを定義する ⊤:=p1∧p1, ⊥:=¬⊤。

論理式αの双対な論理式DC(α)を以下で定義する(1)DC(pi)=pi(2)DC(¬α)=¬DC(α),DC(α∧β)=DC(α)∨DC(β),DC(α∨β)=DC(α)∧DC(β)。論理式αの部分論理式Sf(α)[注:Sf(α)は集合]を以下で定義する(1)Sf(pi)={pi}(2)Sf(¬α)=Sf(α)∪{¬α},Sf(α∧β)=Sf(α)∪Sf(β)∪{α∧β}。論理式αの深さdeg(α)[注:deg(α)は自然数]を以下で定義する(1)deg(pi)=0(2)deg(¬α)=deg(α)+1,deg(α∧β)=max(deg(α),deg(β))+1,deg(α∨β)=max(deg(α),deg(β))+1。代入操作とは、σ:PV→Fに対して、以下のように構成される:σ(¬α)=¬σ(α),σ(α∨β)=σ(α)∨σ(β),σ(α∧β)=σ(α)∧σ(β)。

piと¬piをliteralと呼ぶ。DNFとはliteralを∧でつなげた複数の論理式を∨でつなげたもの。CNFとはliteralを∨でつなげた複数の論理式を∧でつなげたもの。

証明論(ゲンツェン)

0個の公理と6の規則からなる。規則は(IS)/α⊢α (MR)X'⊢α/X⊢α for X'⊇X (∧1)X⊢α,β/X⊢α∧β (∧2)X⊢α∧β/X⊢α,β (¬1)X⊢α,¬α/X⊢β (¬2)X,α⊢β X,¬α⊢β / X⊢β。ここで∨に関しては以下で再定義する α∨β:=¬(¬α∧¬β)。(※これが正当化されるが意味論から確認は必要)その他の結合子は統語論で規定したものと同じである。X⊢αという二項関係をシーケントといい、(X,α)と書くこともある。シーケントの並びS=(S0;S1;…Sn)で、Sn=(X,α)の場合、SをXからのαの演繹という。

幾つかの有用な追加規則が存在し、証明できる。(¬-elimination) X,¬α⊢α / X⊢α (reductio ad absurdum) X,¬α⊢β,¬β / X⊢α (→-elimination) X⊢α X⊢α→β / X,α⊢β (cut rule)X⊢α X,α⊢β / X⊢β (→introduction) X,α⊢β / X⊢α→β (detachment rule)X⊢α,α→β / X⊢β。

上記規則は一般化して、R: (X1,α1);(X2,α2);…(Xn,αn) / (X,α) と表現できる。規則Rについて「EがRで閉じている」を以下で定義する: E(X1,α1) ,E(X2,α2),..E(Xn,αn)が E(X,α)をimplyする。特にEが上述6規則すべてに閉じているならば、X⊢αは、E(X,α)をimplyするといえる。例えとして後述の「⊨」があげられる。

意味論

証明論(ヒルベルト)

知見

∉ ⊬ ⊭ ↓ ↑

logic

⊢ ∉ ⊬ ⊭ ↓ ↑ ⊥ ⊤