証明論的意味論

証明論的意味論（しょうめいろんてきいみろん、）とは、証明論の一分野であり、論理の意味論へのアプローチである。これによれば、命題および論理結合子の意味は、それらが推論の体系のうちで果たす役割によって説明される。この見方では、証明とは単に、ある事前の意味の割り当てのもとで文が成立することを確立する装置ではなく、むしろ正しい推論のパターンそれ自体が、論理的語彙が意味するものを構成するのである。この立場には哲学的側面と技術的側面の両方がある。哲学的には、論理の正当な主題は真理ではなく論理的帰結の関係であり、意味は推論的役割の関数であるとみなす伝統に立つ。技術的には、ゲルハルト・ゲンツェンの自然演繹およびシークエント計算の分析、直観主義結合子のブラウワー=ハイティング=コルモゴロフ解釈、そして現代形では、原子的規則の体系における証明可能性への参照によって推論の妥当性が定義される形式意味論——なかでも「基底拡張意味論」（）——の家族をつうじて発展してきた。

この枠組みは、論理結合子の導入規則がその定義を提供し、除去規則がそれらの定義に従うものであることを示唆したゲンツェンの所見に起源をもつ。この思想の技術的展開は、ダグ・プラヴィッツの自然演繹についての仕事から始まり、マイケル・ダメットによる論理的調和の説明、そしてとによって導入された形式意味論をつうじて続き、タルスキに由来するモデル論的伝統に対する実質的な代替を生み出した。最も最近の展開には、真理関数的解釈に訴えることなく初等的かつ構成的な手段によって確立された、一階古典および直観主義論理に対する健全かつ完全な基底拡張意味論や、様相論理およびいくつかの部分構造論理への拡張が含まれる。

哲学的動機

証明論的意味論の中心にある意味の構想は、日常的な例によって最も生き生きと描き出される。「タミーは雌ギツネである」が何を意味するかと問われて、人は通常、述語に外延を割り当てた対象の集合を提示するわけではない。むしろ、タミーを雌ギツネと呼ぶことは、彼女が雌でありかつキツネであることにコミットすることであり、その代わりに、雌でありかつキツネであるならば誰でも雌ギツネである、という推論を認めることである、と言う。証明論的意味論者の主張は、論理的語彙についても同じ説明のパターンを精緻にすることができ、そうすることによって少なくとも他の代替案と同程度に技術的実質性をもつ意味論が得られる、というものである。

このテーゼには長い哲学的系譜がある。意味が推論的役割によって与えられるという見解——ロバート・ブランダムに従って「推論主義」と呼ばれることもある——は、ウィルフリッド・セラーズをつうじてゴットロープ・フレーゲの『ベグリフスシュリフト』にまで遡って辿ることができる。ダメットはこの立場に言語哲学において最も持続的な定式化を与えた。意味の理論は、ある表現を理解するとはどういうことかを説明しなければならず、ある表現を理解することはそれを正しく用いる能力をもつことであり、論理定項を支配する推論能力はその意味の把握を構成する、というものである。証明論的意味論は、事実上、この構想を記号論理学の形式的設定のなかで展開したものである。

基底拡張意味論

証明論的意味論の主たる現代的枠組みが「基底拡張意味論」（）である。これは論理定項の意味を、モデルにおける真理ではなく、推論規則の集まりと論理式とのあいだの支持関係（）の観点から定義する。

原子的体系と基底

「原子的体系」()とは、原子的(非論理的)文のストックに対する有限ないし無限の規則の集まりである。通常認められる規則の形式は二つある。すなわち、次の形式の前提なし規則:

であり、これに加えて場合によっては原子的仮定の解消()を含む規則がある。原子的体系は、論理定項に関する任意のコミットメントに先立つ、原子的語彙に関する推論的コミットメントの体系と呼びうるものを表現する。「基底」（）は許容可能な原子的体系のクラスである。基底の選択が異なれば、結果として異なる論理に対応することになる。

支持関係

論理定項を支配する意味論的節は次の形式をとる。ここでは基底にわたる。

