[FOM] Eliminability of AC

[Richard Zach]

An incidental question: Who first made the observation Joe has been
posting about (viz., that if an arithmetical (or even Sigma^1_2)
sentence follows from ZFC, it already follows from ZF)?  Solovay credits
a similar observation, namely that if an arithmetical sentence follows
from ZFC + GCH, it follws from ZFC alone, to Kreisel (Gödel's Collected
Works, vol II, p. 19).  

Best,
-RZ