|
自然演繹（しぜんえんえき、）は、「自然な」ものとしての論理的推論の形式的モデルを提供する証明理論の手法であり、哲学的論理学の用語である。 == 自然演繹論理 == 自然演繹論理のあるバージョンには、公理が存在しない。ジョン・レモンが開発した体系 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 の各規則では、入力とエントリの許容できる型が決まっており、その入力で使われる前提の扱い方もそれぞれ決まっている。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「自然演繹」の詳細全文を読む 英語版ウィキペディアに対照対訳語「 Natural deduction 」があります。 スポンサード リンク
|