Arithmetical conservativity results, a theory of operations and Goodman's theorem

Abstract

We present a new theory of operations HAP$_{\epsilon}$ and show that it is a conservative extension of Heyting Arithmetic. An important property of HAP$_{\epsilon}$ is that in this system all arithmetical formulas are self-realising. This will allow us to give a new proof of Goodman's theorem. Our proof of Goodman's theorem uses the proof interpretations realizability and forcing and is inspired by the work of Michael Beeson \cite{beeson} and Gerard Renardel de Lavalette \cite{lavalette}. In contrast to their proofs, we broke up the proof of Goodman's theorem into four steps, making sure we only use one proof interpretation at the time. This makes each step easier to understand.