シナジーのメタファー１

　Die intuitionistische Logik wird in der Grammatik einer natürlichen Sprache kaum verwendet. Aber es handelt sich hier um die Formalisierung einer natürlichen Sprache in die mtuitionistische Logik, weil der intuitionistische Beweis so ähnlich dem Begrifl eines Computerprogramms ist. Ranta nimmt eine Grammatik eines englischen Fragments an, die ähnlich der Struktur von PTQ ist. Zuerst betrachtet Ranta die Quantoren und Anaphern, und dann diskutiert zusätzlich die Dynamischheit eines Textes.
　Ranta stellt auf Matin-Lör hin die intuitionistische Typentheorie vor. Die intuitionistische Typentheorie hat die Ausdrücke für Propositionen.

(22) (�肺: A) B and (Πx: A) B.

　Die Ausdrücke entsprechen (∃x) und (∀x) in der Prädikatenrechnung，die im Bereich A interpretiert wird. Der Unterschied besteht darin, daß die Typentheorie einen Bereich und/oder einen Urteil (oder eine Behauptung) explizit macht. Die Typentheorie ist noch formaler als die Prädikatenrechnung. Der Bereich kann nur von der Interpretation verstanden werden. Der Urteil ist noch breiter in einem Skopus als die Proposition, die als ein Teil eines Urteils angesehen werden mag.

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