線形論理は、みなさんに馴染みの深い（？）直観主義論理や古典論理と並ぶ論理体系の 一種で、ちょっと変わった「含意（ならば）」や「連言（かつ）」が登場します。 なぜそんなものがいるのかを理解するために次の命題を考えましょう。
命題Ａ：「私は１１０円持っている」
命題Ｂ：「私はコーラを買える」
命題Ｃ：「私はチョコレートを買える」
今、コーラもチョコレートも１１０円だとしましょう。すると、 １１０円持ってればコーラもチョコレートも買えますから 「ＡならばＢ」かつ「ＡならばＣ」であると言えます。 ということは、普通の論理だと、「Ａならば”ＢかつＣ”」がいえますから、 「１１０円持っていれば、コーラも買え、かつ、チョコレートも買える」ということになります。 これは正しいでしょうか？Ｘ君とＹ君は次のように言い争いになりました。
Ｘ：「１１０円持ってれば、コーラもチョコレートもどちらでも好きな方を買える。だから どっちも買えるというのは正しい。」
Ｙ：「１１０円持ってても、コーラを買えばお金はなくなっちゃうからチョコレートは買えなくなる。だからどっちも買えるというのは間違いだ。」
この言い争いの原因は何でしょうか？ それはＸ君とＹ君は「かつ」を別の意味で解釈しているからです。 つまり、「ＡかつＢ」を、Ｘ君は「ＡもＢも（同時になりたつとはかぎらないけど） どちらも好きな方を成立させることができる」と解釈し、Ｙ君は「ＡもＢも同時に成り立つ」 と解釈しているわけです。ところが通常の論理では「かつ」に相当する論理記号は 一つだけですから、上のような混乱が生じたわけです。 そこで、線形論理では、Ｘ君にような解釈とＹ君のような解釈を別々の連言で表します （ここでは前者を＆で表し、後者をΛで表すことにします）。 さらに、「１１０円持っていれば○○が買える」では、○○を買ってしまったら 「１１０円持っている」という事実はなくなってしまうわけですから、 「ならば」の意味も通常の論理の含意とは異なることがわかります。そこで、含意についても 違う記号を用意して、-o で表すことにします。
さて、以上のように新しい論理記号を用いると、何が成立するかを次のように 正確に表現できます。
Ａ-o Ｂ：「１１０円持ってれば、コーラを買える。ただしコーラを買ってしまったら １１０円はもうなくなってしまう。」
Ａ-o Ｃ：「１１０円持ってれば、チョコレートを買える。ただしチョコレートを買ってしまったら１１０円はもうなくなってしまう。」
ではもう一度、Ｘ君とＹ君の主張を確認してみましょう。Ｘ君は、 「Ａならば"ＢかつＣ"」を「Ａ-o（Ｂ＆Ｃ）」のことだと解釈していたわけです。 だからその意味では、Ｘ君の主張は正しかったわけです。 一方、Ｙ君は、「Ａならば"ＢかつＣ"」を「Ａ-o（ＢΛＣ）」、すなわち 「Ａが成り立っていればＢもＣも同時に成立する」と解釈していたわけです。 だからそれが誤りだというＹ君の主張も正しかったわけです。
以上が線形論理の簡単な動機づけです。線形論理には上で導入した以外にも いろいろな論理記号が登場します。勘のいい人にはすでに察子がついたと 思いますが、「選言（または）」も２つの論理記号にわかれます。 また、通常は、Ａ-oＢとＡからＢを導くと、Ａは成立しなくなってしまいますから、 「いつでも成立する」命題を表現するために、「！Ａ」というような論理式も導入します （！がついていれば、何回でも使えるわけです）。
この十年、上のような線形論理のコンピュータサイエンスへの応用が注目を集め、 さまざまな角度から研究がされてきました。我々の研究室でも、その一つとして、 並行・分散プログラミング言語と線形論理との関係について研究をすすめてきました。 いったいどんな関係があるんだ？と興味のある人は課題3 を選んでみましょう。