# Arithmetical conservation results

## TL;DR

This paper proves Goodman's Theorem, showing that adding the axiom of choice to Heyting arithmetic in finite types does not expand the set of provable arithmetical sentences, using simplified methods and new insights.

## Contribution

It provides a new, simplified proof of Goodman's Theorem by integrating recent ideas, including van Oosten's work, and offers a corollary relevant to classical systems.

## Key findings

- Proof of Goodman's Theorem established
- A new corollary for classical systems derived
- Simplified proof technique introduced

## Abstract

In this paper we present a proof of Goodman's Theorem, a classical result in the metamathematics of constructivism, which states that the addition of the axiom of choice to Heyting arithmetic in finite types does not increase the collection of provable arithmetical sentences. Our proof relies on several ideas from earlier proofs by other authors, but adds some new ones as well. In particular, we show how a recent paper by Jaap van Oosten can be used to simplify a key step in the proof. We have also included an interesting corollary for classical systems pointed out to us by Ulrich Kohlenbach.