Arithmetical conservation results |
| |
Authors: | Benno van den Berg Lotte van Slooten |
| |
Affiliation: | 1. Institute for Logic, Language and Computation (ILLC), University of Amsterdam, P.O. Box 94242, 1090 GE Amsterdam, The Netherlands;2. Mathematical Institute, Utrecht University, P.O. Box 80010, 3508 TA Utrecht, The Netherlands |
| |
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. |
| |
Keywords: | Corresponding author. |
本文献已被 ScienceDirect 等数据库收录! |
|