0. 前提と表記

古典命題論理をわかっている人向け（少しレベルが高め）
F は全ての論理式を表す集合で、 PowerF はそのべき集合。p,q,r...は原子命題、α,β,...は論理式、X,Y,...は論理式の集合。
メタレベルでの「かつ・または・もし・もしそしてそのときにのみ」をそれぞれ &, ||, ⇒, ⇔ と表記。オブジェクトレベルでは ∧,∨,→,↔ を使う。+はXOR, ↑はNAND, ↓はNOR。⊤,⊥ は恒真・恒偽な論理式で、t,f を対応する定数ブール関数、1,0 を対応するブール値とする。
意味論的帰結関係には ⊨ , シーケント計算で導出可能なシーケント（であるペア）に成立する関係には ⊢ を使う。X⊢α,β は「X⊢α & X⊢β」の略とする（のでゲンツェン流シーケント計算との表記違いに注意)。X⊢Y、X⊨α,β、X⊨Y に関しても同様。

1. 表現適格性

注：（命題論理というよりもその意味論である）ブール代数に閉じた話。

表現適格なブール関数の組み合わせ例:

表現適格.txt

{↑}, {↓}, {￢,∧}, {￢,∨}, {→, f}

極大で不適格なブール関数の組み合わせは (項同値性を除いて) 5種類のみ:

5種類の互いに異なる極大な表現不適格.txt

{∧,∨,t,f}
{→,∧} と その双対
{↔,￢}
{d3,￢}  where d3(x,y,z) := x∧y∨y∧z∨z∧x (d3は自己双対)

互いで互いを定義:

シグネチャ同士の相互定義.txt

t: p∨￢p, p+￢p
f: p∧￢p, p↔￢p 
￢: p+t(), p↔f(), p→f(), p↑p, p↓p, 
∧: ￢(￢p∨￢q), ￢(p→￢q), ￢p↓￢q
∨: ￢(￢p∧￢q), ￢p↑￢q
→: ￢p∨q, ￢(p∧￢q)
↔: p∧q∨￢p∧￢q, (p→q)∧(q→p), p+￢q
+: p↔￢q

2. 帰結関係

PowerF×F 上の関係 ⊢, ⊨ は、以下の性質(R)(M)(T)(S)(F)(D)を持つ。一般に、(R)(M)(T) を満たす関係を帰結関係と呼び、さらに(S)を満たす帰結関係を構造的な帰結関係と呼ぶ:

(R) α ⊨ α                                     (reflexivity)
(M) X ⊨ α & X ⊆ X' ⇒ X' ⊨ α                 (monotonicity)
(T) X ⊨ Y & Y ⊨ α ⇒ X ⊨ α                    (transitivity)
(S) X ⊨ α ⇒ Xσ ⊨ ασ                          (substitution invariance)
(F) X ⊨ α ⇒ X0 ⊨ α なる有限な部分集合X0が存在  (finiteness)
(D) X,α ⊨ β ⇒ X ⊨ α→β                        (deduction theorem)

帰結関係により、整合などの概念や関連する定理を展開できる:

(定義) Xは不整合: X ⊢ ⊥
(定義) Xは整合: X が不整合でない
(C+) X ⊢ α ⇔ X,¬α ⊢ ⊥; (C-) X ⊢ ¬α ⇔ X,α ⊢ ⊥
(定義) Xが極大整合： Xが整合で、任意の Y⊃X において Y は不整合
(LI) X が整合ならば、極大整合な Y⊃X が存在
(MC) Yが極大整合の時、 Y ⊢￢α ⇔ α ∉ Y; Y ⊢α∧β ⇔ α,β∈Y;
(sat) Yが極大整合の時、Y は充足可能

「X⊢α ⇔ X⊨α」が完全性。⇒は基本規則適用において ⊨で示される性質が保存されることから帰納的に示せて、⇐は対偶を考えると X∪{￢α} の整合性の問題に帰着し、(LI)(sat)を使ってその充足可能性から示せる。(S)を使ったエレガントな証明法もある。

3. 恒真式・同値な式・妥当な推論

恒真式を列挙するよりも演繹定理(D) を使って、同値な式や妥当な推論を列挙した方が役に立つことが多い。

まずは基本となる￢∧∨に関する同値な式:

α∧(β∧γ) ≡ α∧β∧γ, α∨(β∨γ) ≡ α∨β∨γ    (associativity);
α∧β ≡ β∧α, α∨β ≡ β∨α                   (commutativity);
α∧α ≡ α, α∨α ≡ α                         (idempotency);
α∧(α∨β) ≡ α, α∨α∧β ≡ α                 (absorption);
α∧(β∨γ) ≡ α∧β∨α∧γ                     (∧-distributivity);
α∨β∧γ ≡ (α∨β)∧(α∨γ)                   (∨-distributivity);
¬(α∧β) ≡ ¬α∨¬β, ¬(α∨β) ≡ ¬α∧¬β         (de Morgan rules).

→関連の恒真式

p→p                       (self-implication)
(p→q)→(q→r)→(p→r)         (chain rule)
(p→q→r)→(q→p→r)           (exchange of premises)
p→q→p                     (premise charge)
(p→q→r)→(p→q)→(p→r)       (Frege’s formula)
((p→q)→p)→p               (Peirce’s formula)

Coq で証明した:

Require Import Classical.
Section PropositionLogic.
Variable P Q R S T U: Prop.

Goal P->P.
Proof. intro. assumption. Qed.
Goal (P->Q)->(Q->R)->(P->R).
Proof. intros. apply H0. apply H. assumption. Qed.
Goal (P->Q->R)->(Q->P->R).
Proof. intros. apply H. assumption. assumption. Qed.
Goal P->Q->P.
Proof. intros. assumption. Qed.
Goal (P->Q->R)->(P->Q)->(P->R).
Proof. intros. apply H. assumption. apply H0. assumption. Qed.
Goal ((P->Q)->P)->P. (* Classical *)
Proof. intro. apply imply_to_or in H. destruct H. apply imply_to_and in H.
  destruct H. assumption. assumption. Qed.

→関連の同値な式には重要なものが多い:

α→β ≡ ￢β→￢α                                    (contraposition)
α→β∧γ ≡ (α →β)∧(α →γ); α→β∨γ ≡ (α →β)∨(α →γ) (→-left-distributivity) 
α∧β→γ ≡ (α →γ)∨(β →γ); α∨β→γ ≡ (α →γ)∧(β →γ) (→-right-distributivity)
α1 → α2 → ...→ αn ≡ α1∧ ···∧αn−1 → αn

妥当な推論と、妥当な推論に関する定理(≒シーケント計算の導出規則):

α,α→β ⊨ β                     (modus ponens)
α→γ,β→γ ⊨ α∨β→γ              (constructive dilemma)
α→β,β→γ ⊨ α→γ                 (chain/transition)

X ⊨ ⊥ ⇒ X ⊨ α               (explosion)
X,￢α ⊨ ⊥ ⇒ X ⊨ α           (reductio ad absurdum)
X,￢α ⊨ α ⇒ X ⊨ α            (￢-elimination)
X,α ⊨ β ⇒ X ⊨ α→β            (deduction theorem)
X ⊨ α,α→β ⇒ X ⊨ β            (detachment)
X ⊨ α & X,α ⊨ β ⇒ X ⊨ β      (cut rule)
X,α ⊨ β & X,¬α ⊨ β ⇒ X ⊨ β   (proof by cases)