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

本気で命題論理を復習する。Rautenbergの教科書の第1章に多くを負っている。

Fという言語 : 「括弧と可算無限の原子命題Piと￢,∧,∨」で言語を定める。逆ポーランド記法を使えば括弧は不要だし、↑ なら論理記号は一つで済むはずだし、逆に → を未定義の論理記号として採用することもできた。命題記号に P, Q, ...を割り当てる方法が好みだったり、真偽を表す t, f を採用することもできた。にも関わらず この言語 F を採用する。F 上で各種の（メタな）定理といった道具立てを揃える。その他の方言にはあとで翻訳すればよい。

再帰的な考え方： 論理式に関する述語/性質がある（例：「・・は右括弧と左括弧の数が等しい」、「・は一意分解可能」）。論理式に関する関数がある（例：部分論理式 Sf, ランク rk, 双対 δ, 置換 σ, 値付け w）。これらを定義・構成するために再帰的な考え方が必要（Principle of formula induction、帰納的定義）。

値付けとFnという言語: 原子命題全体 PV から 2 への写像を定めれば、F から 2 への写像が一意に決まる(ように論理記号 と 真理関数 を対応付ける）。この描像の下では、n個の原子命題しか登場しない言語 Fn において、任意の論理式 φ ∈ Fn は n 変数の関数 f ∈ Bn を denote する。逆に、任意の関数 f ∈ Bn を選んだ時に それが何らかの論理式 φ ∈ Fn で denote できるなら Fn の表現力が十分強い (functional complete)といえる。実際 言語 F の表現力は十分強い。

F の類別と標準形: 論理式の二項関係 ≡:「・と・は任意の値付け w において同じ真理値（＝2の元）を持つ」は同値関係なので F を類別する。（F の表現力は十分強いので）同値類の数は Bn の濃度 2^(2^n) に一致し、各同値類には CNF, DNF なる元が存在する。任意の f ∈ Bn が与えられたときに f を denote する CNF/DNF な論理式 φ ∈ Fn を構成する処方がある。

意味論的帰結関係: ⊨ というシンボルは 充足関係(e.g. w ⊨ X)にも 帰結関係 (e.g. X ⊨ α) にも用いられるが混乱は生じない。帰結関係には、RMTS(reflexivity, monotonicity, transitivity, substitution invariance)や、F(finitary)という性質を持つ。また、D(意味論的演繹定理)から、論理的帰結を引くこととトートロジーの確認は同値であることがわかる。なお、 ⊨ ⊆ PowF × F であることに注意（つまり演繹関係 ⊢ と同じ型であり その観点で後に議論する）。

帰結関係: 逆に、RMTSを満たすような関係を一般に帰結関係と呼ぶ。こうすることで古典論理の多くや多値論理といった言語における帰結関係を統一的に扱える。帰結関係の下で、「X は 帰結関係 の下で (maximally) consisitent」といった概念や、「帰結関係 は consisitent」、「X は deductive closure」などの概念を定義できる。

自然演繹: 基本則(IS, MR, ∧1, ∧2, ￢1, ￢2) およびその派生則はゲンツェン流と呼ばれる。すなわち各規則は、n個のシーケント(以降seq.と略)を前件として、1つの seq. を帰結する形。この描像の下で 演繹関係 X ⊢ α は、有限な seq. の列 (S0;S1;...;Sn) where Sn = (X, α) と表現できる。これはステップ実行の過程の記録とみなせる。つまり Sk+1 は S0...Sk から任意の個数の seq. を選び、それに基本則or派生則のどれか一つにあてはめて Sk+1 を得たとみなせる。よって、一般に性質 E ⊆ PowF × F が基本則の適用において保存されるなら、 X ⊢ α ⇒ E(X, α) であるという原則(Principle of rule induction)が正当化できる。

自然演繹の完全性: Principle of rule induction における E の重要な例は 帰結関係 ⊨ である。よって、X ⊢ α ⇒ X ⊨ α 。続いて、X ⊨ α ⇒ X ⊢ α を示すために対偶: X ⊬ α ⇒ X ⊭ α を示す。仮定より X,￢α が consistent であるので、これを maximally consistent な集合 Y に拡大でき(Lindenbaumの定理)、Y は充足可能、よって コンパクト性定理により X, ￢α も充足可能で、よって X, α は充足不能、よってQED。

Hilbert計算: 4つの公理図 Λ (Λ1, Λ2, Λ3, Λ4) と一つの推論規則 MP を用いた 証明関係 X :⊢ α も自然演繹と同じように有限列 Φ = (φ0, φ1, ..,φn) where φn = α というように表現できる。この場合、ステップ実行の過程として、φk+1 は X∪Λ の元であるかもしくは、φ1...φk までのどれか二つを選んでMP を適用したかのどちらかであるというように見なす。したがって、Hilbert版 induction principle が正当化される。すなわち、性質 E ⊆ F (注! X を固定するのでPowF × Fではない) が Λ∪X の任意の元において成立し、かつ Eα,E(α→β) を仮定したときに Eβ が言えるならば、 X :⊢ α ⇒ Eα。顕著な適用例は、（Xを固定した）意味論的帰結関係 ⊨。よって X :⊢ α ⇒ X ⊨ α なる健全性が確かめられる。

Hilbert計算の完全性: 前節で健全性は示された。さて、「X :⊢ α が成立する」という性質は、自然演繹のPrinciple of rule induction を適用できるので、X ⊢ α ⇒ X :⊢ α。あとは ⊢ と ⊨ の同値性から、X ⊨ α ⇒ X :⊢ α となって完全性が示された。