Logic Seminar

Scott Messick
A history of foundations with a bias toward $\lambda$-calculus and type-free systems, part 2

Tuesday, September 12, 2017 - 2:55pm
Malott 206

Despite the name, this talk should make sense for anyone; attendance of part 1 is not needed. In part 2 I will shift to focus more specifically on two threads in the modern history of foundations: constructive type theories and type-free systems. I'll talk about how these kinds of systems were developed historically and how they contrast ontologically with each other and with set theoretic foundations. I'll go into more detail on the two major strong type-free foundational systems in the literature: Myhill and Flagg's system (1989) and Grue and Berline's system Map Theory (1992-2016), and contrast these with each other. Finally, I'll discuss which properties of those two systems I do and do not want to incorporate into my own system under construction, called OE (Operations and Equalities).