【自著紹介】根拠づけの論理の論文を書きました

2026-03-04 投稿

私の書いた "Simple Sequent Calculus for Weak Full Grounding" という論文が先日、Journal of Logic, Language, and Information に受理されました。著者最終稿は PhilArchive にアップロードしてあります。以下では、この論文の概要を解説します。

背景

この論文は、根拠づけ (grounding) の論理にかかわるものです。AがBを根拠づけるというのは、Bがなぜ成り立つのかの理由をAが与えるということです。例えば、p&qという連言は、その連言肢であるpとqに根拠づけられると言えます。というのも、p&qが成り立つ理由は、pとqが両方とも成り立つことに求められるからです。

根拠づけの論理の分野においては、Fine 2012 等で打ち出された二つの区別に依拠して議論するのが標準となっています。それは、完全な (full) 根拠づけ／部分的な (partial) 根拠づけの区別と、厳密な (strict) 根拠づけ／弱い (weak) 根拠づけの区別です。

今回書いた論文は、専ら弱く完全な根拠づけの論理に焦点を絞ったものです。

弱く完全な根拠づけの論理体系としては色々なものがすでにありますが、今回の論文では、Lovett 2020 で提示された論理体系 LWG というものに着目しています。

メインの結果

LWG が、次のような sequent スタイルの証明体系 \(\mathcal{G}_\mathbf{LWG}\) と同等であることを示しました。(Theorem 5.6)

$$ \scriptsize \begin{array}{|rlrl|} \hline \mathbf{Initial\ Sequents} & & \\ (\text{Initial}^+) & \Gamma, p \Rightarrow p, \Delta \quad \text{where } \sigma(\Gamma, p) \subseteq \sigma(p, \Delta) & \\ (\text{Initial}^-) & \Gamma, \lnot p \Rightarrow \lnot p, \Delta \quad \text{where } \sigma(\Gamma, \lnot p) \subseteq \sigma(\lnot p, \Delta) & \\[1.5ex] \mathbf{Logical\ Rules} & & \\ (\land \text{L}) & \dfrac{\Gamma, A, B \Rightarrow \Delta}{\Gamma, A \land B \Rightarrow \Delta} & (\land \text{R}) & \dfrac{\Gamma \Rightarrow A, \Delta \quad \Gamma \Rightarrow B, \Delta}{\Gamma \Rightarrow A \land B, \Delta} \\[4ex] (\lor \text{L}) & \dfrac{\Gamma, A \Rightarrow \Delta \quad \Gamma, B \Rightarrow \Delta}{\Gamma, A \lor B \Rightarrow \Delta} & (\lor \text{R}) & \dfrac{\Gamma \Rightarrow A, B, \Delta}{\Gamma \Rightarrow A \lor B, \Delta} \\[4ex] (\lnot\land \text{L}) & \dfrac{\Gamma, \lnot A, \lnot B \Rightarrow \Delta}{\Gamma, \lnot(A \land B) \Rightarrow \Delta} & (\lnot\land \text{R}) & \dfrac{\Gamma \Rightarrow \lnot A, \lnot B, \Delta}{\Gamma \Rightarrow \lnot(A \land B), \Delta} \\[4ex] (\lnot\lor \text{L}) & \dfrac{\Gamma, \lnot A, \lnot B \Rightarrow \Delta}{\Gamma, \lnot(A \lor B) \Rightarrow \Delta} & (\lnot\lor \text{R}) & \dfrac{\Gamma \Rightarrow \lnot A, \Delta \quad \Gamma \Rightarrow \lnot B, \Delta}{\Gamma \Rightarrow \lnot(A \lor B), \Delta} \\[4ex] (\lnot\lnot \text{L}) & \dfrac{\Gamma, A \Rightarrow \Delta}{\Gamma, \lnot\lnot A \Rightarrow \Delta} & (\lnot\lnot \text{R}) & \dfrac{\Gamma \Rightarrow A, \Delta}{\Gamma \Rightarrow \lnot\lnot A, \Delta} \\[2ex] \mathbf{Structural\ Rules} & & \\ (\text{Contraction L}) & \dfrac{\Gamma, A, A \Rightarrow \Delta}{\Gamma, A \Rightarrow \Delta} & (\text{Contraction R}) & \dfrac{\Gamma \Rightarrow A, A, \Delta}{\Gamma \Rightarrow A, \Delta} \\[3ex] \hline \end{array} $$

ただし、Initial Sequent のところに出てくる \(\sigma\) という関数は大体次のように定義されます。（より正確な定義は論文の第 3.1 節を参照してください。）

$$ \sigma(A) := \{ p \mid p \text{ は } A \text{ にポジティブに現れる } \} \cup \{ \lnot p \mid p \text{ は } A \text{ にネガティブに現れる } \}. $$

\(\mathcal{G}_\mathbf{LWG}\) は次の基本的な特徴を持ちます。

さらに、\(\mathcal{G}_\mathbf{LWG}\) は他の sequent 計算の体系と次のような関係にあります。