💻 computer science

Inference-Behaviour Semantics for All $^\ast$ Connectives in Two-Dimensional Sequent Calculi

本論文は、二次元シーケント計算における1万組を超える連結子規則ペアを体系的に分析することで、21の有意義な連結子を特定し、様々な論理体系にわたるそれらの意味論的相互関係を精密にマッピングし、直観主義的連結子が古典的連結子の意味の正確に半分を捉えていることを明らかにすることにより、新たな推論・振る舞い意味論（I-bS）アプローチを検証するものである。

原著者： Sophie Nagler

公開日 2026-07-23

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Sophie Nagler

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

ある言葉の「真の意味」を理解しようとしている場面を想像してみてください。辞書的な定義こそが意味だと考えるかもしれませんが、ある哲学者や論理学者のグループは、意味とは actually 「使用」 に関するものであると主張しています。それは自転車の乗り方を学ぶのに似ています。マニュアルを読んで「サイクリング」を理解するのではなく、ペダルを漕ぎ、バランスを取り、ハンドルを切るという「動作」を通じて理解するのです。形式論理学の世界において、これらの「言葉」は**連結子（connectives）と呼ばれる記号（「かつ」、「または」、「否定」など）です。何十年もの間、論理学者は、証明の規則がいかにこれらの記号の使用を規定しているかを見ることで、これらの記号の真の意味を解明しようとしてきました。この分野は証明論的意味論（proof-theoretic semantics）**と呼ばれます。大きな問いは、もしゲームのルール（論理）を変えたら、言葉の意味も変わってしまうのか？それとも、文脈に関わらず一定に保たれる、各連結子の核となる不変の「魂」が存在するのか？ということです。

この論文は、**推論挙動意味論（Inference-Behaviour Semantics: I-bS）**という新しい手法を用いて、この問いを深く掘り下げます。I-bSは、単に紙の上のルールを見るのではなく、記号が最も削ぎ落とされた、最小限の環境の中で自らの存在を証明しようとする際に、どのように振る舞うかを観察するハイテクスキャナーのようなものだと考えてください。著者たちは、あらゆる可能な論理連結子の規則の書き方を検証し、その中でどの規則が独自の、意味のある「指紋」を持つのかを調べようとしました。彼らは単に推測したのではなく、どのルールが生き残り、どのルールが崩壊するかを見るために、巨大なテスト場を構築したのです。

大いなる連結子のセンサス（調査）

著者たちは、驚くべき数の可能性をテストすることに挑みました。それは10,816通りの異なる規則ペアです。すべてのマス目が、最大2つの開始ステップと2つの構成要素を用いて論理的な「言葉」を定義する異なる方法を表す、巨大なグリッドを想像してください。彼らはこれら10,816の候補を、彼らの「最小導出関係（minimal derivability relation）」へと投入しました。この関係は、推論の絶対的な基礎のみを含む、小さな空っぽの部屋のようなものです。そこには「AはAである（恒等式）」というルールと、「もしAからBへ、そしてBからCへと至るなら、AからCへと至る」というルール（カット）だけが存在します。これは論理学におけるサバイバルキットのようなもので、飾り立てた機能や追加の道具はなく、ただ本質的なものだけが存在します。

目標は、これら10,816の候補のうち、どれがこの「部屋」の中で「定義可能」であることを証明できるかを見ることでした。定義可能であるためには、以下の2つの厳しいテストに合格しなければなりませんでした。

保守性（Conservativity）： それ自体がなくても可能であったはずの新しい事柄を、魔法のように証明してはならない。公平に振る舞う必要がある。
一意性（Uniqueness）： それは、自分が行うことができる唯一のものでなければならない。もし別の記号が全く同じ仕事ができるのであれば、それは独自の特別な意味を持つほどユニークではない。

フィルター：10,816から21へ

塵が収まったとき、結果は驚くほど限定的なものでした。10,816の候補のうち、最初のテスト（保守性）を通過したのはわずか376個でした。しかし、二番目のテスト（一意性）を適用すると、リストはさらに縮小しました。最終的に、著者たちは正確に21個の連結子が「最小限の意味を持つ」ことを発見しました。

これら21の生存者こそが、論理的な言葉の「純粋な」バージョンです。これらには以下が含まれます。

