Event Detail

Goedel’s Dialectica interpretation of Heyting arithmetic HA may be seen as expressing a lack of confidence in our understanding of unbounded quantification. Instead of inferring existential statements or inferring from universal statements, he looks, under suitable conditions, for the crucial instances that make the inferences valid. Due to the nesting of implications, this process calls for an interpreting theory T of functionals in all finite types.

We extend the concept of functional interpretation to Aczel’s constructive set theory CZF^- and its version in all finite types CZF^omega which we interpret in its bounded-quantifier fragment T_epsilon, a set-theoretic analog of Goedel’s T developed by Burr 2000. To this end, we adapt the Diller-Nahm interpretation of Heyting arithmetic in all finite types to the set-theoretic context, thus simplifying earlier versions developed by Burr 2000 and by Schulte 2007. Like these authors, we obtain CZF^omega as a conservative extension of T_epsilon and closure of CZF^omega under a Markov rule. A novel element is a lemma on the absorption of bounds in interpreted formulas which is basic for the smooth operation of our translation. We also study our version of Schulte’s Troelstra-style hybrid interpretation of CZF^omega which yields closure of CZF^omega under a weak rule of choice. We conjecture that this result cannot be improved to a strong rule of choice, contrary to what one might expect of a standard constructive theory.