Studia Logica 107 (6):1159-1198 (2019)

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. 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: Completeness in type theory, The completeness of the first-order functional calculus and Completeness in propositional type theory. More precisely, from and 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 \. From, 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.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1007/s11225-018-9833-5
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 51,304
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Completeness in the Theory of Types.Leon Henkin - 1950 - Journal of Symbolic Logic 15 (2):81-91.
The Completeness of the First-Order Functional Calculus.Leon Henkin - 1949 - Journal of Symbolic Logic 14 (3):159-166.
Completeness in Hybrid Type Theory.Carlos Areces, Patrick Blackburn, Antonia Huertas & María Manzano - 2014 - Journal of Philosophical Logic 43 (2-3):209-238.

View all 14 references / Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Hybrid Identities and Hybrid Equational Logic.Klaus Denecke - 1995 - Mathematical Logic Quarterly 41 (2):190-196.
Completeness: From Gödel to Henkin.Maria Manzano & Enrique Alonso - 2014 - History and Philosophy of Logic 35 (1):1-26.
An Approach to Infinitary Temporal Proof Theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Completeness in Hybrid Type Theory.Carlos Areces, Patrick Blackburn, Antonia Huertas & María Manzano - 2014 - Journal of Philosophical Logic 43 (2-3):209-238.
Basic Propositional Calculus I.Mohammad Ardeshir & Wim Ruitenburg - 1998 - Mathematical Logic Quarterly 44 (3):317-343.
Validity Measurement in Some Propositional Logics.Branislav Boričić - 1997 - Mathematical Logic Quarterly 43 (4):550-558.
Basic Propositional Calculus I.Mohamed Ardeshir & Wim Ruitenberg - 1998 - Mathematical Logic Quarterly 44 (3):317-343.
Resolution Calculus for the First Order Linear Logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.
Russell's Completeness Proof.Peter Milne - 2008 - History and Philosophy of Logic 29 (1):31-62.
Intensional Models for the Theory of Types.Reinhard Muskens - 2007 - Journal of Symbolic Logic 72 (1):98-118.


Added to PP index

Total views
12 ( #718,492 of 2,330,104 )

Recent downloads (6 months)
4 ( #193,234 of 2,330,104 )

How can I increase my downloads?


My notes