Simple Type Theory

• Typed variables: no $x\in x$

• Avoids paradoxes by hierarchy.

• Each variable has a fixed type.

• Used in early set-theoretic foundations.