Week 4, 4 February (17:00-19:00 Watson 310)

Study group: HoTT chapter 2

Speaker: Zachiri McKenzie (Cambridge)
Universal-existential sentences in the simple theory of types (slides)


Abstract: I will talk about ongoing research that is being done in collaboration with Anuj Dawar and Thomas Forster. The simple theory of types (TST) is a simplification, proposed independently by Ramsey and Chwistek, of the underlying system used in Russell and Whitehead’s Principia. This theory apparently avoids the set theoretic paradoxes by partitioning the universe into types and only allowing sets at a given successor type to contain objects from the preceding type. It has been conjectured that TST decides every universal-existential sentence. In this talk I will show that every existential-universal sentence that is true in some model of TST is true in all models of TST minus infinity that are generated by a sufficiently large finite number of atoms. The talk will continue with a sketch of a proof which shows that TST decides a subclass of the universal-existential sentences. Finally, I will discuss a connection between the universal-existential sentences of TST and the term model of a weakening of the theory of simple types.

About the seminar

The Midlands Logic Seminar was founded in 2011 and aims to cover all areas of mathematical logic, as well as related areas of theoretical computer science, and philosophy of mathematics.


All meetings for Term 2, 2013-14 will be Tuesday from 17:00-19:00 in room 310 of Watson Building (School of Mathematics) on the campus of the University of Birmingham.
  • campus map
  • google maps
    To get to campus, take the train from Birmingham New Street to the University stop (7 minutes).


    Dr Richard Kaye
    School of Mathematics
    University of Birmingham


    Dr Walter Dean
    Department of Philosophy
    University of Warwick