Logical problems of functional interpretations Original Research Article

Gödel interpreted Heyting arithmetic View the MathML source in a “logic-free” fragment View the MathML source of his theory View the MathML source of primitive recursive functionals of finite types by his famous Dialectica-translation D. This works because the logic of View the MathML source is extremely simple. If the logic of the interpreted system is different—in particular more complicated—, it forces us to look for different and more complicated functional translations. We discuss the arising logical problems for arithmetical and set theoretical systems from View the MathML source to View the MathML source. We want to test the thesis: While the functionals take care of the proof theoretic strength of the interpreted system, it is the functional translation that has to cope with the logical complexities of the system.