Abstract:
Gödel'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
ω which we interpret in its bounded
quantifier fragment T
∈, a set theoretic analog of
Gödel'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
ω as a
conservative extension of T
∈ and closure of CZF
ω
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
ω which
yields
closure of CZF
ω 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.