Predicative Functionals and an Interpretation of ID^_
In 1958 Gödel published his Dialectica interpretation, which reduces classical arithmetic to a quantifier-free theory T axiomatizing the primitive recursive functionals of finite type.
In 1958 Gödel published his Dialectica interpretation, which reduces classical arithmetic to a quantifier-free theory T axiomatizing the primitive recursive functionals of finite type.