Please use this identifier to cite or link to this item:
Title: Completeness in Equational Hybrid Propositional Type Theory
Author: Manzano Arjona, María
Huertas Sánchez, María Antonia
Martins, Manuel A.
Keywords: Propositional type theory
Hybrid logic
Equational logic
Issue Date: 20-Oct-2018
Publisher: Studia Logica
Citation: Manzano Arjona, M., Huertas, M.A. & Martins, M.A. (2018). Completeness in Equational Hybrid Propositional Type Theory. Studia Logica, (), 1-40. doi: 10.1007/s11225-018-9833-5
Also see:
Abstract: Equational hybrid propositional type theory (EHPTT) 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 (a nonempty set with functions) and a Kripke frame. The main result in this paper is the proof of completeness of a calculus specifically defined for this logic. 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. More precisely, from (i) and (ii) we take the idea of building the model described by the maximal consistent set; in our case the maximal consistent set has to be named, -saturated and extensionally algebraic-saturated due to the hybrid and equational nature of EHPTT. From (iii), we use the result that any element in the hierarchy has a name. The challenge was to deal with all the heterogeneous components in an integrated system.
Language: English
ISSN: 0039-3215MIAR

Appears in Collections:Articles

Files in This Item:
File SizeFormat 
EquationalHybrid.pdf739.24 kBAdobe PDFView/Open Request a copy

Items in repository are protected by copyright, with all rights reserved, unless otherwise indicated.