A diagrammatic proof-theoretic semantics for the Greimas semiotic square

技術的概要：グレマス記号論的正方形のための図式的証明論的意味論

問題提起
本論文は、アルジルド・ジュリアン・グレマスによって開発された構造記号論的方法、特に記号論的正方形に関する形式的仕様の欠如を扱っている。記号論的正方形は、物語構造や意味化を分析するための広く用いられるヒューリスティックなツールであるが、「同型化（構造的アナロジー）」を確立し、メタ項（複合項、中立項、指示項）を構築するための操作手順は未だ十分に規定されていない。従来の定式化は、非公式な組み合わせ操作（「+」と表記）と二項対立に依存しており、それらの論理的地位（例えば、対立と矛盾の区別）についてしばしば曖昧である。さらに、この文脈における否定の標準的な解釈は、しばしばブール補完と混同され、構造記号論における対立の关系的かつ非網羅的な性質を捉え損なっている。本論文は、記号論的正方形の背後にある生成過程を形式化するために、これらの操作の厳密な証明論的再構成を提供することを目的としている。

方法論
著者らは、単一スパイダー図（Howse et al., 2005）に基づく図式的証明系を開発し、集合論的拡張ではなく意味構成を表すためにこの形式を適応させた。

1. 形式の適応：

   • 輪郭は、セム（意味の基本単位）またはセメムを表す。
   • スパイダー（実存ドット）は、セムの実在化（決定的存在）または仮想化（未決定的存在）を符号化する。複数の領域にまたがるスパイダーは仮想化された状態（意味的未決定性）を表し、単一の領域に限定されたスパイダーは決定された実在化を表す。
   • 領域は、宇宙 $X$ 内の意味領域を表し、メタ項（$M$）の部分集合と特定のセムクラス（$S_1, S_2$）を含む。

2. 中核的関係の定義：
   本論文は、記号論的正方形の基本的な関係を、推論規則によって支配される図式的変換として再定義する：

   • 図式的対立（$\#_{diag}$）：$S_1$ と $S_2$ が互いに排他的（ disjoint な領域）であるが、独立して実在化されている、2 つの図式間の静的関係として定義される。
   • 図式的否定（$\neg_{diag}$）：ブール否定（グローバルな補完を生み出す）とは異なり、これはスパイダーの生息域を対立項と意味宇宙の外側へと拡張し、意味的未決定性を導入する変換として定義される。これは「制限され、領域によって決定された意味的対位」である。
   • 図式的含意（$\Rightarrow_{diag}$）：否定の逆として定義され、スパイダーの生息域が一連の領域から単一の領域へと制限（洗練）され、未決定性が決定された実在化へと解決される。

3. 推論系（$R$）：
   これらの変換は、スパイダー図計算から適応された規則を用いた形式系における導出として実現される。これには以下が含まれる：

   • AddFeet, SplitSpider, Combine, EraseSpider, CopySpider, ConjunctionElimination, および Idempotency。
   • これらの規則により、ある意味構成から別のものへの移行を立証する証明木を構築することが可能となる。

主要な貢献と結果

1. メタ項構築の形式化：
   本論文は、グレマス正方形の 4 つの標準的なメタ項（複合項 $S$、中立項 $\bar{S}$、正の指示、負の指示）が、基本構成の対合的ペアから均一な導出スキーマを通じて導出可能であることを証明する。

   • 操作「+」は、論理的または集合論的な和としてではなく、導出的リフトとして再解釈される。
   • 2 つの図式のペア $(d_a, d_b)$ が与えられたとき、系は Combine, AddFeet, SplitSpider などの規則の系列を適用し、メタレベル領域 $M$ 内の新しいスパイダー（立証者）を含む新しい図式 $d^+_{ab}$ を構築する。
   • この新しい立証者は、入力セムの構造的な非互換性を崩すことなく、それらの結合表現を仲介する。

2. 非ブール否定：
   この系は、この枠組みにおける図式的否定がブール補完ではないことを形式的に示す。否定された項 $\neg_{diag}(S_i)$ の生息域は、セム対立およびメタレベル領域に対して許容される領域に制限され、標準的な集合論的補完に含まれるはずの領域は除外される。これは、否定が網羅的な排除ではなく、仮想化された状態を生成する「対立の关系的性格」を捉えるものである。

3. 証明論的立証：
   本論文は、以下のものに対する立証者として機能する明示的な証明木（$T_1$ から $T_8$ など）を構築する：

   • 実在化されたセムからそれらの否定への移行（例：$/life/ \to /not-life/$）。
   • 含意を通じて否定から実在化された項への戻り（例：$/not-life/ \to /death/$）。
   • 構成セムペアからの 4 つのメタ項全体の構築。

4. 非標準的項への拡張：
   推論系は二項合成に対して閉じていることが示され、標準的な解釈では通常除外されるが、この図式的枠組み内では well-defined な意味対象である非標準的メタ項（例、「正のスキーマ」$s_1 + \neg s_1$ および「負のスキーマ」$s_2 + \neg s_2$）の導出が可能である。

意義と主張
本論文は、グレマス記号論的正方形に対する構成的で規則ベースの意味論を提供すると主張する。その主な意義は以下の点にある：

• 暗黙の手続きの明示化：従来の記号論においてしばしばヒューリスティックであった用語の「組み合わせ」と「同型化」手続きを、明示的な形式的導出へと変換する。
• 「+」演算子の再解釈：メタ項形成を、静的な論理的結合ではなく、構築的プロセス（導出的リフト）として証明論的に記述する。
• 推論設定の統合：図式的推論が、非古典的な意味操作（特に非ブール否定と関係的対立）を統合された推論設定内でいかに形式化できるかを示す。
• スパイダー図の拡張：この研究は、スパイダー図計算の表現範囲を、集合論的および実存的推論を超えて、複雑な構造的意味操作をモデル化するように拡張する。

著者らは、この枠組みにより、記号論的正方形は単なる分析ツールではなく、変換が形式的な図式的推論を通じて明示化される生成意味システムとして捉えられ得ると結論付けている。