Logic & Philosophy of Science Colloquium


Justus Diller
Universität Münster, Germany

"Functional Interpretations of Constructive Set Theory in All Finite Types"


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.

Friday, February 16, 2007
SST 318
3 pm

Refreshments will be served