証明論的意味論

原子システムとは、原子（非論理的）文のストックに対する有限または無限のルールの集合である。通常、2つの形式のルールが認められる。1つは、次の形式の前提ゼロのルールである。

$\displaystyle {\frac {}{P}}\qquad {\text{および}}\qquad {\frac {P_{1}\quad \cdots \quad P_{n}}{P}}}$

場合によっては、原子的な仮定の解除に関する規則も伴う。原子システムは、論理定数に関するいかなるコミットメントにも先行する、原子語彙に関する推論的コミットメントの体系とでも呼ぶべきものを表す。基底とは、許容可能な原子システムのクラスであり、後述するように、異なる基底の選択は異なる論理に対応する。

論理定数を規定する意味節は、次の形式をとる。$\displaystyle {\mathcal {B}}}$基底の範囲: ^{[ 4 ] [ 5 ]}

$\displaystyle \Vdash _{\mathcal {B}}P\quad {\text{iff}}\quad \vdash _{\mathcal {B}}P\qquad (P{\text{ atomic}})}$

$\displaystyle \Vdash _{\mathcal {B}}\varphi \wedge \psi \quad {\text{iff}}\quad \Vdash _{\mathcal {B}}\varphi {\text{ かつ }}\Vdash _{\mathcal {B}}\psi }$

${\displaystyle \Vdash _{\mathcal {B}}\varphi \to \psi \quad {\text{iff}}\quad \varphi \Vdash _{\mathcal {B}}\psi }$

${\displaystyle \Vdash _{\mathcal {B}}\forall x\,\varphi \quad {\text{iff}}\quad \Vdash _{\mathcal {B}}\varphi [x\mapsto t]{\text{ for every closed term }}t}$

$\displaystyle \Delta \Vdash _{\mathcal {B}}\varphi \quad {\text{すべての }}{\mathcal {C}}\supseteq {\mathcal {B}} に対して \Vdash _{\mathcal {C}}\psi {\text{すべての }}\psi \in \Delta に対して \Vdash _{\mathcal {C}}\varphi \quad {\text{が成り立つ場合}$

結果は、基数に関する定量化によって定義される。${\displaystyle \Gamma \Vdash \varphi }$念のため${\displaystyle \Gamma \Vdash _{\mathcal {B}}\varphi }$すべての$\displaystyle {\mathcal {B}}}$選択されたクラスにおいて。拡張に対する量化${\displaystyle {\mathcal {C}}\supseteq {\mathcal {B}}}$推論のための節におけるは、直観主義論理のクリプキ意味論に組み込まれた単調性の構造的対応物であり、新しい原子規則が追加されても結果が維持されることを保証する。

選言、存在、不条理を表す節は、これらの接続詞の最も自然な解釈が直観主義論理の特徴ではないことが判明したため、個別に考察する必要がある。^{[ 6 ]}

${\displaystyle \Vdash _{\mathcal {B}}\varphi \vee \psi \quad {\text{iff}}\quad \Vdash _{\mathcal {B}}\varphi {\text{ or }}\Vdash _{\mathcal {B}}\psi }$

これは、直観主義命題論理では許容されるが導出できないスキーマであるクライゼル・パトナム公理を検証するものであり、結果として得られる論理はウィル・スタッフォードによって探究的論理の変種として特定されている。 ^{[ 7 ]}そこでサンドクヴィストは、システムFやプラウィッツの論文でおなじみの選言の2階定義をモデルにした代替節を提案した。

${\displaystyle \Vdash _{\mathcal {B}}\varphi \vee \psi \quad {\text{iff}}\quad {\text{for every }}{\mathcal {C}}\supseteq {\mathcal {B}}{\text{ and every atom }}P,\ {\text{if }}\varphi \Vdash _{\mathcal {C}}P{\text{ and }}\psi \Vdash _{\mathcal {C}}P,\ {\text{then }}\Vdash _{\mathcal {C}}P}$

