Benno van den Berg: Arithmetical conservation results and Goodman’s Theorem

Abstract: A well–known result by Goodman [1] states that Heyting arithmetic in all finites types together with the axiom of choice for all types is conservative over Heyting arithmetic. Goodman’s original proof was quite complicated and many people have since tried to give more perspicuous proofs of his theorem, including Goodman himself, Beeson, Renardel de Lavalette, Coquand and possibly others. In this talk I will present my preferred proof, developed together with Lotte van Slooten, which combines ideas from all these authors and adds some new ones.

[1] N.J. Goodman, The theory of Gödel functionals, Journal of Symbolic Logic 41 (3), 1976, pp. 574–582