帰結はそれゆえ基底にわたる量化によって定義される。すなわち、が成り立つのは、選択されたクラスのなかのすべてのについてが成り立つとき、かつそのときに限る。推論を支配する節における拡張にわたる量化は、直観主義論理のクリプキ意味論に組み込まれた単調性に対する構造的対応物であり、新しい原子的規則が加えられても帰結が保持されることを保証する。

選言・存在・不条理

選言、存在、不条理()に対する節は別途コメントするに値する。なぜならば、これらの結合子の最も自然な解釈が直観主義論理を特徴づけないことが判明するからである。次の読み方:

は、直観主義命題計算では許容可能ではあるが導出可能ではないシェーマであるを妥当にする。結果として得られる論理を、ウィル・スタッフォードは()の一変種として同定した。それに応じてサンドクヴィストは、システムFおよびプラヴィッツの学位論文でなじみのある選言の二階定義に倣った代替的節を提案した。

並行する節が存在量化子を支配し、エクス・ファルソ・クォドリベトは、任意の原子についてが成り立つとき、かつそのときに限りである、と規定することによって捕捉される。これらの節のもとでは、許容可能な基底の選択——基底が仮定の解消を伴う規則を許すかどうか、またどのレベルで許すか——が、支持関係によって捕捉される論理を決定する。

健全性と完全性

サンドクヴィストは、基底が原子的仮定の解消を伴う規則を許すとき、直観主義命題論理が支持関係に対して健全かつ完全であることを示し、また基底が解消を伴わない規則に限定されるとき、含意、不条理、全称量化子に限定された古典論理が健全かつ完全であることを示した。

完全な一階の場合——古典・直観主義の両方——は、2025年にアレクサンダー・V・ゲオルギウによって決着がつけられた。彼は両者の一階述語論理に対する健全かつ完全な基底拡張意味論を、初等的、構成的、かつ証明論的に固有な手段によって確立した。この結果はいくつかの点で意義深い。それは二つの論理を、許容可能な基底のみが異なる統一的枠組みのなかで扱う。また、サンドクヴィストの先の古典的証明に必要であったバー帰納法の技法を不要にする。そしてさらに、の古典命題論理に対する先の完全性証明——これは基底と古典的付値とのあいだの対応を示すことによって、問題を真理関数的意味論に還元したものである——とは異なり、それは古典論理のモデル論的解釈に訴えることなく完全性を確立し、それによって枠組みの推論的資源をそれ自身の用語のうえで示すのである。

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

古典と直観主義の一階論理の差異を、許容可能な基底の差異に還元することは、この枠組みの特に印象的な特徴の一つである。結合子に対する意味論的節は両者の場合で同一であり、帰結の論理的性格はもっぱら、原子的体系それ自体の推論的資源によって、前論理的レベルで完全に固定されているのである。

歴史的展開

ゲンツェン

ゲルハルト・ゲンツェンの1934–35年の学位論文『論理的推論についての研究』（Untersuchungen über das logische Schließen）は自然演繹とシークエント計算を導入し、後者についてカット除去定理を確立した。後続の考察を形作ってきた一節において、ゲンツェンは、結合子の導入規則は「いわば、当の記号の定義を表す」のに対し、除去規則は「最終的に言えば、これらの定義の帰結にすぎない」と述べた。導入規則が意味を定め、除去規則がそれらに従う、というテーゼは、証明論的意味論が成長してきた種子である。

プラヴィッツと議論の妥当性

ゲンツェンに沿った意味論的理論を発展させる最初の試みはダグ・プラウィッツによるものである。彼の『自然演繹——証明論的研究』（Natural Deduction: A Proof-Theoretical Study、1965年）は正規化定理を証明した。すなわち、直観主義自然演繹におけるあらゆる導出は、最初に導入されてすぐに除去される論理式が存在しない正規形へと簡約される。系として、あらゆる閉じた導出は最終ステップが導入規則であるものへと簡約される、という結果が得られる。これはカリー=ハワード同型対応および直観主義型理論の中心にある結果である。

