命題論理チートシート
0. 前提と表記
- 古典命題論理をわかっている人向け(少しレベルが高め)
- F は全ての論理式を表す集合で、 PowerF はそのべき集合。p,q,r...は原子命題、α,β,...は論理式、X,Y,...は論理式の集合。
- メタレベルでの「かつ・または・もし・もしそしてそのときにのみ」をそれぞれ &, ||, ⇒, ⇔ と表記。オブジェクトレベルでは ∧,∨,→,↔ を使う。+はXOR, ↑はNAND, ↓はNOR。⊤,⊥ は恒真・恒偽な論理式で、t,f を対応する定数ブール関数、1,0 を対応するブール値とする。
- 意味論的帰結関係には ⊨ , シーケント計算で導出可能なシーケント(であるペア)に成立する関係には ⊢ を使う。X⊢α,β は「X⊢α & X⊢β」の略とする(のでゲンツェン流シーケント計算との表記違いに注意)。X⊢Y、X⊨α,β、X⊨Y に関しても同様。
1. 表現適格性
注:(命題論理というよりもその意味論である)ブール代数に閉じた話。
表現適格なブール関数の組み合わせ例:
{↑}, {↓}, {¬,∧}, {¬,∨}, {→, f}
極大で不適格なブール関数の組み合わせは (項同値性を除いて) 5種類のみ:
{∧,∨,t,f}
{→,∧} と その双対
{↔,¬}
{d3,¬} where d3(x,y,z) := x∧y∨y∧z∨z∧x (d3は自己双対)
互いで互いを定義:
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)
Author And Source
この問題について(命題論理チートシート), 我々は、より多くの情報をここで見つけました https://qiita.com/41semicolon/items/ada28f4ca8f17e1ffa38著者帰属:元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。
Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .