自然演繹論理

ウィキペディア小見出し辞書

自然演繹論理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 09:51 UTC 版)

「自然演繹」の記事における「自然演繹論理」の解説

自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系 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 における空集合の前提から証明可能な列 ある証明の例（モーダストレンス）: p → q, ¬q ⊢ ¬p [Modus Tollendo Tollens (MTT)] 前提番号行番号論理式 (wff)根拠となる規則と使っている行1 (1) (p → q) A 2 (2) ¬q A 3 (3) p A (for RAA) 1,3 (4) q 1,3,MPP 1,2,3 (5) q ∧ ¬q 2,4,∧I 1,2 (6) ¬p 3,5,RAA Q.E.D 別の証明の例（排中律）: ⊢p ∨ ¬p 前提番号行番号論理式 (wff)根拠となる規則と使っている行1 (1) ¬(p ∨ ¬p) A (for RAA) 2 (2) ¬p A (for RAA) 2 (3) (p ∨ ¬p) 2, ∨I 1, 2 (4) (p ∨ ¬p) ∧ ¬(p ∨ ¬p) 1, 2, ∧I 1 (5) ¬¬p 2, 4, RAA 1 (6) p 5, DN 1 (7) (p ∨ ¬p) 6, ∨I 1 (8) (p ∨ ¬p) ∧ ¬(p ∨ ¬p) 1, 7, ∧I (9) ¬¬(p ∨ ¬p) 1, 8, RAA (10) (p ∨ ¬p) 9, DN Q.E.D 自然演繹論理の体系 L の各規則では、入力とエントリの許容できる型が決まっており、その入力で使われる前提の扱い方もそれぞれ決まっている。