自然演繹
自然演繹(しぜんえんえき、英: Natural deduction)は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。
これらの規則で、[t/x] A と書かれている部分は、A に存在する全ての x の実体を t と置換することを意味する(詳しくはラムダ計算を参照されたい)。規則名の上付き文字は、その規則によって排除される要素を意味している。a という項は ∀I の結論には出現しない(このような項をパラメータと呼ぶ)。また、規則 ∃E における仮説名 u と v は、仮説的導出の第二前提に局所化されている。これまでの節で論じてきた命題論理は決定可能だったが、量化子を加えたことで決定不能となる。
ここまで述べた量化表現は「一階; first-order」である。その場合、量化されるオブジェクトと命題は区別される。高階論理ではその部分が異なり、命題は区別されない。命題の量化には量化の範囲があり、それが規則にも反映される。
高階論理における導入規則と除去規則は、ここでは扱わない。一階論理と高階論理の間には様々な段階がある。例えば、二階論理は、項を量化した命題と、命題を量化したものを命題として扱う。