直感主義のタイプ理論は、命題の表現を持っている。まず複合命題を考えてみよう。これは、領域 A の中で解釈される述語計算の（ヨX) と（Vx) に相応する。但し、タイプ理論が述語計算に比べてより形式的となっている点に違いがある。それは、タイプ理論が命題や判断（または主張）を明確にするためである。命題は、判断の一部ですが、その逆になることはない。ここで、A: prop は、 命題Aが適格な式であるという判断を意味している。a: Aは、A が真であるという判断である。つまり、a は A の証明になる。こうした判断は、 例えば、疑問文などに生じることがある。
演算子 ∑ と Π は、ドイツ語の文章を形式化する場合、述語計算の（ヨX) や（Vx) と同じ方法で使用される。つまり、直感主義タイプ理論の量化表現を含む命題をドイツ語の文章へシュガーリングする規則と原子的な命題のシュガ ーリングの規則により、派生できるようになる。
しかし、自然言語を処理するためにタイプ理論をさらに豊かにする必要がある。そのように定義すれば、一般化された関数のタイプ（x:α)ß の中で判断ができるようになる。判断は、変項に対するタイプ割り当ての中で行われる。そして、仮定の連鎖は、例えば、判断Jが文脈の中で実行される場合、変項は、自由に J の中に現れることになる。また、判断 J が文脈の中で行われ、定項が変項と置換 される場合、判断が文脈に依存することはない。
断片的なドイツ語の文法を記述する準備として、最後に演算子 ∑ と Π をさらに高いレベルで考察する。それは、これらの演算子がドイツ語の レキシコンに含まれるからである。∑ は、変数として集合と集合上で定義される命題関数を取り命題を返す。集合の統語表記は、∑(A，B) となる。また、演算子 pair を使用して ∑(A，B) の要素が形成される場合は、 要素 a: A と B(a) の証明が必要になる。次に要素 A と証明 B(p(c)) から c：∑(A，B) を生成する投射の演算子 p と q が導入される。これらの演算子は、規範的なものではない。Π は ∑ と同じタイプの演算子であるが、 範疇の割り当てから単形の規則を導くために、単形の λI 抽象化と ap 演算子が挿入される。
花村嘉英著（2005）「計算文学入門－Thomas Mannのイロニーはファジィ推論といえるのか？」より