『証明論における観念と結果』（Ideas and Results in Proof Theory、1971年）においてプラヴィッツは、議論（）——所与の形式体系の規則そのものである必要はない推論ステップを用いて構築された論理式の木——に対する妥当性の概念を、固定された原子的規則の体系と許容可能な簡約操作のクラスに相対的に定義することを提案した。プラヴィッツは、直観主義自然演繹はこの概念に関して完全である、すなわちあらゆる妥当な議論は体系における導出として再現できる、と予想した。この予想はその後ピーチャ、デ・カンポス・サンツ、シュレーダー＝ハイスターによって反駁された。彼らは、プラヴィッツの考えの最も直接的な形式的明確化は直観主義論理よりも厳密に強い論理を生み出すことを示したのである。プラヴィッツの意味での証明論的妥当性と、現在一般に用いられている基底拡張意味論との関係はゲオルギウとデイヴィッド・パイムによって研究されており、両者が一致する条件を同定している。

ダメットと調和

マイケル・ダメットはゲンツェン=プラヴィッツのプログラムの哲学的含意を数十年にわたって発展させ、『形而上学の論理的基礎』に結実させた。結合子「tonk」の事例から生じたニュエル・ベルナップの示唆に基づいて、ダメットは論理的調和（）の概念を導入した。すなわち、推論規則の体系が調和的であるのは、シークエント計算についてカット除去によって、自然演繹について正規化によって保証されているように、任意の証明から分析的証明を回復することが常に可能であるとき、というものである。調和を欠く言語は不整合な推論形式を許し、無矛盾性を欠くおそれがある。ダメットはこの枠組みが反実在論的な意味の構想を支持するものと考えた。これは、言明の意味がその真理条件ではなくその主張可能性条件によって与えられるとするものであり、結果として得られる立場は古典的諸原理よりも直観主義的諸原理を自然に支持する、と——詳細に、また論争なしにではないが——論じた。

シュレーダー＝ハイスターと分野の命名

「証明論的意味論」という用語はによって、1980年代の講義と1991年の刊行物において導入された。シュレーダー＝ハイスターは、このプロジェクトが形式的導出可能性と意味論的含意との伝統的関係を逆転させるのではなく——健全性と完全性は依然として形式体系の望ましい特徴である——むしろ、もはや形式的導出としてのみ理解されるのではなく論理定項の意味を構成するものとして理解された証明の観点から、意味論的帰結の概念を再構成するものであることを強調してきた。ラース・ハルネスとともに、シュレーダー＝ハイスターはまた、プラヴィッツの逆転原理を帰納的に定義された述語へと一般化したもので、証明論的意味論と論理プログラミングとのあいだに橋を提供する「定義的反映」()の概念を発展させてきた。

モデル論的意味論との関係

形式言語の意味論に対する20世紀の支配的なパラダイムはタルスキによって確立された。これによれば、論理式が前提の集合の帰結であるのは、のあらゆるモデルがのモデルであるとき、かつそのときに限る。この構想では、帰結とはあらゆる許容可能な解釈にわたって前提から結論への真理の伝達であり、結合子の意味はその真理関数によって与えられる。証明論的意味論は、関連する三つの点について異なる説明を提供する。

説明の順序。モデル論者にとっては、真理は推論に対して概念的に先行する。すなわち、推論が妥当なのはそれが真理を保存するからであり、文の真理条件は証明可能性についてのいかなる問いも生じる前に確定する。証明論的意味論者にとっては、推論が真理に対して概念的に先行する。すなわち、結合子の意味はその推論的役割によって確定し、真理は——もしそれが現れるとしても——派生的な観念である。

意味の所在。モデル論的説明では、論理定項の意味は構造のうちのそれと結びついた意味論的節によって——連言については真理値の最小演算によって、全称量化子については領域にわたる普遍的制限によって——固定される。証明論的説明では、意味は定項を支配する推論規則によって——ゲンツェンの読み方では自然演繹の導入規則によって、現代的定式化では基底拡張意味論の支持節によって——固定される。

