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.
花村嘉英（2005）「計算文学入門－Thomas Mannのイロニーはファジィ推論といえるのか？」より