# Contents

## Idea

Originally, “simple type theory” was the name of the type theory introduced by Church (1940) (therefore often and more informatively: “Church’s type theory” or similar). This type theory allowed (only) function type-type formation (therefore often: “simply typed lambda-calculus”) based on two elementary types (a kind of type of natural numbers and a type of propositions).

In mild generalization, if one admits in addition product type-type formation then [e.g. Gunter (1992)] these are the type theories whose categorical semantics is in cartesian closed categories (see also at relation between category theory and type theory).

More generally, the term “simple type theory” has come to refer to any type theory whose type formations are not indexed, in that the judgment that a type $A$ is well-formed has no other inputs, understood in contrast to:

## References

Original articles:

• Bertrand Russell, Mathematical Logic as Based on the Theory of Types, American Journal of Mathematics, Vol. 30, No. 3 (Jul., 1908), pp. 222-262

• Alonzo Church, §5 of: A Formulation of the Simple Theory of Types, The Journal of Symbolic Logic 5 2 (1940) 56-68 [doi:10.2307/2266170]