We all know Gödel proved the consistency of the Axiom of Choice with $\mathsf{ZF}$ using his constructible universe, and Cohen proved the consistency of $\neg \mathsf{AC}$ using his new method of forcing some thirty years later. In the excellent book Zermelo's Axiom of Choice by G.H. Moore, there...

Q1: Except for those quotes, is there any tangible trace of such a proof obtained by Gödel? Gödel commented on his independence results in a letter dated June 30, 1967 to W. Rautenberg. In his reply (in German, translated here), Gödel confirmed what Church had stated: In reply to your inquiry I ...