帰結の形式。両方の枠組みは、ある構造のクラスにわたる指定された意味論的性質の保存として帰結を定義するが、当の構造は著しく異なる。モデル論的帰結はモデル——非論理的語彙に外延を割り当てる解釈——にわたって量化する。基底拡張意味論は基底——原子的語彙にわたる推論規則の集まり——にわたって量化する。後者は直観主義論理に対するクリプキ意味論と明らかな親近性をもち、実際、基底拡張のもとでの支持関係に組み込まれた単調性条件は、クリプキ・モデルにおける持続性条件に対する構造的対応物である。しかし、違いは実質的である。基底はクリプキ・フレームによって自然に表現されるものより広範な推論的資源を許容し、また証明論的枠組みは、標準的なモデル論的扱いが不自然であるか利用できないさまざまな論理——いくつかの部分構造論理を含む——に対して意味論を提供するのである。

二つの枠組みは単純に競合しているのではない。それぞれが特徴的に異なる種類の洞察を生み出してきた。モデル論的資源への翻訳に依存する証明論的結果——とりわけ古典命題論理に対するマキンソンの完全性証明——は、両者のあいだの実りある相互作用を示している。証明論的意味論の特徴的な哲学的主張は、それが自身の資源のうえに立ちうる、すなわち、意味の推論的説明は事前のモデル論的説明に寄生するものではない、というものである。

拡張

古典論理

証明論的意味論と古典論理との関係は長らく困難の源であった。なぜならば、定義としての導入規則というテーゼは、しばしば直観主義的諸原理を支持するものと解されるからである。ダメットは古典的推論と推論的意味論との調和を、意味の理論における最も根本的な問題の一つと記述した。サンドクヴィストは、基底が解消を伴わない規則に限定されるとき、古典述語論理のある断片が基底拡張意味論に対して健全かつ完全であることを示し、その後マキンソンはサンドクヴィストの意味での基底と古典的付値とのあいだの対応を示した。ゲオルギウの一階の結果は、完全な一階古典論理に対する完全性を固有な証明論的手段によって確立することによって、この線を完結させる。

様相論理

ティモ・エクハートとデイヴィッド・パイムは様相論理に対する基底拡張意味論を発展させた。そこでは基底が可能世界の役割を果たし、事態の記述としての基底のもつ部分的性格を反映する制約に従う接続可能性関係によって接続される。この枠組みは公理 K、T、4、5 によって決定される正規様相論理に対して健全かつ完全な意味論を生み出す。接続可能性関係に対する条件のその後の調整によって、S5 とその多様相一般化に対する健全かつ完全な意味論が得られる。

部分構造論理

ゲオルギウ、タオ・グー、パイムはこの枠組みを部分構造論理——収縮と弱化という標準的構造規則が制限されている——に適応させた。基本的な考えは、原子的体系を資源敏感的にする——仮定の出現を正確に一回だけ解消することを許す——とともに、原子的資源に対する明示的なパラメータをもって支持関係を豊かにすることである。結果として得られる意味論はに対して健全かつ完全であり、さらに加法的節を伴うとその加法的結合子による拡張に対しても、そして第二の原始的含意と付随する文脈形成子を伴うと、()に対する意味論をもたらす。

証明論的意味論シンポジウム

「証明論的意味論シンポジウム」（）は、2019年以来、この分野に特化して毎年開催されてきた国際会議で、新しい結果の発信の主たる場として機能している。各回はいくつかのヨーロッパの研究機関で開催されてきており、シュロス・ダグストゥールやバンフ国際リサーチステーションでの関連ワークショップとも結びついている。シンポジウムで初めて発表ないし実質的に議論された展開には、ピーチャ=シュレーダー＝ハイスターの体系が中間論理であるとするスタッフォードの同定、ピーチャおよびシュレーダー＝ハイスターとともに発表されたいわゆる「スタッフォードの論理」の公理化、エクハートとパイムによる公的発表論理の意味論——のような認識論的パズルの扱いを与える——、ゲオルギウの一階の結果などがある。このシリーズはまた、()、証明の同一性、いわゆる「意味論的汚染」()、推論的意味の分子的説明対全体論的説明など、この分野で未解決のままの哲学的問題を論じる場ともなってきた。

証明論的意味論

Źródło i licencja