Bruno Dinis (Universidade de Lisboa, CMAFCIO)
Abstract: In this two-part talk I will present a bounded modified realizability and a bounded functional interpretation for intuitionistic nonstandard arithmetic in finite types with nonstandard principles. These interpretations are sound and complete and allow to fulfill a three part goal: (i) to obtain constructive content for nonstandard arithmetic via the extraction of bounds on witnesses; (ii) to study proof-theoretic properties of nonstandard arithmetic; (iii) to fill a gap in the literature, being in line with nonstandard methods to analyze compactness arguments.
The functional interpretation presented in this talk is the intuitionistic counterpart of the functional interpretation presented by Ferreira and Gaspar. In fact, by extending Krivine's negative translation and combining it with our intuitionistic functional interpretation one obtains Ferreira and Gaspar's classical functional interpretation for nonstandard arithmetic. Moreover, restricting the realizability and the functional interpretation to the so-called "purely external fragment" one recovers respectively the bounded modified realizability of Ferreira and Nunes and the bounded functional interpretation of Ferreira and Oliva. Our interpretations also bear similarities with a functional interpretation presented by Van den Berg, Briseid and Safarik but replacing finiteness conditions by majorizability conditions.
I will make some remarks concerning the Transfer principle and present versions with truth of both the realizability and the functional interpretation. These versions with truth will allow to introduce the so-called "copies-only method" that allows to give a faster proof of the soundness theorem.
(Joint work with Jaime Gaspar)
Room 6.2.33 [⤴]