I will sketch a brief motivation for my project to design a new foundational system, and then dive into the history of formal foundations. This talk will cover the period of approximately 1870-1950. Highlights will include the work of Frege, Hilbert's program, Principia Mathematica (Russell and Whitehead), Zermelo's axiomatization of set theory and Fraenkel's later improvement, Brouwer's intuitionism and his conflict with Hilbert, Gödel's incompleteness theorems, and Church's λ-calculus, all with detailed technical commentary (or at least, more detailed than usual historical overviews).

The history is of independent interest, of course, but will also help facilitate an explanation of what properties I want in a new system. The history gives context and clues as to the fundamental capabilities and limitations of formal systems, as well as psychological pitfalls for the humans who study them. Audience commentary and discussion is strongly encouraged!