シナジーのメタファー１

　ここでは、直感主義論理に基づいた簡単なドイツ語の文法を導入する。直感主義は、論理の系統の中で様相論理などと共に多値論理のグループに属し、やはり量化の表現に真理値を割り当てる上で古典的な二値論理では不十分であるという立場を取る。また、直感主義を用いた自然言語に関する証明は、コンピュータのプログラムにも通じる方法であり、Ranta (1991)は、MontagueのPTQを土台にした英語の断片を提示している。ここで導入するドイツ語の文法は、レキシコン、範疇文法そしてシュガーリングを構成要素にする。
　まず前提として、テキストのダイナミズムを直接反映するために、Ranta (1991)は、Matin-Löf (1982)のタイプ理論を取り入れた。Matin-Löfの動機は、統語論と意味論を数学によって明確にするという立場から、 直感主義の数学とプログラミング間をつなぐために（例えば、argument とinput、valueとoutput、x=eとx:=e、関数の合成とS1；S2、条件の定義とif B then S1 else S2、回帰の定義とwhile B do Sなど)、直感主義のタイプ理論を考案した。（Matin-Löf 1982)
　直感主義のタイプ理論は、命題の表現を持っている。まず複合命題を考えてみよう。（66)は、領域Aの中で解釈される述語計算の（ヨx)と（∀x) に相応する。但し、タイプ理論が述語計算に比べてより形式的になっている点に違いがある。それは、タイプ理論が、命題や判断（または主張）を明確にするためである。命題は、判断の一部であるが、その逆となる ことはない。ここでは、A: propは、命題Aが適格な式であるという判断を意味している。a: Aは、Aが真であるという判断である。つまり、aはAの証明になる。こうした判断は、 例えば、疑問文などに生じることがある。
　演算子�狽ﾆ∏は、ドイツ語の文章を形式化する場合、述語計算の（ヨx) や（∀x)と同じ方法で使用される。つまり、直感主義タイプの理論の量化表現を含む命題をドイツ語の文章へシュガーリングする規則と原子的な命題のシュガーリングの規則により、Ein Mann keucht. が派生することになる。
　しかし、自然言語を処理するためにタイプ理論をさらに豊かにする必要がある。一般化された関数のタイプ（x:α）ßの中で判断ができるようにした。判断は、変項に対するタイプ割り当ての中で行われる。そして、仮定の連鎖は、文脈（x1: α1,…, xn:αn )になる。例えば、判断Jが文脈の中で実行される場合、変項x1,…, xnは、自由にJの中に現れることになる。また、判断Jが文脈の中で行われ、定項も（a1: α1,…,an:αn（a1,…, an-1/x1,…, xn-1)が変項x1,…, xnと置換される場合、判断が文脈に依存することはない。　

花村嘉英（2005）「計算文学入門−Thomas Mannのイロニーはファジィ推論といえるのか？」より