Speaker: David McAllester – Toyota Technological Institute at Chicago

Title: Type theory from the perspective of artificial intelligence

Abstract: This talk will discuss dependent type theory from the perspective of artificial intelligence and cognitive science. From an artificial intelligence perspective it will be argued that type theory is central to defining the “game” of mathematics — an action space and reward structure for pure mathematics. From a cognitive science perspective type theory provides a model of the grammar of the colloquial (natural) language of mathematics. Of particular interest is the notion of a signature-axiom structure class and the three fundamental notions of equality in mathematics — set-theoretic equality between structure elements, isomorphism between structures, and Birkoff and Rota’s notion of cryptomorphism between structure classes. This talk will present a version of type theory based on set-theoretic semantics and the 1930’s notion of structure and isomorphism given by the Bourbaki group of mathematicians. It will be argued that this “Bourbaki type theory” (BTT) is more natural and accessible to classically trained mathematicians than Martin-Löf type theory (MLTT). BTT avoids the Curry-Howard isomorphism and axiom J of MLTT. The talk will also discuss BTT as a model of MLTT. The BTT model is similar to the groupoid model in that propositional equality is interpreted as isomorphism but different in various details. The talk will also briefly mention initial thoughts in defining an action space and reward structure for a game of mathematics.