線形論理

線形論理（せんけいろんり、）は、「弱化(weakening)規則」と「縮約(contraction)規則」という構造規則を否定した部分構造論理の一種である。「資源としての仮説 (hypotheses as resources)」という解釈をする。すなわち、全ての仮説は証明において「一回だけ」消費される。古典論理や直観論理のような論理体系では、仮説（前提）は必要に応じて何度でも使える。例えば、"A" と "A" ⇒ "B" という命題から "A" ∧ "B" という結論を導出するのは、次のようになる。
これをシークエントで表すと、"A", "A" ⇒ "B" "A" ∧ "B" となる。上記の証明ではどちらの行でも、"A" が真であるという事実を「消費」している。この真理の「気軽さ」は形式手法では一般に必須である。
しかし、日常的な世界に関する文に適用するには、真理は抽象的すぎ、扱いにくい。例えば、約1リットルのクリームから約450グラムのバターができるとする。クリームをバターを作るのに使うとすると、クリームとバターの両方を持っているという結論は得られない。ところが上の論法でいけば cream, cream ⇒ butter cream ∧ butter となる（ここで、cream は「私は1リットルのクリームを持っている」という命題を表し、butter は「私は450グラムのバターを持っている」という命題を表す）。
このような活動を通常の論理でうまく表せないのは、クリームやバターなどの「資源」全般の性質によるものである。ある量の資源は、真理のように好きなように使ったり始末したりできず、全ての「状態変化」について注意深く見ていかなければならない。バター作りを正確に表すと、次のようになる。
線形論理ではこれを cream, cream butter butter と表記する。論理結合子（⇒ の代わりに ）と論理内含（ の代わりに ）の記号が異なる点に注意されたい。
線形論理は1987年、フランスの論理学者ジャン＝イヴ・ジラールが提唱した。
線形結合記号.
線形論理では、論理結合子が再検討される。各結合子は、乗法的 (multiplicative) なものと加法的 (additive) なものに分けられ、それぞれ同時 (simultaneous) 存在と択一 (alternative) 存在に対応する。結合子を解説するため、ここでは自動販売機を例として説明する。
実際の自動販売機は、これらの結合子の複雑な組み合わせで表され、それによって機械の全ての振る舞いを記述できる。
線形論理の変種.
線形論理には、様々な限定バージョンや変種が存在する。その1つは、古典/直観論理の軸に沿った変種である。古典線形論理 (CLL) は Girard が最初に提唱した線形論理である。CLL では、全ての結合子には双対が存在する。以下は、CLL をシークエント計算で表したものである。
証明は全てカット規則を使わない形に変換できる。
線形含意はこの表には出ていないが、線形否定と乗法的論理積を使えば、CLLでも "A" "B" ≡ "A"⊥ "B" と定義できる。これは古典論理ではお馴染みの形である。例えば、普通の含意 ⇒ は、"A" ⇒ "B" ≡ ?"A"⊥ "B" と定義できる。
このような定義はもちろん「線形否定」の記法を必要とするが、古典論理では双対を使うこともできる。"A" の双対は "A"⊥ と記述され、以下のように定義される。
論理単位元も同様の双対を持つ。例えば、⊥ = 0 であり、! と ? は双対である。双対の規則とは、ある項を一方の辺からもう一方に移す場合、その双対に変換される、というものである。
直観線形論理 (ILL) は、1つの帰結しか許容しない。CLL とは異なり、ILL の結合子には完全な双対性はない。実際、par () と why not (?) と命題定数「ボトム (⊥)」は、導入規則の帰結が複数必要となるため、ILL には存在しない。結果として、ILL では線形含意が基本的結合子となっている。
線形論理の他の変種には、特定の結合子を持つものと持たないものなどがあり、扱う論理の複雑さも様々である。以下は、最も一般的な変種である。
線形論理には一階のものと高階の拡張があるが、その考え方は標準的である。
ほかの部分構造論理.
線形論理に近い部分構造論理として、以下のものがある。