JAIST Logic@JAIST

Point-free foundations of Mathematics

  • Dr. Marco Benini
  • Dipartimento di Scienze Teoriche e Applicate Università degli Studi dell’Insubria
Date: 2014/05/22 (Thu) 15:30 to 17:00
Place: JAIST Collaboration Room 6 (I57-g)
Group: Logic Unit
Is it possible to work with logical theories without assuming the existence of a universe where to interpret terms? This talk will positively answer to the above question in the case of first-order, intuitionistic-based theories by providing a class of models, defined inside Category Theory, such that they allow to interpret theories in a sound and complete way. Furthermore, the models explain the computational meaning of the corresponding theories via a semantic version of the Curry-Howard isomorphism. And their peculiar aspect is that they provide no universe where to interpret terms.