FOM: Zermelo and Gentzen/Infinitary proof

[Taylor, Gregory]

In some late papers from the early 1930s Zermelo describes a theory of
infinitary proposition systems (Satzssysteme).  Part of this theory is a
concept of infinitary proof whereby a proof of a proposition p amounts to a
mental scan of a hierarchy of propositions in which p is situated.  Zermelo
is most interested, for technical reasons, in proof concepts involving
hierarchies with alpha levels, for alpha a strongly inaccessible cardinal.  

Zermelo's own, very brief, discussion of his new proof concepts focuses on
the hierarchies (or systems) of propositions themselves.  He says in several
places that the proof _is_ the system.  Describing his proofs as mental
scans or Gedankenexperimente was, I thought, pretty much my own idea.  I
have also never seen any discussion in the literature of Zermelo's proof
concepts per se aside from Moore's 1980 article.  However, to my surprise, I
recently came upon the following reference in Lakatos' Proofs and
Refutations (Cambridge, 1976), p. 52, fn. 2:

"Today the main dispute is about what is rigorous and what not in
set-theoretical and metamathematical proofs, as shown by the well-known
discussions about the admissibility of Zermelo's and Gentzen's
thought-experiments."

So now my own question for FOM subscribers is, What were these well-known
discussions?  Who were the participants?  Did they appear in print?
Lakatos' Chapter 1, from which the quotation is taken, first appeared in
1963-64.  So I am thinking that these discussions would have occurred in and
around British universities in the late 1950s perhaps.

With that in mind, I thought to look in Kreisel's papers, examining (1) the
1968 JSL "Survey of Proof Theory," (2) "Mathematical Logic" in Lectures in
Mathematics, edited by T. Saaty, (1963) and (3) "Mathematical Logic:  What
Has It Done for the Philosophy of Mathematics?" in Bertrand Russell:
Philosopher of the Century (London, 1967).  The first two of these articles
contain nothing concerning Zermelo on proof.  The third article does contain
the reconstruction of what Kreisel sees as Zermelo's argument for the
decidability of the Continuum Hypothesis in ZF2.  But I don't think that
this is what Lakatos is referring to.

Gregory Taylor
Computer Science Department
Trinity College (Hartford, CT, USA)