We introduce a new typed combinatory calculus with a type constructor that, to each type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}, associates the star type σ∗\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma ^*$$\end{document} of the nonempty finite subsets of elements of type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}. We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this star combinatory (...) calculus, we define a functional interpretation of first-order predicate logic and prove a corresponding soundness theorem. It is seen that each theorem of classical first-order logic is connected with certain formulas which are tautological in character. As a corollary, we reprove Herbrand’s theorem on the extraction of terms from classically provable existential statements. (shrink)

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 formally proving an implication with an existential consequent or with a universal antecedent, the dialectica interpretation asks, under suitable conditions, for explicit 'interpreting' instances that make the implication valid. For proofs in constructive set theory CZF-, it may not always be possible to find just one such instance, but it must suffice to explicitly name a set (...) consisting of such interpreting instances. The aim of eliminating unbounded quantification in favor of appropriate constructive functionals will still be obtained, as our ∧-interpretation theorem for constructive set theory in all finite types CZFω- shows. By changing to a hybrid interpretation ∧q, we show closure of CZFω- under rules that – in stronger forms – have already been studied in the context of Heyting arithmetic. In a similar spirit, we briefly survey modified realizability of CZFω- and its hybrids. Central results of this paper have been proved by Burr 2000a and Schulte 2006, however, for different translations. We use a simplified interpretation that goes back to Diller and Nahm 1974. A novel element is a lemma on absorption of bounds which is essential for the smooth operation of our translation. (shrink)