logicEL - 41semicolon/41semicolon.github.io GitHub Wiki

述語論理を復習する。Rautenbergの教科書の第2,3章に多くを負っている。

アルファベット: 1階言語の記号は Var={v0,v1,...} ¬,⋀,∀,=。さらに言語ごとに 関係記号, 操作記号, 定数記号 が加わる。例えば 集合論では∈, 数論では S,0,+,*, 群論では ◦, e。なお、⋁,→,↔,∃,∃!,⊤,⊥ は統語的な省略形という形で導入。

項と式の帰納的定義: 項と式 を帰納的に定義するので 項帰納法, 式帰納法, 帰納的定義が正当化できる (例: 深さ, 自由変数, 束縛変数, 衝突判定, 代入, Openな式, 文, PNF, ∀式, ∀∃式, 核, CNF, DNF, 節, ...)

意味論的同値関係・帰結関係: ドメインDとモデル(=構造A+付値w)で 項の値(=Dの元) や 式の値(=充足性)を帰納的に定める。同値関係と帰結関係には二種類の定式化がある: 一方で A,w⊨φ の下で 同値関係≡と帰結関係⊨を定め、他方で 付値の閉包をとったA⊨φの下で同値関係≡A, 帰結関係⊨g を定める。≡ ⊆ ≡A である。また⊨gは演繹定理や場合分けが無条件には成立しない等制約がある(例: x=y ⊨g ∀xy.x=y は成立するが ⊨g x=y→∀xy.x=yは成立しない)ので 基本的には前者を使う。

理論とは: 帰結関係に閉じる文の集合を理論と呼ぶ。理論は 公理系(＝文の集合)を指定する方法や 構造を与える方法(つまり {α∈L0| A⊨α})で指定する。公理系を空集合とした理論 Tautが一番小さい理論で、一番大きい理論は全ての文を覆う不整合な理論。また、理論における式の同値関係 ≡Tや 項の同値関係≈Tもまた定まる。我々のよく使う同値関係は主にこの概念に該当する。

定義と言語の拡張: 新たな記号を意味ありげに導入することを定義による言語の拡張という(例: 数論での<, 群論での-1)。新たな言語において、定義式を公理系に付け加えるという取り扱いになる。定義による拡大はconservativeであるし、逆に記号を削除して議論もできる(消去定理)。よって必要に応じて拡大と縮小を行える。特に重要な例は定数拡大であり、HenkinSetを構成する際によく使われる。

健全性と完全性: 自然演繹をシーケント計算でとらえる。X⊢φの導出列は シーケントに対する基本則の順次適用なので 規則帰納法が正当化される。これにより 自然演繹の健全性: X⊢φ⇒X⊨φ が直ちに従う。完全性は対偶証明。X,¬φ が整合と仮定すると HenkinSet(かつ極大整合) Y まで拡大でき、Yが充足可能なので X,φ は充足不能。

決定性: 式の充足可否を考える。式を≡で PNFに変形し、充足同値関係≈で ∀式に変形する(スコーレムの方法)。その核を命題論理の方法でCNFに変形して節の集合を得る。この集合（を操作して得られる式の集合）の充足不能性こそが もとの式の充足不能性に一致する(エルブランの定理)。よって式が充足不能である場合には その判定は有限のステップで完了する。これを敷衍できる: もし式の集合 X が充足不能であるならば、有限のステップでそう判定できる。つまり、推論の妥当性や妥当式の判定も それがそうである場合には有限のステップで判定可能(述語論理の半決定可能性)。