First-order transitional modal logics of quasiary predicates with equality
DOI:
https://doi.org/10.17721/1812-5409.2025/1.23Keywords:
modal logic, transitional modal system, predicate, equality, logical consequenceAbstract
In this paper we study new classes of program-oriented logical formalisms of the modal type – first-order transitional modal logics (TML) of quasiary predicates with equality. Modal logics are successfully used for describing and modeling various subject areas. Epistemic logics are used to describe artificial intelligence, information, and expert systems. Temporal logics are used for modeling complex dynamic systems, program specification and verification. Traditional modal logics are based on classical predicate logic. However, such logic insufficiently accounts for the incompleteness, partiality and structuredness of information about the subject area. These limitations necessitate the development of new, program-oriented modal logical formalisms; this underscores the relevance of the proposed paper. We consider pure first-order TML of partial quasiary predicates without monotonicity condition and enriched with equality predicates. Two types of such logics can be distinguished: TMLQ≡ with strong equality predicates ≡х, and TMLQ= with weak equality predicates =ху. A feature of these logics is the use of the extended renomination composition. For quantifier elimination in TMLQ≡, special total indicator predicates Ez are used, while in TMLQ= the partial indicator predicates are =zz. Transitional modal systems (TMS) form the semantic basis of TML. For TMLQ≡ and TMLQ= important varieties of such systems are specified: general (GMSQ≡ and GMSQ=), temporal (TmMSQ≡ and TmMSQ=), and multimodal (MMSQ≡ and MMSQ=). We describe semantic models and languages of these TMS and examine the properties related to equality predicates. Four types of consequence relations in TMS and logical consequence relations on sets of formulas specified with states are considered: irrefutability (IR), truth (T), falsity (F), and strong (TF). The properties of replacement of equals in TMLQ≡ and TMLQ= are described. The properties of logical consequence relations on sets of formulas specified with states are the semantic basis for the further construction of the corresponding sequent type calculi.
Pages of the article in the issue: 174 - 181
Language of the article: English
References
Abramsky, S., Gabbay, D. M., & Maibaum, T. S. E. (Eds). (1993–2000). Handbook of Logic in Computer Science (Vol. 1–5). Oxford University Press.
Baier, C., & Katoen, J. (2008). Principles of Model Checking. MIT Press.
Bjorner, D., & Henson, M. C. (Eds). (2008). Logics of Specification Languages, EATCS Series. Springer.
Blackburn, P., van Benthem, J., & Wolter, F. (Eds). (2006). Handbook of Modal Logic. Elsevier.
Cocchiarella, N., & Freund, M. (2008). Modal Logic. An Introduction to its Syntax and Semantics. Oxford University Press.
Fisher, M. (2011). An Introduction to Practical Formal Methods Using Temporal Logic. Somerset, NJ: Wiley.
Fitting, M., & Mendelsohn, R. (2023) First-Order Modal Logic. Springer.
Goranko, V. (2023). Temporal Logics. Cambridge University Press.
Kröger, F. & Merz, S. (2008).Temporal Logic and State Systems. Springer-Verlag.
Nikitchenko, M., Shkilniak, O., & Shkilniak, S. (2016). Pure first-order logics of quasiary predicates. Problems in Programming, 2–3, 73–86 [in Ukrainian].
Shkilniak, O. (2015). Modal logics of non-monotone partial predicates. Bulletin of Taras Shevchenko National University of Kyiv. Series Physics & Mathematics, 3, 141–147 [in Ukrainian].
Shkilniak, O., & Shkilniak, S. (2023). First-Order Sequent Calculi of Logics of Quasiary Predicates with Extended Renominations and Equality. Proceedings of UkrPROG'2022, Kyiv, Ukraine. CEUR Workshop Proceedings (CEUR-WS.org), 3–18.
Shkilniak, O., & Shkilniak, S. (2024). Modal Logics of Partial Quasiary Predicates with Equality. Proceedings of DSMSI-23. Kyiv, Ukraine. CEUR Workshop Proceedings (CEUR-WS.org), 35–48.
Shkilniak, S. (2019). First-order composition-nominative logics with predicates of weak equality and of strong equality. Problems in Programming, 3, 28–44 [in Ukrainian].
Downloads
Published
Issue
Section
License
Copyright (c) 2025 Oksana Shkilniak
This work is licensed under a Creative Commons Attribution 4.0 International License.
Authors who publish with this journal agree to the following terms:
- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).
