Emanuele Frittaion
CMAFCIO, Universidade de Lisboa

Abstract: Goodman's theorem (after Nicholas D. Goodman) asserts that adding the axiom of choice to intuitionistic arithmetic in all finite types yields a system which is conservative over Heyting arithmetic. This is in contrast with classical arithmetic in all finite types. In fact, the combination of choice with classical logic results in a system as strong as full second-order arithmetic.

There are several proofs of this result. The most direct proof was given by Goodman in his paper "Relativized realizability in intuitionistic arithmetic of all finite types", J. Symbolic Logic 43 (1978) and is based on a realizability interpretation which combines Kleene recursive realizability with Kripke semantics. I will discuss this notion of realizability and then present a modified version of Goodman realizability that shows that intuitionistic arithmetic in all finite types augmented with both choice and extensionality is also conservative over Heyting arithmetic. The only proof of this result is due to Michael Beeson.

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.