並列節は存在量化子を支配し、ex falso quodlibet は次のように規定することで捉えられる。${\displaystyle \Vdash _{\mathcal {B}}\bot }$念のため${\displaystyle \Vdash _{\mathcal {B}}P}$すべての原子に対して${\displaystyle P}$これらの条項の下では、許容される基底の選択（基底が仮説の解除を伴う規則を許容するかどうか、またどのレベルで許容するか）によって、サポート関係によって捉えられる論理が決まります。^{[ 5 ]}

サンドクヴィストは、基底が原子仮定の解除を伴う規則を許容する場合、直観主義命題論理はサポート関係に対して健全かつ完全であり、基底が解除を伴わない規則に限定される場合、含意、不条理、および全称量化子に限定された古典論理は健全かつ完全であることを示した。^{[ 4 ] [ 8 ]}

古典論理と直観主義論理の両方を含む完全な一階述語論理の問題は、2025 年にAlexander V. Gheorghiuによって解決されました。彼は、初等的で構成的かつ証明論的にネイティブな方法によって、両方の種類の一階述語論理の健全で完全な基底拡張意味論を確立しました。 ^{[ 5 ]}この結果はいくつかの点で重要です。許容される基底のみが異なる統一的な枠組みの中で 2 つの論理を扱います。Sandqvist の以前の古典的証明で必要とされたバー帰納法を不要にします。また、David Makinsonの以前の古典命題論理の完全性証明 (基底と古典的評価の対応関係を示すことによって問題を真理関数意味論に還元した) とは異なり^{[ 9 ]}、古典論理のモデル理論的解釈に訴えることなく完全性を確立し、それによって枠組みの推論リソースを独自の条件で示します。

この証明は、もともとサンドクヴィストが命題直観主義の場合に考案し、一階古典論理の設定に大幅に拡張したシミュレーション手法によって進められる。候補となる帰結が与えられた場合、問題となる式の部分式に対するヒルベルト系の導入と消去のステップを模倣する原子規則を持つ基底を構築する。予備定数プールから抽出された固有変数の使用などの補助的な手段によって、量化子規則と開式のシミュレーションが処理される。妥当性の推定証明から、対応する公理的計算における導出を抽出する。

古典論理と直観主義一階述語論理の違いを、許容される基底の違いに還元するという点は、この枠組みの最も顕著な特徴の一つである。接続詞に対応する意味節は両者で同一であり、結果の論理的性質は、原子システム自体の推論資源によって、論理以前のレベルで完全に決定される。

ゲルハルト・ゲンツェンの1934年から1935年の博士論文『論理的演繹に関する研究』 （Untersuchungen über das logische Schließen）は、自然演繹とシーケント計算を導入し、後者のカット除去定理を確立した。 ^{[ 10 ]}その後の考察に影響を与えた一節で、ゲンツェンは、結合子の導入規則は「いわば、関係する記号の定義」を表し、除去規則は「最終的には、これらの定義の結果に過ぎない」と述べている。導入規則が意味を固定し、除去規則がそれに従うというテーゼは、証明論的意味論が発展する種となった。

ゲンツェンの路線に沿って意味論を展開しようとする最初の試みは、ダグ・プラヴィッツによるもので、彼の著書『自然演繹：証明論的研究』（1965年）では、直観主義的自然演繹におけるすべての導出は、最初に導入されてすぐに消去されるような式がない正規形に還元されるという正規化定理が証明された。^{[ 11 ]}その結果として、すべての閉じた導出は、最終段階が導入規則である導出に還元されるということが導かれ、この結果はカリー・ハワード対応と直観主義的型理論の中核をなすものである。

プラウィッツは『証明論におけるアイデアと結果』 （1971年）の中で、固定された原子規則体系と許容可能な還元操作のクラスに関して定義される、推論ステップを用いて構築された論理式のツリーである議論の妥当性の概念を提案した。[ 12 ]^{プラウィッツは、}直観主義的自然演繹はこの概念に関して完全であると推測した。すなわち、すべての妥当な議論は、その体系における導出として複製できる。この推測は後に、ピーチャ、デ・カンポス・サンツ、シュローダー＝ハイスターによって反駁され、プラウィッツのアイデアの最も直接的な形式的表現は、直観主義論理よりも厳密に強い論理を生み出すことが示された。^{[ 6 ]}プラウィッツの意味での証明論的妥当性と、現在一般的に使用されている基底拡張意味論との関係は、アレクサンダー・V・ゲオルギウとデイビッド・ピムによって研究され、両者が一致する条件が特定されている。^{[ 13 ]}

