Completeness in Equational Hybrid Propositional Type Theory
Studia Logica 107 (6):1159-1198 (2019)
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. 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.Author Profiles
My notes
Similar books and articles
Completeness in Equational Hybrid Propositional Type Theory.Maria Manzano, Manuel Martins & Antonia Huertas - 2019 - Studia Logica 107 (6):1159-1198.
A Hilbert-Style Axiomatisation for Equational Hybrid Logic.Luís S. Barbosa, Manuel A. Martins & Marta Carreteiro - 2014 - Journal of Logic, Language and Information 23 (1):31-52.
Completeness in Hybrid Type Theory.Carlos Areces, Patrick Blackburn, Antonia Huertas & María Manzano - 2013 - Journal of Philosophical Logic (2-3):1-30.
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.
Proof-Theoretic Functional Completeness for the Hybrid Logics of Everywhere and Elsewhere.Torben Braüner - 2005 - Studia Logica 81 (2):191-226.
Pure extensions, proof rules, and hybrid axiomatics.Patrick Blackburn & Balder Ten Cate - 2006 - Studia Logica 84 (2):277-322.
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.
Hybrid logics with infinitary proof systems.Rineke Verbrugge, Gerard Renardel de Lavalette & Barteld Kooi - unknown
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.
Analytics
Added to PP
2019-12-20
Downloads
6 (#1,104,593)
6 months
1 (#449,844)
2019-12-20
Downloads
6 (#1,104,593)
6 months
1 (#449,844)
Historical graph of downloads
Author Profiles
Citations of this work
Identity, equality, nameability and completeness. Part II.María Manzano & Manuel Crescencio Moreno - 2018 - Bulletin of the Section of Logic 47 (3):141.
References found in this work
The completeness of the first-order functional calculus.Leon Henkin - 1949 - Journal of Symbolic Logic 14 (3):159-166.
Modal logic: A semantic perspective.Patrick Blackburn & Johan van Benthem - 1988 - Ethics 98:501-517.
Pure extensions, proof rules, and hybrid axiomatics.Patrick Blackburn & Balder Ten Cate - 2006 - Studia Logica 84 (2):277-322.