History of Mac Lane's dissertation on abbreviated proving

Question

Saunders Mac Lane published his thesis (Abgekuerzte Beweise in Logikkalkul) which anticipated to some degree constructing proofs of theorems by constructing programs, giving a sufficient input, and proving the program would prove the theorem if executed, but not actually following out or executing the program.

1) Did anybody cite his thesis, prior the late 1970's? What is the first edition, if it was printed?

2) Mac Lane published a note in english (prior to coming back to the USA) that communicated his ideas to those who did not read his dissertation? What is the reference? And did anybody cite it prior the late 1970's?

He writes in his autobiography, and a chapter after the reprint, that it seemed to have no influence but anticipated much of the subject. Perhaps some mathematicians did read it but he was unaware they did?

Answer 1

It is clear now that nobody later was influenced or aware of either. The abstract was too vague. It was written also prior to the completed thesis. The two citations are: MacLane, Saunders, (Nov 1933) Jan 1934, Abbreviated Proofs in Logic Calculus, Bulletin of the American Mathematical Society 40(1):37--38. MacLane, Saunders, 1934, Abgekuerzte Beweise in Logikkalkul, Goettingen: Hubert.

The thesis had insignificant distribution, mostly to the author's few dozen local friends (who had not interest in the subject). Weyl and Bernays saw it as the advisors, of course but didn't consider it much mathematics.

It goes: an input and the repetitive processes operating on it, a program, if worked, is equivalent all intermediate results of program execution and the output. Let this be a proof; if so we have two identical proofs, one often much shorter than the other but equally simple. They have same mathematical symbolic content, the same information we would say if it were binary.

We record the symbolic repetitive inference procedures as the axiom symbolic inference functions, to be recursively applied as needed rather than recording any results of their use. This works there is proof that these functions give valid inferences and can recursively operated with, that they can compress symbols systems.

It is a compression scheme for standard logical symbolic proofs, similar to sets of shorter sequences and chunks having same information as the symbols sequences they chunked but requiring less storage, eliminating the storage problem (Miller 1956, Pribram 1970), and considering as equivalent bits strings and fewer bit programs that output these measurements sequences and so normalizing to common units the strings by the programs (Solomonoff 1960, Chaitin 1966).