Completeness in Equational Hybrid Propositional Type Theory

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


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.



    Upload a copy of this work     Papers currently archived: 76,264

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

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.
On Some Completeness Theorems in Modal Logic.D. Makinson - 1966 - Mathematical Logic Quarterly 12 (1):379-384.


Added to PP

6 (#1,104,593)

6 months
1 (#449,844)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Citations of this work

Add more citations

References found in this work

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.
A theory of propositional types.Leon Henkin - 1963 - Fundamenta Mathematicae 52:323-334.

View all 14 references / Add more references