節（Clause） 全ての要素がアトムであるシークェントのことを節という。空シークェントを空節という。 冠頭標準形：スコーレム標準形：節集合 充足不能性で等価である。 スコーレム標準形を節の集合で表したものを節形式という。 名前変代入 名前変えにより…

最汎単一化子 代入の合成 θ=[f(x)/x,g(z,b)/y] σ=[f(z)/x,a/z] h(x,y,z)θσ=h(f(x),g(z,b),z)σ=h(f(f(z)),g(a,b),a) こんな代入になるような代入の合成を定義する。 代入θ=[s1/u1, ... , sm/um],σ=[t1/v1, ... ,tn/vn]に対してその合成は θσ=[s1σ/u1, ... ,sm…

スコーレム標準形 スコーレム標準形とは、存在限量子を含まず、全称限量子の変数が全て異なる冠頭標準形のことである。 スコーレム標準形は任意の論理式に同値な論理式が存在するとは限らないが、任意のAに対してスコーレム標準形Bが存在し、 Aが充足不能 if…

連言・選言標準形 以下の議論では限量子を含むものは考えない 連言標準形 (P1 ∨ P2)∧(P3 ∨ P4)∧(P5 ∨ P6)のように、∨で結合した節(clause)を∧で結合した形。 選言標準形 (P1 ∧ P2)∨(P3 ∧ P4)∨(P5 ∧ P6)のように、∧で結合したもの（特に名前はない）を∨で結合…

Gの完全性の証明（続き） 復習 公平な導出木 ΦとΨ（各辺の無限経路のある位置以上の位置に存在し続ける論理式の和集合） 任意のシークェントに対して公平な導出木が存在する。 →展開レベルの小さいものから展開する。 補題6.7.6 ※このとき、有限な公理で終了…

Gの完全性 エルブラン解釈 一階言語の部分集合Sについての構造みたいな感じのMについて Mがエルブラン構造で、V(x)=x for all x ∈ Var_s なら、I=(M,V)はエルブラン解釈エルブラン構造 |M|＝Hs=T(Fun_s,Ver_s) M［[f]］(t1,...,tn)=f(t1,...,tn) M［[P]］は…

6.4 その他のシークェント計算 カット規則 等号に関する公理シークェント 等式論理という分野がある。 その他の規則 弱化規則 縮約規則 シークェント計算の健全性 （書けなかった） シークェント計算の完全性 =Γ⇒Δならば├Γ⇒Δ 対偶を証明する。 （全部やる…の…

6.1 シークェント 定義 A1,A2,...,An ⇒ B1,B2,...,Bm 論理式の多重集合同士の関係 解釈Iに対して、I |= A1,A2,...,An ⇒ B1,B2,...,Bm (Iはシークェントを満たす） iff あるiが存在してI［[Ai]］=falseまたはあるjが存在してI［[Aj]］=true iff I |= A1,A2,..…

証明系の健全性 ある証明系において、Φ├{PS}AならばΦ|=Aという証明系を健全であるという。 （PSの推論規則においてΦからAが導けるならばΦを満たすすべての解釈はAを満たす） 証明系の完全性 ある証明系において、Φ|=AならばΦ├{PS}Aという証明系を完全である…

5.1 自然演繹による証明 を証明する。 こういうときは、勝手に選んだ値y=aを決める。 が成り立つことを示せば、任意のaについて、 を証明できる。この証明を木構造で表すと（めんどい） 証明木と推論規則 証明木を定義する Asmp(Π)：証明木Πの上の仮定 Concl…

4.5 意味論的同値 どんな解釈の仕方をしてもAとBは真偽が同じ 定義：すべての付値について 意味論的同値は同値関係である 復習：同値関係 反射的 対称的 ならば 推移的 かつならば 補題4.5.6 変数の名前替えをしたもの同士は意味論的に同値である。 命題4.5.…