2017/06/19 by Benno van den Berg, Berg, Benno van den, Lotte van Slooten +1
Arts and Humanities · #FOS: Mathematics #Logic (math.LO) #Philosophy and History of Science
paper · pdf · doi:10.48550/arxiv.1706.05901
openalex publication_date 2017/06/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.