On Goodman realizability

Emanuele Frittaion, University of Leeds. Part of the Logic Seminar Series.

Goodman's theorem (after Nicholas D. Goodman) asserts that adding the axiom of choice to intuitionistic arithmetic in all finite types yields a system which is conservative over Heyting arithmetic. This is in contrast with classical arithmetic in all finite types. In fact, the combination of choice with classical logic results in a system as strong as full second order arithmetic.

There are several proofs of this result. The most direct proof was given by Goodman in his paper "Relativized realizability in intuitionistic arithmetic of all finite types", J. Symbolic Logic 43 (1978) and is based on a realizability interpretation which combines Kleene recursive realizability with Kripke semantics. I will discuss this notion of realizability and then present a modified version of Goodman realizability that shows that intuitionistic arithmetic in all finite types augmented with both choice and extensionality is also conservative over Heyting arithmetic.

The first proof of the extensional case was given by Beeson in "Goodman’s theorem and beyond", Pacific J. Math. (1979). Other proofs can be found in Gordeev  "Proof-theoretical analysis: weak systems of functions and classes", Ann. Pure Appl. Logic (1988), and more recently in van den Berg and Slotte "Arithmetical conservation results", Indagationes Mathematicae (2017).

Check out: Emanuele Frittaion "On Goodman realizability" (see https://arxiv.org/abs/1801.04968)