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. (shrink)

Pure Type Systems, PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic. First we consider (...) a simplification of the start and weakening rules of PTSs, which allows contexts to be sets of statements, and a generalisation of the conversion rule. The resulting Set-modified PTSs or SPTSs, though essentially equivalent to PTSs, are closer to standard logical systems. A simplification of the abstraction rule results in Abstraction-modified PTSs or APTSs. These turn out to be equivalent to standard PTSs if and only if a condition (*) holds. Finally we consider SAPTSs which have both modifications. (shrink)