自然演繹
自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系 L は、証明の構文規則に関する次のような9つの基本的規則だけを持つ。
仮定の規則 "The Rule of Assumption" (A)
モーダスポネンス "Modus Ponendo Ponens" (MPP)
二重否定の規則 "The Rule of Double Negation" (DN)
条件付き証明の規則 "The Rule of Conditional Proof" (CP)
∧-導入の規則 "The Rule of ∧-introduction" (∧I)
∧-除去の規則 "The Rule of ∧-elimination" (∧E)
∨-導入の規則 "The Rule of ∨-introduction" (∨I)
∨-除去の規則 "The Rule of ∨-elimination" (∨E)
背理法 "Reductio Ad Absurdum" (RAA)
L では、証明は以下のような条件で定義されている。
論理式(wff)の有限な列を持つ。
各行は、L の規則によって正当化される。
証明の最終行が結論であり、証明の前提(群)のみを使って導かれなければならない。また、前提が存在しない場合もある。
前提がない場合、その列を定理と呼ぶ。従って、L における定理は、次のように定義される。
空集合の前提を使って L において証明可能な列
L における空集合の前提から証明可能な列
ある証明の例(モーダストレンス):
別の証明の例(排中律):
自然演繹論理の体系 L の各規則では、入力とエントリの許容できる型が決まっており、その入力で使われる前提の扱い方もそれぞれ決まっている。