Abstract

Treating propositions as types allows for a unified presentation of logic and type theory. Both fields thereby gain in expressive and deductive power. This chapter introduces the reader to a system of type theory where propositions are types. The system will be presented as an extension of the simple theory of types. Philosophical and historical observations are made along the way. A linguistic example is given at the end.