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.

To get to campus, take the train from Birmingham New Street to the University stop (7 minutes).

School of Mathematics

University of Birmingham

http://web.mat.bham.ac.uk/R.W.Kaye/

Dr Walter Dean

Department of Philosophy

University of Warwick

http://go.warwick.ac.uk/whdean