Week 2, 21 January (17:00-19:00 Watson 310)

Study group: HoTT chapter 2

Speaker: Walter Dean (Warwick)
On constructive validity and the interpretation of intuitionistic logic in the Theory of Constructions


I'll first survey several definitions of "A is constructively valid" with respect to which we might attempt to formulate the completeness of intuitionistic first-order logic (HPC). I'll next suggest that definitions which attempt to directly formalize the notion of construction which appears in the so-called Brouwer Heyting Kolmogorov interpretation of the intuitionistic connectives fare better than do various state-based notions of validity with respect to a number of potential adequacy conditions. I'll then present a system known as the Theory of Constructions (orginally due to Kreisel [1962/1965] and Goodman [1968/1970]), discuss a paradox about constructive validity pertaining to its formulation, and then show how a consistent variant of the theory can be used to interpret HPC. Time permitting, I'll also discuss how the Theory of Constructions is related to formalisms such as Intuitionistic Type Theory which are based on the propositions-as-types correspondence.

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