Abstract

The calculus of constructions is formulated as a natural deduction system in which deductions follow the constructions of the terms to which types are assigned. Strong normalization is proved for deductions. This strong normalization result implies the consistency of the underlying system, but it is still possible to make contradictory assumptions. A number of assumption sets useful in implementations are proved consistent, including certain sets of assumptions whose types are negations, negations of certain equations, arithmetic, classical logic, classical arithmetic, and the existence of power sets. All results are given with complete proofs