Labelled Sequent Calculi for Propositional Team Logics

論理パズルを解こうとしている場面を想像してみてください。伝統的な方法（「タルスキ的意味論」と呼ばれます）では、ただ一つの特定の角度からパズルを見ます。「この記述は、まさにこの一点において真であるか？」と問いかけるのです。

しかし、この論文の著者たちは、これとは異なる種類の論理であるチーム意味論（Team Semantics）を用いています。単一の地点を見るのではなく、一つのチームとして共に立っている人々の集まりを見ていると考えてください。記述がただ一人の個人に対して真であるかどうかを問うのではなく、その記述が、一つのグループ全体として行動しているときに真であるかどうかを問うのです。

この「チーム」のアプローチは、データベースにおける変数の依存関係（例：「価格は色に依存するか？」）を明らかにしたり、言語における質問の意味（例：「雨が降っている、あるいは雪が降っている、というのは真か？」）を理解したりするといった、現実世界のシナリオで使用されます。

問題：チームに関する証明方法

著者たちは、これらのチームに関する記述が真であるか偽であるかを証明するためのルール（「計算機」のようなもの）を作成したいと考えました。彼らはこれを**ラベル付きシーケント計算（Labelled Sequent Calculi）**と呼んでいます。

「シーケント」を天秤と考えてみてください。片側には、あなたが知っている事実のリスト（チームの現在の状態）があり、もう片側には、証明したい結論があります。目標は、もし左側の事実が真であれば、右側の結論も必ず真になることを示すことです。

この論文では、4つの異なるタイプのチーム論理に対して、4つの特定の「計算機（証明体系）」を紹介しています。

1. 基本的不明瞭論理（Basic Inquisitive Logic）: 質問を扱う標準的なチーム論理。
2. 命題的直観主義依存論理（Propositional Intuitionistic Dependence Logic）: 「AはBに依存する」といった「依存関係」を扱うチーム論理。
3. 2つの拡張版: これらは特別な「テンソル論理和（Tensor Disjunction）」（チームを二つの別々のグループに分割して、異なる事柄をチェックするという高度な方法）を追加したものです。

ツール：チームメンバーとしてのラベル

これらの計算を機能させるために、著者たちはラベルを使用しています。

• 想像してみてください。チームの全メンバーが名札をつけています。
• 一部の名札は個人（単独の人）のためのものです。
• 一部の名札はグループ（チーム全体）のためのものです。
• これらのルールを用いることで、「グループ $x$ はグループ $y$ と同一である」や「グループ $x$ はグループ $y$ の部分集合である」といったことが言えるようになります。

論文では、主に2種類の計算形式を提示しています。

1. 「詳細な」計算機 ($G(L)$)

このバージョンは非常に精密です。チームやその和集合（二つのチームの結合）、および共通部分（二つのチームの重なり）を表現できる複雑なラベルを使用します。

• 比喩: これは、渋滞の中にあるすべての車の正確な位置、そしてそれらがどのように合流したり車線を分かれたりするかを追跡する、高性能なGPSのようなものです。数学的に厳密であり、現実世界のチームの振る舞いを正確に反映しています。
• 難点: あらゆる詳細を追跡するため、GPSの計算がいつ終わるのか（計算が永遠に続いてしまうのではないか）を判断するのが困難です。

2. 「停止する」計算機 ($G^*(L)$)

「永遠に走り続ける」という問題を解決するために、著者たちは簡略化されたバージョンを作成しました。

• 比喩: 高性能なGPSの代わりに、このGPSは単にこう言います。「5台の車がリストにあります。では、これら5台のあらゆる組み合わせをチェックしましょう。」
• トリック: 彼らは、可能な「状態」（例えば、考えられる限られた天候条件）が有限であると仮定しています。可能性の数が限られているため、計算機は必ず一定時間内に停止することが保証されます。それは、証明を見つける（成功！）か、あるいはこれ以上適用できるルールがない壁に突き当たる（失敗／反例）かのどちらかです。
• 重要性: これにより、これらの論理において記述が真であるか偽であるかを判定するコンピュータプログラムを常に作成できることが保証されます。

ゲームの主要なルール

論文では、これらの計算が**健全（Sound）かつ完全（Complete）**であることを証明しています。

• 健全性: 計算機が「真」と言えば、それは実際に「真」です。（計算機は嘘をつきません。）
• 完全性: もし何かが実際に「真」であれば、計算機は最終的にその証明を見つけ出すことができます。（計算機は見落としません。）

また、彼らはこれらの計算が**許容ルール（admissible rules）**を持つことも証明しました。

• 弱化（Weakening）: リストに余計で無用な事実を追加しても、論理を壊すことはありません。
• 縮約（Contraction）: 同じ事実を二度リストした場合、それを一度だけリストされているものとして扱えます。
• カット（Cut）: AがBを導くと証明でき、かつBがCを導くなら、中間のステップを示さずに「AがCを導く」と直接飛ぶことができます。

「テンソル」の挑戦

この論文の最も困難な部分の一つは、テンソル論理和（Tensor Disjunction）（「分割」のルール）を扱うことでした。

• 比喩: 名探偵のチームを想像してください。
  • 標準的な論理はこう言います：「チーム全員が答えに同意すれば、チーム全体が事件を解決する。」
  • テンソル論理はこう言います：「チームを二つのグループに分割でき、グループAが事件の一部を解決し、グループBが残りの部分を解決できるならば、チームは事件を解決する。」
• 著者たちは、この分割の振る舞いを数学的にシミュレートするために、特別なルール（fin ルールと呼ばれるもの）を発明しなければなりませんでした。彼らは、可能な「世界（値付け）」の数が有限であると仮定することで、「すべてのチームは、これら特定の限定された世界の組み合わせである」と言うことができました。これにより、分割の振る舞いを数学的に扱うことが可能になったのです。

要約

要約すると、著者たちは、人々（チーム）の関わる論理パズルを解くための二種類のルールブックを構築しました。

1. 詳細で数学的に完璧なルールブック: 複雑なグループ間の相互作用を扱いますが、自動化が困難です。
2. 終了が保証された簡略化されたルールブック: 可能性の数が限られていることを前提としており、コンピュータが記述の真偽を自動的にチェックすることを可能にします。

彼らは、これらが研究対象とした特定の論理に対して、信頼できる（健全である）こと、およびあらゆる真理を網羅している（完全である）ことを証明しました。