I am reading Turing's 1939 paper on ordinal logic ("Systems of Logic Based on Ordinals", A. M. Turing, Proc. London Math. Soc. ser. 2, 45 (1939), #1, 161-228, DOI: 10.1112/plms/s2-45.1.161.) Immediately after talking about successively extending axiomatic systems using transfinite iteration of the reflection principle, he says, on p. 197: "Another ordinal logic of this type has in effect been introduced by Church". Does anyone know what this is referring to? Turing gives two references in a footnote, but the first gives no details and the second is mimeographed notes which I don't have.
Turing's 1939 paper on ordinal logic
5
$\begingroup$
reference-request
logic
-
1For those who want to take a look: Turing writes that the ordinal logic is in outline contained on pages 279-280 of Church's *A Proof of Freedom from Contradiction*, PNAS 1935 21 (5) 275-281, available [here](http://www.pnas.org/content/21/5.toc). – 2012-01-05