Ana Borges
Instituto Superior Técnico, Universidade de Lisboa
Abstract: We present a functional interpretation for nonstandard Heyting arithmetic based on previous work by Van den Berg, Briseid and Safarik [1]. 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 possibleto define a preorder of end-star terms. The interpretation is monotoneover this preorder: if a certain end-star term is a witness for anexistential statement, then any “bigger” term also is. Using thisproperty, we are able to prove asoundness theorem for theinterpretation, which eliminates principles recognisable from nonstandardanalysis. From this theorem, we get as corollary theconservativity of nonstandard arithmetic over standard arithmetic, aswell as a term extraction theorem.
[1] B. van den Berg, E. Briseid, and P. Safarik. A functional interpretation for nonstandard arithmetic. Annals of Pure and Applied Logic 163(2012), pp. 1962-1994.
This seminar is supported by National Funding from FCT - Fundação para a Ciência e a Tecnologia, under the project: UID/MAT/04561/2013.
