テンプレート:推論規則
推論規則（すいろんきそく）とは、論理式から他の論理式を導く規則である。
記号、公理、代入規則、推論規則によって理論を形式化したものを公理系という。
公理は記号だけで記述されるが、推論規則や代入規則はこれらの記号について述べているメタ言語で記述される。
推論規則は恒真式 （トートロジー）から導くのが妥当である。
代表的な推論規則を以下に示す。（⊢は証明を表すメタ言語の記号であり、A0, …, An-1 ⊢ BはA0, …, An-1からBが導かれることを示す。）
- 前件肯定 P, P→Q ⊢ Q
- 後件否定 ￢Q, P→Q ⊢ ￢P
- 否定の導入P → ⊥ ⊢ ￢P
- 普遍例化 ∀xψ(x) ⊢ ψ(a)
- 存在一般化 ψ(a) ⊢ ∃xψ(x)
関連項目