ボトム（Bottom）とトップ（Top）： 論理的な「偽」と「真」に相当するもの。
2種類の否定： 直観主義論理における「否定（慎重な否定）」と、二重直観主義論理における「否定（より攻撃的な否定）」。論文では、私たちが日常の数学で使う「古典的」な否定は、これら2つの異なる意味を混ぜ合わせたものであることが示されています。
連言（かつ/Conjunctions）： 「加法的（additive）」なバージョン（標準的な「かつ」のようなもの）と、「乗法的（multiplicative）」なバージョン（リソースを消費する、より厳格な「かつ」）。
選言（または/Disjunctions）： 同様に、標準的な「または」と、より厳格な「分裂（fission）」バージョン。
。
含意（ならば/Implications）： 右含意（right-implication）と左含意（left-implication）があり、それぞれに加法的および乗法的な性質があります。
逆および反転（Converses and Inverses）： 論文では、これらの連結子が反転したり、裏返されたりした意味のあるバージョンも見出しています。

残りの10,795の候補はどうなったでしょうか？それらは拒絶されました。中には、紙の上では異なって見えるが、実際には勝者である21個と同じ挙動を示すだけの「過剰な連結子（bloctnectives）」もありました。また、保守的でないもの（部屋のルールを破るもの）や、一意性を持たないもの（他の記号と区別がつかないもの）もありました。

「半分の意味」の発見

最も遊び心があり、かつ深遠な発見の一つは、これらの意味がどのように変化するかに関するものです。この論文は、古典論理（ほとんどの数学で使用される標準的な論理）が、異なる材料を混ぜ合わせるブレンダーのようなものであることを示しています。

例えば、古典論理では、通常「かつ」を一つのものとして考えます。しかし、この論文は、古典的な「かつ」が、実は加法的な「かつ」と乗法的な「かつ」という、2つの異なる意味のブレンドであることを示しています。あなたが直観主義論理（コンピュータサイエンスや構成的数学で使用される論理）に切り替えると、乗法的なバージョンが失われます。あなたは加法的なバージョンだけが残された状態になります。

著者たちは、直観主義的な否定、選言、および含意が、それぞれ古典的な対応物の意味の半分しか捉えていないと結論付けています。それはまるで、古典論理が「私はフルサンドイッチだ」と言っている一方で、直観主義論理は「私はパンだけだ」、そして二重直観主義論理は「私は具材だけだ」と言っているようなものです。どちらかが「間違っている」わけではありませんが、彼らは材料の半分しか使っていないのです。

なぜこれが重要なのか

これは単なる記号の分類ゲームではありません。この論文は、**推論挙動意味論（Inference-Behaviour Semantics）**という、意味を理解するための新しい方法を検証しています。この方法が、ノイズを自然にフィルタリングし、論理学者が数十年にわたって研究してきたまさにその21個の連結子を残したことを証明することで、著者たちはこの手法が有効であることを示しています。これは、論理的な言葉の「意味」とは、私たちが恣意的に発明するものではなく、極限まで削ぎ落とした本質的な状態において、それがどのように振る舞うかを見ることで「発見」されるものであることを示唆しています。

この論文は、論理のあらゆる謎を解明したと主張しているわけではありません。より複雑な規則や異なる種類の論理において、これがどのように機能するかについては未解決の問いを残しています。しかし、生き残った21個の連結子について、私たちは今や、それらの意味に対する、規則に依存しない精密な地図を手に入れたのです。「かつ」は単なる「かつ」ではなく、「否定」は単なる「否定」でもありません。それらは複雑で多面的なツールであり、この論文はついに、それらを識別するための設計図を与えてくれたのです。

技術的要約：二次元シーケント計算における全∗接続詞の推論・振る舞い意味論

1. 問題提起

本論文は、証明論的意味論（P-tS）における中心的な課題、すなわち、異なる論理体系（古典論理、直観主義論理、線形論理、および双対直観主義論理など）にわたって、論理接続詞の「意味不変な」意味論的説明をどのように提供するかという問題に取り組んでいる。モデル論的意味論（M-tS）や基底拡張意味論（B-eS）といった従来の接近法は、しばしば「グローバリズム」に陥る。これは、論理を変更すると接続詞の意味（例：古典的な「かつ」と直観主義的な「かつ」）までも変更しなければならないという問題である。これにより、論理的な相違が、共有された概念に関する実質的な相違ではなく、単なる定義の違いによるコミュニケーションの不全へと還元されてしまう。

