On the herbrandised interpretation for nonstandard arithmetic

Abstract

Functional interpretations are useful tools of proof theory. After Godel described his dialectica interpretation for Heyting arithmetic in 1941, many other interpretations have been proposed, each focusing on different goals. We start with an overview of the interpretations of Godel and Shoenfield. We propose a functional interpretation for nonstandard Heyting arithmetic based on previous work by Van den Berg, Briseid and Safarik. This interpretation enables the transformation of proofs in nonstandard arithmetic of internal statements into proofs in standard arithmetic of those same statements. The witnesses for external, existential statements of the interpreting formulas are functions whose output is a finite sequence. Syntactically, the terms representing these functions are called end-star terms. It is possible to define a preorder of end-star terms. Our interpretation is monotone over this preorder: if a certain end-star term is a witness for an existential statement, then any "bigger" term also is. Using this property, we are able to prove a soundness theorem for our interpretation, which eliminates principles recognisable from nonstandard analysis. From this theorem, we get as corollary the conservativity of nonstandard arithmetic over standard arithmetic, as well as a term extraction theorem. It is also possible to prove a characterization theorem for our interpretation. As corollary, we show that the countable saturation principle does not add proof theoretical strength to our intuitionistic nonstandard system. Finally, we give a short description of Weihrauch reducibility and comment on an application of Godel’s dialectica interpretation to, in certain circumstances, prove that a ∀∃-formula Weihrauch reduces to another one.

Keywords

Functional interpretations, nonstandard arithmetic, Weihrauch reducibility

Citation

de Almeida Borges, A. (2016). On the herbrandised interpretation for nonstandard arithmetic (Master's thesis). Instituto Superior Técnico, Universidade de Lisboa.

@MastersThesis{AlmeidaBorges2016_MS,
  author = "{de Almeida Borges}, Ana",
  title = "On the herbrandised interpretation for nonstandard arithmetic",
  school = "{I}nstituto {S}uperior {T}écnico, {U}niversidade de {L}isboa",
  year = "2016",
  url = "https://fenix.tecnico.ulisboa.pt/cursos/mma/dissertacao/1691203502342670",
  keywords = "Functional interpretations, nonstandard arithmetic, Weihrauch reducibility",
  abstract = {Functional interpretations are useful tools of proof theory. After Godel described his dialectica interpretation for Heyting arithmetic in 1941, many other interpretations have been proposed, each focusing on different goals. We start with an overview of the interpretations of Godel and Shoenfield. We propose a functional interpretation for nonstandard Heyting arithmetic based on previous work by Van den Berg, Briseid and Safarik. This interpretation enables the transformation of proofs in nonstandard arithmetic of internal statements into proofs in standard arithmetic of those same statements. The witnesses for external, existential statements of the interpreting formulas are functions whose output is a finite sequence. Syntactically, the terms representing these functions are called end-star terms. It is possible to define a preorder of end-star terms. Our interpretation is monotone over this preorder: if a certain end-star term is a witness for an existential statement, then any "bigger" term also is. Using this property, we are able to prove a soundness theorem for our interpretation, which eliminates principles recognisable from nonstandard analysis. From this theorem, we get as corollary the conservativity of nonstandard arithmetic over standard arithmetic, as well as a term extraction theorem. It is also possible to prove a characterization theorem for our interpretation. As corollary, we show that the countable saturation principle does not add proof theoretical strength to our intuitionistic nonstandard system. Finally, we give a short description of Weihrauch reducibility and comment on an application of Godel’s dialectica interpretation to, in certain circumstances, prove that a ∀∃-formula Weihrauch reduces to another one.}
}