TL;DR
This paper revises Goodman realizability and offers a new proof showing that certain extensions of intuitionistic arithmetic do not increase its proof-theoretic strength, maintaining conservativity over Heyting arithmetic.
Contribution
It introduces a modified version of Goodman realizability and provides a novel proof for the extensional case, extending previous results.
Findings
The modified realizability preserves conservativity.
A new proof technique for the extensional case.
Reinforces the understanding of the relationship between extended arithmetic systems.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.