Finite type arithmetic: computable existence analysed by modified realisability and functional interpretation
Klaus Frovin Jørgensen · 2001
of natural deduction an introduction to the Dialectica interpretation and compare the interpretation with modified realisability. We show how the interpretations represent two structurally different methods for unwinding computable information from proofs which may use certain prima facie non-constructive (ideal) elements of mathematics. Consequently, the two interpretations also represent different views on what is to be regarded as constructive relative to arithmetic. The differences show up in the interpretations of extensionality, Markov’s principle and restricted forms of independence-of-premise. We show that it is computationally a subtle issue to combine these ideal elements and prove that Markov’s principle is computationally incompatible with independence-of-premise for negated purely universal formulas. In the context of extracting computational content from proofs in typed classical arithmetic we also compare in an extensional context (i) the method provided by negative translation + Dialectica interpretation with (ii) the method provided by negative translation + A-translation + modified realisability. None of these methods can be applied fully to E-PA ω, since E-HA ω is not closed under Markov’s rule, whereas the method based on the Dialectica interpretation can be used if only weak extensionality is required.