型理論
言語学の分野では自然言語の形式意味論の研究に用いられている。モンタギュー文法が代表的である。
最下層の型の個体要素間についての空でない二項関係 R で以下を満たすものが存在。 狭義の全順序(非反射的で推移的で、強連結 (∀x, y[''x ≠ y''↔[''xRy'' ∨ ''yRx'']])) で有り、極小元以外の任意の要素はそれより大きい要素を持つ(余定義域は定義域の部分領域で有る)。 注意無限性 は純粋に数学的な ST 固有の公理である。これは R が全順序関係であることを意味している。最下層の型に 0 を割り当てたとき、R の型は 3 となる。無限性 が成り立つのは R の議論領域が無限のときだけであり、結果として無限集合の存在を前提としている。関係を順序対で定義する場合、この公理の前に順序対を定義する必要が生じる。これは ST に Kuratowski の定義を導入することで実現する。ZFCのような他の集合論の無限集合の公理がなぜ ST で採用されなかったのかは書籍にも書かれていない。
ST は型理論が公理的集合論と似ていることを明らかにした。さらに、ZFC などの従来の集合論よりも単純な存在論に基づく "iterative conception of set" と呼ばれる ST のより精巧な存在論がもっと簡単な公理(公理型)を構成している。型理論の出発点は集合論だが、その公理、存在論、用語は異なる。型理論には他にも New Foundations や Scott-Potter set theory がある。