Por Manuel Martins (Universidade de Aveiro).

Abstract: Equational Hybrid Propositional Type Theory is a combination of propositional type theory, equational logic and hybrid modal logic. The structures used to interpret the language contain a hierarchy of propositional types, an algebra and a Kripke frame. In this talk we present a calculus for this logic that combines the axiomatics of its three components. The completeness proof is based on the three proofs Henkin published last century: (i) Completeness in type theory (ii) The completeness of the first-order functional calculus and (iii) Completeness in propositional type theory. The challenge was to deal with all the heterogeneous components in an integrated system.
(This is joint work with Maria Manzano and Antonia Huertas).