古典論理の推論規則から3値論理の演算を補完する
はじめに2値論理
通常の論理学は論理演算fに真(True),偽(False)いずれかの引数を2つ取り,同様に真偽のいずれかの値を1つ返します.
以下に2値論理におけるEqual, NotEqual, And, Or, Implication, Notを表としてまとめます.左から左辺,右辺,評価結果と並んでいます.
Equal : x = y | ||
---|---|---|
T | T | T |
T | F | F |
F | T | F |
F | F | T |
NotEqual : x /= y | ||
---|---|---|
T | T | F |
T | F | T |
F | T | T |
F | F | F |
And : x ∧ y | ||
---|---|---|
T | T | T |
T | F | F |
F | T | F |
F | F | F |
And : x ∨ y | ||
---|---|---|
T | T | T |
T | F | T |
F | T | T |
F | F | F |
Impl : x ⇒ y | ||
---|---|---|
T | T | T |
T | F | F |
F | T | T |
F | F | T |
Not : ¬x | |
---|---|
T | F |
F | T |
見やすいようにひとつのテーブルにまとめます.
LHS | RHS | ∧ | ∨ | ⇒ | ¬ |
---|---|---|---|---|---|
T | T | T | T | T | F |
T | F | F | T | F | |
F | T | F | T | T | T |
F | F | F | F | T |
含意(Implication)についてはAndとNotを使った表現方法があり,以下と同値です.
また,古典論理に限ってド・モルガンの法則を使って次のように変形できます.
2値論理における推論規則
推論とは「AならばB」のことで,推論規則とはImplicationの形で与えられる論理式の真偽を判定するための規則です.と書きます.ただしここでは論理演算Implicationとは区別し,演算子の優先順位を1つ下げます.
古典論理における推論規則には以下の11があります.また,詳細は後述しますが,3値論理を導入する際に古典論理との整合性を保つためにこの推論規則から3値目の論理値の振る舞いを制約としてある程度決定することができます.
前件肯定:
後件肯定:
否定導入:
二重否定の除去:
二重否定の導入:
選言三段論法:
仮言三段論法:
導出:
普遍例化:
存在汎化:
後件肯定:
推論規則から3値目の値の振る舞いを決定する
前置きが長くなってしまいました.このエントリで本当に述べたかったことはここの節からです.
3値目の値をUとするならば,当然,その値の推論規則による振る舞いが決定されていなければなりません.そしてその振る舞いは古典論理の拡張であるならば自由に決定できるものではなく,制約を満たした上で決定されます.
その制約を得てみましょう.アルゴリズムは各推論規則に対し自由変数にUを代入して変数を消去することによって進行します.以下の通りです.
1. 推論において,左辺に出現する自由変数にUを代入したときにRHSをTrueにする式の形から論理演算を決定する.
2. 推論において,AをTrueにする変数の組み合わせがBへの制約条件となり,B中に存在する自由変数にUを代入する.そのあとの方針は1と同じ.
前件肯定: 前件肯定: P, P -> Q |- Q より T, T -> U |- U よって T -> U = T 後件否定: ¬Q, P -> Q |- ¬P より ¬F, U -> F |- ¬U よって U -> F = T 否定導入: P -> F |- ¬P より U -> F |- ¬U よって U -> F = T 二重否定の除去: ¬¬P |- P より ¬U = x1 ¬x1 = x2 x2 -> U = T より ¬U = F ならば ¬U = F = x1 ¬F = T = x2 T -> U = T よって ¬U = F -- 3 二重否定の導入: P |- ¬¬P よって ¬U = F U -> ¬¬U = U -> ¬F = U -> T = T 選言三段論法: P ∨ Q, ¬P |- Q より F ∨ U, ¬F |- U よって F ∨ U = T T -> U = T 仮言三段論法: P -> Q, Q -> R |- P -> R より U -> Q, Q -> R |- U -> R より U -> T, T -> T |- U -> T よって U -> T = T P -> U, U -> R |- P -> R より P -> U, U -> T |- P -> T より T -> U, U -> T |- T -> T F -> U, U -> T |- F -> T U -> U, U -> T |- U -> T よって U -> U = T U -> T = T P -> Q, Q -> U |- P -> U より T -> T, T -> U |- T -> U T -> U, U -> U |- T -> U F -> T, T -> U |- F -> U F -> F, F -> U |- F -> U F -> U, U -> U |- F -> U U -> T, T -> U |- U -> U U -> F, F -> U |- U -> U U -> U, U -> U |- U -> U よって F -> U = T 導出: L ∨ P, ¬L ∨ Q |- P ∨ Q より T ∨ T, ¬T ∨ U |- T ∨ U よって F ∨ U = T T ∨ U = T F ∨ T, ¬F ∨ U |- T ∨ U よって T ∨ U = T T ∨ U, ¬T ∨ T |- U ∨ T よって U ∨ T = T F ∨ U, ¬F ∨ T |- U ∨ T よって F ∨ U = T F ∨ U, ¬F ∨ F |- U ∨ F よって U ∨ F = T 後件肯定: Q, P -> Q |- P より T, U -> T |- U よって U -> T = T T -> U = T
以上の手続きから3値目の値に対する論理演算の一部が得られました.
前件肯定より
後件否定より
二重否定の除去より
二重否定の導入より
選言三段論法より
仮言三段論法より
仮言三段論法より
導出より
実際には,古典論理からの互換性が必須でないため,論理演算の妥当性を優先するならば推論規則をいくつか棄却して制約条件を得なければなりません.