Proof and definition in logic and type theory

Robin Adams

(Royal Holloway, University of London)

Most approaches to logic focus on proof. The logic consists of the axioms and rules of deduction that may be used when proving a theorem. Definitions are secondary: to say that a function is definable typically means just that a certain formula is provable. Type theory takes the opposite approach. A type theory specifies which operations are acceptable when constructing an object. With type theory, proof is secondary: to say that a theorem is provable means just that an object of a certain type is constructible.


Wednesday 2nd September 2009, 14:00
Robert Recorde Room
Department of Computer Science