本論文が扱う具体的な問題は、Nagler [Nag26] によって提案された新しいアプローチである「推論・振る舞い意味論（Inference-Behaviour Semantics: I-bS）」の、体系的かつ形式的な実装の欠如である。I-bSは、接続詞の「最小限の推論的振る舞い」を孤立させてその意味を定義するという有望な枠組みを提供しているが、これまでは、可能な接続詞ルールの空間全体にわたる包括的な技術的評価を欠いていた。本論文の目的は、広範で非構造的な候補接続詞の集合に対してI-bSを適用することで、特定の構造規則（弱化や縮約など）に依存しない、個別の最小限の意味を保持する接続詞が果たして存在するのかどうかを判定し、I-bSを検証することにある。

2. 方法論

本研究は、最小の設定における接続詞の推論的使用に基づいて、接続詞の「意味」を測定するという、厳密でデータ駆動型のプローチを採用している。

2.1 調査対象：All∗Connectives（全∗接続詞）

著者らは、調査範囲を、以下の制約に従う二次元シーケント計算において定式化可能な演算ルール対（operational rule pairs）である all∗connectives と定義する。

演算ルール： 個別であり、明示的であり、かつ対称的であること（定義3）。
制約： 前件シーケントは最大2つ、能動的な論理式はルールあたり最大2つまで。
全空間： これにより、正確に 10,816 個の構文的に一意なルール対（前件の形状と能動的な論理式の位置の組み合わせ）が得られる。

2.2 テスト環境：最小可導関係

特定の論理の構造的特徴から接続詞の意味を分離するため、著者らは以下の最小限の背景計算を用いる。

恒等性 ( $Id_{pr}$ ): 原始的な論理式のみに限定される。
カット ( $Cut_{cd}$ ): 文脈を区別するカット規則。
構造的仮定: 交換（マルチセット）を仮定するが、弱化と縮択は除外する。これは多くの論理に共通する「部分構造的核（substructural kernel）」を表している。

2.3 測定装置：推論の振る舞い

核心となる指標は、最小の計算体系内での定義可能性が証明される際に、接続詞が示す構文的パターンである 推論の振る舞い（inference behaviour） である。

定義可能性の基準: Belnap [Bel62] に従い、接続詞が計算体系に加わった結果、保存的拡張（conservative extension）（接続詞なしでは新しい定理が生じない）となり、かつ 一意性（uniqueness）（接続詞が同型を除いて一意に決定される）を持つ場合、その接続詞は定義可能であるとする。
意味論的節（Semantic Clause）: 接続詞の「意味」は、最小の推論の振る舞いのプロファイル（定義可能性の証明中に、接続詞とその能動的な論理式が占める構成要素の位置の最短リスト）をもたらす、その接続詞の 最小の演算ルール対 として特定される。

2.4 データ生成と分析

著者らは、10,816個の候補を体系的にフィルタリングする。

フィルター1（定式化可能性）: 全10,816個のルール対。
フィルター2（保存性）: 正のケースに対してカット除去を証明し、非保存的なケースに対して反例を構成する。これにより、集合は 376 個の保存的な接続詞へと減少する。
フィルター3（一意性）: 水平的および垂直的な相互導出可能性を確立する。これにより、集合はさらに 150 個の一意に定義可能な接続詞へと減少する。
最小性分析: 150個の定義可能な接続詞の中で、著者らは「最小限の意味を持つ接続詞」と「ブロットネクティブ（bloatnectives：構文的な冗長性を持つ等価な接続詞）」を区別する。前件の型における最小性（前件シーケントの最小カーディナリティ）の基準を適用することで、真に最小限の意味的節を孤立させる。

3. 主な貢献と結果

3.1 21個の最小限の意味を持つ接続詞の特定

主要な結果は、正確に 21 個の最小限の意味を持つ接続詞の特定である。これらは、馴染みのある論理定数とその共役（converse）または逆（inverse）に対応するが、加法的（格子型）バージョンと乗法的（群型）バージョンの厳密な区別がある。

