古典論理と様相論理

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

古典論理と様相論理

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

「自然演繹」の記事における「古典論理と様相論理」の解説

話を単純化するため、ここまでの説明では直観論理を使ってきた。古典論理は、直観論理に次の公理あるいは排中律を追加して拡張したものと言える。 「任意の命題 p について、命題 p ∨ ¬p は真である」 この文自体は、導入も除去も明確でない。実は、これは2種類の連結子に関係している。ゲンツェンは、排中律を以下の3つの（等価な）定式化のうちの1つとして扱った。これらはヒルベルトと Arend Heyting の論理体系にも類似の形式で提示されていた。 -------------- XM1A ∨ ¬A true ¬¬A true---------- XM2A true -------- u¬A true⋮p true------ XM3u, pA true この排中律の扱い方は、純粋主義的観点からは好ましくないのに加えて、正規形の定義においてさらなる複雑さを生む。 導入規則と除去規則だけからなる従来からの自然演繹にとって好ましい対処法は、1992年、Michel Parigot が λμ と呼ばれるラムダ計算の一種として提案した。彼の手法の鍵となった洞察は、真理値を中心とした判断 "A true" を、より古典的な記法に置換したことである。局所的形式では、Γ ⊢ A の代わりに Γ ⊢ Δ とした。この Δ は Γ と同様な命題の集合である。Γ は命題群の論理積であるが、Δ は命題群の論理和である。この構造はシークエント計算から直接持ってきたものだが、λμ での新規な点は、古典的な自然演繹的照明に計算的意味を与えた点であり、それには継続あるいはLISPやその後継で見られる throw/catch が用いられる。 もう1つの重要な拡張は様相論理学などの論理に関するもので、それらは単なる基本的な真理値の判断以上のことをする必要がある。1965年に Dag Prawitz が様相論理のための自然演繹的記法を述べており、その後も様々な研究が行われてきた。簡単な例を示すため、必要性の様相論理での新たな判断 "A valid" を考える。これは次のような意味である。 「もし "B true" という形式の前提無しで "A true" ならば、"A valid" である」 この断定的判断は単項結合子 ◻A（"necessarily A"）として表され、以下のような導入規則と除去規則となる。 A valid-------- ◻I◻ A true ◻ A true-------- ◻EA true なお、前提 "A valid" には定義規則がないが、その代わりに妥当性の断定的定義が使われる。この様相は、局所化された形式で仮説を明示的に示すとより明確になる。"Ω;Γ ⊢ A true" と記したとき、Γ は以前のように真なる仮説群を表し、Ω は妥当な仮説群を表す。右辺には単純な判断 "A true" しかない。"Ω ⊢ A valid" は定義から "Ω;⋅ ⊢ A true" と同じ意味であるため、妥当性はここでは不要である。導入規則と除去規則は次の通りである。 Ω;⋅ ⊢ π : A true-------------------- ◻IΩ;⋅ ⊢ box π : ◻ A true Ω;Γ ⊢ π : ◻ A true---------------------- ◻EΩ;Γ ⊢ unbox π : A true 様相仮説には独自の仮説規則と代入定理がある。 ------------------------------- valid-hypΩ, u: (A valid) ; Γ ⊢ u : A true 様相代入定理 Ω;⋅ ⊢ π1 : A true かつ Ω, u: (A valid) ; Γ ⊢ π2 : C true ならば、 Ω;Γ ⊢ [π1/u] π2 : C true である。 このような仮説の集合を区別して判断するフレームワークを、「多項的; polyadic」コンテキストなどと呼び、非常に強力で拡張性がある。様々な様相論理に適用可能で、他にも線型論理や部分構造論理にも適用した例がある。