arXiv · 1801.04968
On Goodman realizability
Abstract
Goodman's theorem (1976) states that intuitionistic finite-type arithmetic plus the axiom of choice plus the axiom of relativized dependent choice is conservative over Heyting arithmetic. The same result applies to the extensional variant. This is due to Beeson (1979). In this paper we modify Goodman realizability (1978) and provide a new proof of the extensional case.
Explore related subjects
Keep this discovery
Emanuele Frittaion. 2018-01-15. On Goodman realizability. https://doi.org/10.1215/00294527-2019-0018
Cite the original work for its findings. Save a collection to share your selection of sources.