シナジーのメタファー１

　Die einfache Typentheorie ist überhaupt nicht genug für die formale Sprache. Um sie vollständig zu formalisieren, ist die reichere Typentheorie gebraucht. Wollen wir die folgenden Urteile betrachten.

(31)
Urteil α： type, α=ß: type, a: α, a=b: α 　
Welche Voraussetzungen -, α:type, ß: type. α： type, α: type, a: α, b: α 　　　　　　　　　　
bedeutet daß　α ist eine Type, α und ß sind gleiche Typen, a ist ein Objekt von α, a und b sind gleiche Objekte von a.

　Alle Urteile können unter Hypothesen (x: α) gemacht werden, die den Variablen die Typen zuweisen. Ein Kontext ist eine Folge der Hypothesen, deren Form x1:α,...,xn:α ist. Wenn ein Urteil J im Kontext gemacht wird, mögen Variable x1,...,xn in J frei erscheinen. Wenn ein Urteil J im Kontext gemacht wird und Konstanten a1: α1,...,an:αn (a1,...,an-1/x1,...,xn-1) durch Variablen x1,...,xn in J substituiert werden, ist ein Urteil unabhängig vom Kontext.
　Wollen wir weiter �� und Π auf dem höheren Niveau betrachten. Die Type "prop" einer Proposition wird eingeführt (prop: type und prop = set: type). �� ist ein Operator, der als das Argument eine Menge und eine propositionale Funktion nimmt, die auf der Menge definiert wird und eine Proposition herausbringt.

(32) ��: (X:set)((X) prop) prop.

Die Syntax des höheren Niveaus ist ��(A, B), wo A:set und B:(A) prop eingesetzt werden. Wenn ein Element von ��(A, B) durch das Operator "pair" geformt wird, sind ein Element a: A und ein Beweis von B(a) gebraucht.

(33) pair: (X:set)(Y: (X)prop)(x:X)(Y(x))��(X,Y).

　Die Projektionen (p und q), die ein Element von A und einen Beweis von B(p(c)) durch einen Beweis c:��(A, B) erzeugen, werden in (34) eingeführt. Allerdings sind sie nicht kanonisch.

(34)
p: (X:set)(Y: (X) prop)(z:��(X,Y))X;
q: (X:set)(Y: (X) prop)(z:��(X,Y))Y(p(X,Y,z)).

　Π ist die gleiche Type wie ��. Aber die monomorphische λ-Abstraktion und das ap-Operator werden eingeführt, um die monomorphische Regelungen aus der Zuweisung der Kategorien abzuleiten. Die Regelungen entsprechen den polymorphischen Typentheorien, die Matin-Löf darstellte. Diese Operatoren wie ��, Π, pair, λ, p, q und ap werden im Lexikon der deutschen Grammatik enthalten.

(35)
Π: (X:set)((X) prop) prop;
λ: (X:set)(Y: (X) prop)((x:X)Y) Π(X:Y);
ap: (X:set)(Y: (X)prop)(Π(X:Y))(x:X) Y(x).

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