推論規則

推論規則（すいろんきそく、英: rule of inference, inference rule, transformation rule）とは、論理式から他の論理式を導く推論の規則である。

記号、公理、代入規則、推論規則によって理論を形式化したものを公理系という。 公理は記号だけで記述されるが、推論規則や代入規則はこれらの記号について述べているメタ言語で記述される。 恒真式 （トートロジー）から推論規則を導くと妥当性のある推論になる。

古典論理における推論規則

古典論理における代表的な推論規則を以下に示す。（⊢は推論を表すメタ言語の記号であり、A₀, …, A_n-1 ⊢ BはA₀, …, A_n-1からBが導かれることを示す。）

演繹

• モーダスポネンス　P, P→Q ⊢ Q
• モーダストレンス　￢Q, P→Q ⊢ ￢P
• 否定導入　P → ⊥ ⊢ ￢P
• 普遍例化　∀xψ(x) ⊢ ψ(a)
• 普遍汎化
• 存在例化
• 存在汎化　ψ(a) ⊢ ∃xψ(x)
• 二重否定の除去　￢￢P ⊢ P
• 二重否定の導入　P ⊢ ￢￢P
• 選言三段論法　P∨Q, ￢P ⊢ Q
• 仮言三段論法　P→Q, Q→R ⊢ P→R
• 導出 l∨P, ￢l∨Q ⊢ P∨Q
• 二条件導入
• 二条件除去
• 構成的ジレンマ
• 破壊的ジレンマ

アブダクション（仮説形成）

• 後件肯定　Q, P→Q ⊢ P

関連項目

• シークエント計算 - カット除去定理
• ルイス・キャロルのパラドックス