零項（Nullary）: 下限 ( $\bot$ ) および上限 ( $\top$ )。
単項（Unary）: 2種類の否定（直観主義的否定 $\neg$ と双対直観主義的否定 $\sim$ ）、および「自明な」共役否定。
二項（Binary）:
- 連言（Conjunction）: 加法的 ( $\sqcap$ ) および乗法的 ( $\otimes$ )。
- 選言（Disjunction）: 加法的 ( $\sqcup$ ) および乗法的 ( $\oplus$ )。
- 含意（Implication）: 加法的右 ( $\rightsquigarrow$ )、乗法的右 ( $\to$ )、加法的左、および乗法的左。
- 共役および逆: 上記のそれぞれについて、その共役（構成要素の入れ替え）および逆に関する明確な意味的節が存在する。

3.2 意味的節と枠組み

本論文は、これら21個の接続詞の各々に対して、明示的な意味的節（最小のルール対）を提供する。決定的なのは、これらの意味が 論理に依存しない ことを示している点である。例えば、乗法的連言 ( $\otimes$ ) の意味的節は、それが線形論理、古典論理、または直観主義論理のいずれに現れるとしても同一である。これらの接続詞が完全な論理（例：古典論理における $\otimes$ と $\sqcap$ の等価性）においてどのように振る舞うかの違いは、接続詞の核となる意味の変化ではなく、構造的リソース（縮約や弱化）に起因するものである。

3.3 様々な論理における意味論的相互関係

本研究は、これら21個の接続詞の論理的適合性を様々な論理間でマッピングしている。

古典論理 (LK): 連言、選言、および含意の加法的バージョンと乗法的バージョンを混同（同一視）する。また、2種類の否定も混同する。
直観主義論理 (LJ): 連言と選言の加版本的、および「右」の含意とは互換性があるが、古典的否定の「半分」の成分（具体的には $\sim_{min}$ を除く $\neg_{min}$ ）のみを捉える。
双対直観主義論理 (LDJ): 古典的否定のもう一方の半分 ( $\sim_{min}$ ) および他の接続詞の双対を捉える。
線形論理 (LL): これら21個の接続詞すべてを区別し、それらを意味的に異なるものとして扱う。

3.4 I-bSの検証

本論文は、特定の論理へのバイアスを持たず、可能なルールを盲目的に網羅的に探索した際に、理論が自然に既存の論理体系に見られる標準的な接続詞へと収束することを示すことで、推論・振る舞い意味論（I-bS） の検証を主張している。「ノイズ」である他の10,795個のルール対が、定義不可能または非最小であるとしてフィルタリングされる事実は、この理論に対する「サニティ・チェック（妥当性確認）」として機能している。

4. 意義と主張

本論文は、その知見を 推論・振る舞い意味論（I-bS） 枠組みの検証として位置づけている。その意義は以下の通りである。

論理独立性: 接続詞の意味を、異なる論理間で不変なものとして定義する方法を提供する。論理を変更すること（例：弱化を加えること）は、接続詞の意味を変えるのではなく、接続詞が作用する 構造的コンテキスト を変えるだけである。
意味変化の解決: なぜ古典論理と直観主義論理が相違して見えるのかについて、意味論的な説明を与える。両者は必ずしも「かつ」や「または」の意味に関して相違しているのではない。むしろ、どの最小限の接続詞を相互作用させ、どの構造規則を許可するかにおいて異なっているのである。例えば、古典的な「かつ」は、2つの異なる最小の意味（ $\otimes$ と $\sqップ$ ）の混同であり、一方で直観主義的な「かつ」は厳密に $\sqcap$ である。
存在論的な節約性: 外部のモデルや基底を必要とせず、証明体系の「部分構造的核」のみに依拠している。
網羅性: 与えられた制約下での定式化可能な全ルールの空間をカバーすることで、本論文は、二次元シーケント計算における最小限の意味を持つ接続詞の完全な分類を提供したと主張している。

著者らは、結果が特定の制約（前件2つ、能動論理式2つ、特定の最小計算）に依存していることを認め、範囲については謙虚な姿勢を保っており、今後の課題として多次元計算、量子化、または代替的な最小可導関係の探索を挙げている。しかし、定義された範囲内において、本論文は I-bS が論理接続詞の原始的な意味を抽出することに成功したと断言している。