On the proof theory of Coquand's calculus of constructions (Q5961667)

The calculus of constructions of Coquand is formulated as a natural deduction system in which deductions follow the constructions of the terms to which types are assigned. Coquand proved the normalization theorem and later the strong normalization theorem for deductions. The 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.