マイケル・ダメットは、ゲンツェン＝プラヴィッツ・プログラムの哲学的含意を数十年にわたって展開し、最終的に『形而上学の論理的基礎』を著した。^{[ 3 ]}ヌエル・ベルナップが接続詞tonkの事例から示唆したことを基に、ダメットは論理的調和の概念を導入した。推論規則の体系は、任意の証明から常に分析的証明を復元できる場合に調和している。これは、シーケント計算ではカット除去によって、自然演繹では正規化によって保証されている。調和を欠く言語は、一貫性のない推論形式を許容し、矛盾を生じやすい。ダメットはこの枠組みを、命題の意味が真理条件ではなく主張可能性条件によって与えられる反実在論的な意味概念を支持するために用い、結果として生じる立場は古典的原理よりも直観主義的原理を自然に支持すると、長々と、そして論争なしにはなかったが論じた。

証明論的意味論という用語は、ピーター・シュローダー＝ハイスターによって1980年代の講義と1991年の出版物で導入されました。 ^{[ 14 ] [ 15 ]}シュローダー＝ハイスターは、このプロジェクトは形式的導出可能性と意味的含意の間の伝統的な関係を逆転させるものではなく、健全性と完全性は形式システムの望ましい特徴のままであり、証明の観点から帰結の意味論的概念を再構築するものであることを強調しています。証明はもはや形式的導出としてのみ理解されるのではなく、論理定数の意味を構成するものとして理解されます。シュローダー＝ハイスターは、ラース・ハルネスとともに、証明論的意味論と論理プログラミングの間の橋渡しとなる、プラヴィッツの反転原理を帰納的に定義された述語に一般化した定義的反射の概念も開発しました。^{[ 16 ]}

証明論的意味論と古典論理の関係は、導入規則を定義とするテーゼが直観主義原理を支持すると解釈されることが多いため、長年にわたり困難の源となってきた。ダメットは、古典的推論と推論的意味論の調和を意味論における最も根本的な問題の一つとして説明した。^{[ 18 ]}サンドクヴィストは、基底を排出のない規則に限定した場合、古典述語論理の断片が基底拡張意味論に対して健全かつ完全であることを示した。 ^{[ 8 ]}その後、マキンソンは、サンドクヴィストの意味での基底と古典的な評価との間の対応関係を示した。^{[ 19 ]}ゲオルギウの1階の結果は、ネイティブな証明論的手段によって完全な1階古典論理の完全性を確立することにより、この流れを完成させた。^{[ 5 ]}

ティモ・エックハルトとデイビッド・ピムは、様相論理のための基底拡張意味論を開発した。この意味論では、基底は可能世界の役割を果たし、事態の記述としての基底の部分的な性質を反映した制約を受けるアクセス可能性関係によって接続される。^{[ 20 ]}この枠組みは、公理 K、T、4、および 5 によって決定される通常の様相論理に対して健全かつ完全な意味論をもたらす。アクセス可能性関係の条件を後から調整すると、S5およびその多様体一般化に対して健全かつ完全な意味論が得られる。

Gheorghiu、Tao Gu、および Pym は、このフレームワークを、収縮と弱化の標準的な構造規則が制限されている部分構造論理に適用しました。 ^{[ 21 ]}基本的な考え方は、原子システムをリソースに敏感にし、仮説の出現をちょうど 1 回だけ放出できるようにし、サポート関係を原子リソースの明示的なパラメータで豊かにすることです。結果として得られる意味論は、直観主義乗法線形論理に対して健全かつ完全であり、さらに加法節を追加することで、加法結合子による拡張に対しても健全かつ完全です。2 番目の原始含意と付随するコンテキスト形成子を使用すると、この構成は、束ねられた含意の論理の意味論をもたらします。