**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 <A HREF="https://doi.org/10.1093/oso/9780195147216.003.0010">here</A>), Gödel confirmed what Church had stated:

> In reply to your inquiry I would like to refer to the presentation of
> the facts that Professor Alonzo Church gave in his lecture at the last
> International Congress of Mathematicians. Mostowski's assertion <sub>[that Gödel, about 1940, had obtained most of Cohen's independence results]</sub>is
> incorrect insofar as I was merely in possession of certain partial
> results, namely, of proofs for the independence of the axiom of
> constructibility and of the axiom of choice in type theory. Because of
> my highly incomplete records from that time,  <sub>[entries in volumes 1 and 15 of his Arbeitshefte from Summer 1942]</sub> I can only
> reconstruct the first of these two proofs without difficulty. My
> method had a very close connection with that recently developed by
> Dana Scott and had less connection with
> Cohen's method. I never obtained a proof for the independence of the
> continuum hypothesis from the axiom of choice, and I found it very
> doubtful that the method that I used would lead to such a result.