タイプ理論タイプりろん

ラッセルのパラドクス回避のために『プリンキピア・マテマティカ』で導入された、命題関数の引数に階層を設ける枠組みをいう。自己言及的な構成を禁じる「悪循環原理」を核に分岐型理論として提示され、のちラムゼイらにより単純型理論として整理された。