This article presents a parametrized functional interpretation. Depending on the choice of two parameters one obtains well-known functional interpretations such as Gödel's Dialectica interpretation, Diller-Nahm's variant of the Dialectica interpretation, Kohlenbach's monotone interpretations, Kreisel's modified realizability, and Stein's family of functional interpretations. A functional interpretation consists of a formula interpretation and a soundness proof. I show that all these interpretations differ only on two design choices: first, on the number of counterexamples for A which became witnesses for ¬A when defining (...) the formula interpretation and, second, the inductive information about the witnesses of A which is considered in the proof of soundness. Sufficient conditions on the parameters are also given which ensure the soundness of the resulting functional interpretation. The relation between the parametrized interpretation and the recent bounded functional interpretation is also discussed. (shrink)

We formulate Hilbert’s epsilon calculus in the context of expansion proofs. This leads to a simplified proof of the epsilon theorems by disposing of the need for prenexification, Skolemisation, and their respective inverse transformations. We observe that the natural notion of cut in the epsilon calculus is associative.

When Gödel developed his functional interpretation, also known as the Dialectica interpretation, his aim was to prove consistency of first order arithmetic by reducing it to a quantifier-free theory with finite types. Like other functional interpretations Gödel’s Dialectica interpretation gives rise to category theoretic constructions that serve both as new models for logic and semantics and as tools for analysing and understanding various aspects of the Dialectica interpretation itself. Gödel’s Dialectica interpretation gives rise to the Dialectica categories , in: Contemp. (...) Math., vol. 92, Amer. Math. Soc., Providence, RI, 1989, pp. 47–62] and J.M.E. Hyland in [J.M.E. Hyland, Proof theory in the abstract, Ann. Pure Appl. Logic 114 43–78, Commemorative Symposium Dedicated to Anne S. Troelstra ]). These categories are symmetric monoidal closed and have finite products and weak coproducts, but they are not Cartesian closed in general. We give an analysis of how to obtain weakly Cartesian closed and Cartesian closed Dialectica categories, and we also reflect on what the analysis might tell us about the Dialectica interpretation. (shrink)

I give an account of proof terms for derivations in a sequent calculus for classical propositional logic. The term for a derivation δ of a sequent Σ≻Δ encodes how the premises Σ and conclusions Δ are related in δ. This encoding is many–to–one in the sense that different derivations can have the same proof term, since different derivations may be different ways of representing the same underlying connection between premises and conclusions. However, not all proof terms for a sequent Σ≻Δ (...) are the same. There may be different ways to connect those premises and conclusions. -/- Proof terms can be simplified in a process corresponding to the elimination of cut inferences in sequent derivations. However, unlike cut elimination in the sequent calculus, each proof term has a unique normal form (from which all cuts have been eliminated) and it is straightforward to show that term reduction is strongly normalising—every reduction process terminates in that unique normal form. Further- more, proof terms are invariants for sequent derivations in a strong sense—two derivations δ1 and δ2 have the same proof term if and only if some permutation of derivation steps sends δ1 to δ2 (given a relatively natural class of permutations of derivations in the sequent calculus). Since not every derivation of a sequent can be permuted into every other derivation of that sequent, proof terms provide a non-trivial account of the identity of proofs, independent of the syntactic representation of those proofs. (shrink)