Midlands Logic Seminar

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.