線形論理

線形論理（せんけいろんり、英: Linear logic）は、「弱化(weakening)規則」と「縮約(contraction)規則」というを否定した部分構造論理の一種である。「資源としての仮説 (hypotheses as resources)」という解釈をする。すなわち、全ての仮説は証明において「一回だけ」消費される。古典論理や直観論理のような論理体系では、仮説（前提）は必要に応じて何度でも使える。例えば、A と A ⇒ B という命題から A ∧ B という結論を導出するのは、次のようになる。 1. * A と A ⇒ B を前提とするモーダスポネンス（あるいは自然演繹でいう含意の除去）により、B が得られる。 2. * 前提 A と (1) の論理積から A ∧ B が得られる。 これをシークエントで表すと、A, A ⇒ B ⊢ A ∧ B となる。上記の証明ではどちらの行でも、A が真であるという事実を「消費」している。この真理の「気軽さ」は形式手法では一般に必須である。 しかし、日常的な世界に関する文に適用するには、真理は抽象的すぎ、扱いにくい。例えば、約1リットルのクリームから約450グラムのバターができるとする。クリームをバターを作るのに使うとすると、クリームとバターの両方を持っているという結論は得られない。ところが上の論法でいけば cream, cream ⇒ butter ⊢ cream ∧ butter となる（ここで、cream は「私は1リットルのクリームを持っている」という命題を表し、butter は「私は450グラムのバターを持っている」という命題を表す）。 このような活動を通常の論理でうまく表せないのは、クリームやバターなどの「資源」全般の性質によるものである。ある量の資源は、真理のように好きなように使ったり始末したりできず、全ての「状態変化」について注意深く見ていかなければならない。バター作りを正確に表すと、次のようになる。 1リットルのクリームがあり、1リットルのクリームを450グラムのバターに変換するプロセスを経ると、450グラムのバターが得られる。 線形論理ではこれを cream, cream ⊸ butter ⊩ butter と表記する。論理結合子（⇒ の代わりに ⊸）と論理内含（⊢ の代わりに ⊩）の記号が異なる点に注意されたい。 線形論理は1987年、フランスの論理学者ジャン＝イヴ・ジラールが提唱した。