Abstract

Martin-Löf's constructive theory introduces, beside proof processes—the brouwerian mental construction—proof objects that could become the subject matter of a new kind of proof theory. In contradistinction to the classical approach, the proposition can then be defined as the set of its proofs. The lower level type theory is therefore a set theory, where the operators Σ and Π generalize the Cartesian product and the functional space to families of sets. To obtain the familiar logical constants, we have only to choose the logical reading of a : A. Σ and Π become ∃ and ∀, or, if there is no functional dependency, & and ⊃.