Characterizing the interpretation of set theory in Martin-Löf type theory (Q2500469)

The paper contributes to the investigation of the relationship between two different formal frameworks relevant to the foundations of constructive mathematics: Martin-Löf's type theory and constructive Zermelo-Fraenkel set theory CZF. Since Aczel's work in the seventies, it is known that CZF has an interpretation in a suitable version of type theory, ML\(_1\)V, using the so-called (Curry-Howard) propositions-as-types interpretation. The same holds also for an extension CZF+REA of constructive set theory, where REA is the so-called regular extension axiom, essentially granting the existence of higher tree classes. In this case the type theory involved is an extension of ML\(_1\)V, known as ML\(_{1W}\)V. On the other hand, the type-theoretic interpretation validates more than what is provable by CZF, whence the natural problem arises: to characterize exactly the set-theoretic theorems which are valid under the type-theoretic interpretation in ML\(_1\)V. The authors solve the problem for a large class of statements, which are supposed to cover all mathematically relevant propositions (the mathematical formulas, roughly corresponding to sets in the classical cumulative hierarchy up to \(\omega+\omega\), and the generalized ones, corresponding to sets of ranks below \(\aleph_\omega\)). As to the contents of the paper, \S 2 gives the necessary details and preliminary notions which are needed to specify suitable choice principles compatible with Martin-Löf's type theory, i.e. \(\Pi\Sigma\)-AC, \(\Pi\Sigma W\)-AC. In \S 3--\S 4 the so-called formulae-as-classes interpretation is presented. First, bounded formulas which correspond to small types are interpreted as sets. Using the appropriate choice principles, it is shown how to simulate the type-theoretic interpretation of CZF in CZF itself and how to prove (Theorems 3.14--3.15) the equivalence between the type-theoretic interpretation (rephrased in CZF) and its set-theoretic counterpart (roughly, this is obtained by defining a constructive version of the cumulative hierarchy). The interpretation is extended by assigning to arbitrary formulas \(\varphi\) suitable proper classes which, roughly, contain the proofs of the given \(\varphi\). In order to implement this idea, the authors need an applicative structure, and in fact a partial combinatory algebra, which makes the required set-theoretic analogues of the type-theoretic constructors computable (e.g., the notion of set exponentiation computable). It turns out (Theorems 4.13--4.14) that the theorems of CZF+\(\Pi\Sigma\)-AC and CZF+REA+\(\Pi\Sigma W\)-AC are validated by the interpretation (provably in CZF, CZF+REA, respectively). In \S 5 it is shown that, for a suitable collection of statements (mathematical, generalized mathematical), inhabitedness of the corresponding formulae-as-classes interpretation implies truth (see Theorems 5.1--5.2, 5.9--5.10, 5.16, Corollary 5.20). Theorem 5.23 establishes a conservative extension result for the same classes of formulas with respect to a number of additional principles. \S 6 outlines an interpretation of type theory in set theory. The construction is rather entangled, due to the complex syntax of type theory; again, the applicative structure of \S 3 is used in that terms of type theory are translated into corresponding application terms. The interpretation is sound according to Theorems 6.8--6.9. In \S 7 the main theorem, 7.6, is proven by combining the results of the previous section: (i) the mathematical theorems of CZF plus the \(\Pi\Sigma\)-axiom of choice are exactly those validated in ML\(_{1}\)V; (ii) the generalized mathematical theorems of CZF+REA plus the \(\Pi\Sigma W\)-axiom of choice are exactly those validated in ML\(_{1W}\)V. \S 8 deals with the standard question whether the systems involved satisfy the disjunction property DP and the existence property EP. Though it is not known yet if CZF satisfies EP, theorems 8.3--8.4 establish EP and DP for CZF+\(\Pi\Sigma\)-AC (CZF+ REA+ \(\Pi\Sigma W\)-AC, respectively) at least for (generalized) mathematical sentences and in presence of relativized dependent choice. The paper applies several technical methods of interest for constructive mathematics. Conceptually, it further justifies the following practice: one is free to carry out standard (constructive) set-theoretic mathematics in CZF or CZF+REA, since the constructive content is exactly granted by the corresponding type theory, according to the theorems above.