Goodman's theorem

Let HA denote Heyting (intuitionistic) arithmetic and HA\(^\omega\) be Heyting arithmetic extended to the language of finite types, i.e. with quantifiers for each finite type. AC stands for the axiom of choice. Finally, recall that a formula is arithmetical if it only contains quantifications over numbers.

In [1,2] Goodman proved the following amazing result:

Theorem. If HA\(^\omega\) + AC proves an arithmetical formula \( A \) then HA already proves \( A \).

In proof theory one would simply say that HA\(^\omega\) + AC is conservative over HA. The fact that HA\(^\omega\) is conservative over HA was already known and is easy to show. But the conservation of HA\(^\omega\) + AC over HA is quite a surprising result.

Recall that adding the axiom of choice to classical mathematics leads to all sorts of strange things (e.g. the Banach-Tarski paradox). Goodman's theorem essentially says that this is not the fault of the axiom of choice, but rather a fault of the combination of the axiom of choice with classical logic. Classical logic on its own makes perfect sense. The axiom of choice in an intuitionistic setting is harmless. But when these two are put together all hell breaks loose.

Proof of Goodman's theorem. Goodman's proof involves two major proof-theoretic techniques: forcing and realizability. Realizability is used to eliminate the axiom of choice, since the axiom of choice has a trivial realizer. But then one ends up with a proof of "\(t\) realizes \(A\)". Forcing is used to recover the truth of \( A \) given that \( A \) has a realizer. That is done by choosing the forcing conditions to be approximations of the Skolem functions of the sub-formulas of \( A \). So, the axiom of choice is replaced by finite approximations of Skolem functions! Let's see a few of the details:

We present here a sketch of Beeson's proof [3] of Goodman's theorem. Beeson's proof has the advantage (over Goodman's proof) that the two techniques of forcing and realizability are clearly separated. The proof consists of the following steps:

(1) Let \( A \) be an arithmetical formula such that HA\(^\omega\) + AC \( \vdash A \).

(2) Let HA\(^\omega_a \) denote the extension of HA\(^\omega\) with a new function symbol \( a \). By the soundness of Kleene realizability relative to \( a \) we have HA\(^\omega_a \vdash t \) realizes \( A \), where \( t \) is a term of HA\(^\omega_a \).

(3) By the soundness of the forcing interpretation we have HA\(^\omega \vdash \exists p (p \Vdash t \) realizes \( A) \), where the forcing conditions are chosen as in the main lemma (below). Forcing is done as usual, with the crucial difference that in the forcing of the atomic formulas the forcing condition \( p \) replaces the "generic" function \( a \), i.e. \( p \Vdash a(n) = m \) is defined as \( p(n) = m \), where I'm actually using the equality symbol "=" for partial equality.

(4) By the main lemma HA\(^\omega \vdash \forall p \exists q \leq p (q \Vdash (t \) realizes \( A) \Rightarrow A) \).

(5) By (3) and (4) we have HA\(^\omega \vdash \exists q (q \Vdash A) \).

(6) As for arithmetical formula HA\(^\omega \vdash (q \Vdash A) \Leftrightarrow A \) we have, HA\(^\omega \vdash A \).

Steps (2) and (3) are pretty standard realizability and forcing interpretations. And only the soundness theorems of these are used. Step (6) is also easy to check by a simple induction on \( A \). So, the crucial bit of the proof is the choice of the forcing conditions and the main lemma which we discuss next.

Main lemma. Fix an arithmetical sentence \( A \). Then there is a set \( C \) of forcing conditions such that $$ \mbox{HA}^\omega \vdash \forall p \exists q \leq p (q \Vdash (t  \mbox{ realizes } A) \Rightarrow A). $$
Proof of main lemma. The set of forcing conditions \( C \) consists of finite functions \( p \) which are approximations to the Skolem functions of all sub-formulas of \( A \). More precisely, these are partial functions \( p \) with finite domain such that for each sub-formula \( B(x, y) \) of \( A \) we have $$ \exists x B(x, y) \wedge (p_{\exists x B(x, y)}(y) \mbox{ defined }) \Rightarrow B(p_{\exists x B(x, y)}(y), y).$$ Hence, whenever the approximation to the Skolem function \( p_{\exists x B(x, y)} \) is defined then it produces the right witness. Relative to these (approximation of) Skolem functions, it's easy to show the following:

(i) HA\(^\omega \vdash \forall p \exists q \leq p (q \Vdash (B(y) \Rightarrow \{j_B\}(y) \mbox{ realizes } B )) \), for some index \( j_B \) which we can construct (using the Skolem functions).

(ii) HA\(^\omega \vdash \forall p \exists q \leq p (q \Vdash (t \mbox{ realizes } B ) \Rightarrow B) \).

Remark. Ulrich Kohlenbach [4] has shown the interesting fact that Goodman's theorem does not hold for fragments of HA\(^\omega\). This means that in order to eliminate AC from the proof of an arithmetical formula \( A \) we might have to use a more complex induction than in the proof which is allowed to use AC. Thierry Coquand [5] has just published another proof of Goodman's theorem.

[1] Goodman, N., The theory of the Gödel functionals, Journal of Symbolic Logic 41, 574-583 (1976)

[2] Goodman, N. Relativized realizability in intuitionistic arithmetic of all finite types. Journal of Symbolic Logic 43, pp. 23-44 (1978)

[3] Beeson, M., Goodman's theorem and beyond. Pacific J. Math. 84, 1-16 (1979)

[4] Kohlenbach, U., A note on Goodman's theorem. Studia Logica 63, 1-5 (1999)

[5] Coquand, T., About Goodman's theorem. Annals of Pure and Applied Logic 164(4), 437-442 (2013)