×

Completeness in equational hybrid propositional type theory. (English) Zbl 07142215

Summary: Equational hybrid propositional type theory \((\mathsf{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, \( \Diamond \)-saturated and extensionally algebraic-saturated due to the hybrid and equational nature of \(\mathsf{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.

MSC:

03B38 Type theory
03B45 Modal logic (including the logic of norms)
03C05 Equational classes, universal algebra in model theory

Software:

ETPS
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Andrews, P., A reduction of the axioms for the theory of propositional types, Fundamenta Mathematicae 52: 345-350, 1963. · Zbl 0127.00701 · doi:10.4064/fm-52-3-345-350
[2] Andrews, P., An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press, Cambridge 1986. · Zbl 0617.03001
[3] Areces, C., P. Blackburn, A. Huertas, and M. Manzano, Completeness in Hybrid Type Theory, J Philos Logic (Journal of Philosophical Logic) 43(2-3): 209-238, 2014. https://doi.org/10.1007/s10992-012-9260-4. · Zbl 1338.03031 · doi:10.1007/s10992-012-9260-4
[4] Barbosa, L., S. Martins, A. Manuel, and M. Carreteiro, A Hilbert-style axiomatisation for equational hybrid logic, Journal of Logic, Language and Information 23(1): 31-52, 2014. · Zbl 1305.03017 · doi:10.1007/s10849-013-9184-6
[5] Blackburn, P., and J. van Benthem, Modal Logic: A Semantic Perspective. Handbook of Modal Logic, Elsevier, New York 2007. · Zbl 1114.03001
[6] Blackburn, P., and B. ten Cate, Pure Extensions, Proof Rules and Hybrid Axiomatics, Studia Logica 84: 277-322, 2006. · Zbl 1115.03009 · doi:10.1007/s11225-006-9009-6
[7] Henkin, L., The completeness of the first order functional calculus, The Journal of Symbolic Logic 14: 159-166, 1949. · Zbl 0034.00602 · doi:10.2307/2267044
[8] Henkin, L., Completeness in the theory of types, The Journal of Symbolic Logic 15: 81-91, 1950. · Zbl 0039.00801 · doi:10.2307/2266967
[9] Henkin, L., Some notes on nominalism, The Journal of Symbolic Logic 18: 19-29, 1953. · Zbl 0072.24903 · doi:10.2307/2266323
[10] Henkin, L., A theory of propositional types, Fundamenta Mathematicae 52: 323-344, 1963. · Zbl 0127.00609 · doi:10.4064/fm-52-3-323-344
[11] Henkin, L., Identity as a logical primitive, Philosophia 5: 31-45, 1975. · doi:10.1007/BF02380832
[12] Manzano, M., Extensions of First Order Logic, Cambridge Univ. Press., Cambridge, 1996. · Zbl 0848.03001
[13] Manzano, M., M. A. Martins, and A. Huertas, A semantics for equational hybrid propositional type theory, Bulletin of the Section of Logic 43(3-4): 121-138, 2014. · Zbl 1318.03031
[14] Manzano, M., Henkin on Completeness, in M. Manzano, I. Sain, and E. Alonso, (eds.), The Life and Work of Leon Henkin. Essays on His Contributions, Springer International Publishing, 2014, pp. 149-176. · Zbl 1300.01009
[15] Manzano, M., and M. C. Moreno, Identity, equality, nameability and completeness, Bulletin of the Section of Logic 46(3/4): 169-195, 2017. · Zbl 1423.03042
[16] Manzano, M., and M. C. Moreno, Identity, Equality, nameability and completeness—Part II, Bulletin of the Section of Logic. To appear. · Zbl 1437.03051
[17] Quine, W., Logic based on inclusion and abstraction, The Journal of Symbolic Logic 2: 145-152, 1937. · Zbl 0018.19402 · doi:10.2307/2268279
[18] Ramsey, F. P., The foundations of mathematics, Proceedings L. M. S. 25(2): 338-384, 1926. · JFM 52.0046.01 · doi:10.1112/plms/s2-25.1.338
[19] Tarski, A., Sur le terme primitif de la logistique, Fundamenta Mathematicae 4: 196-200, 1923. · JFM 49.0031.01 · doi:10.4064/fm-4-1-196-200
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.