{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T08:23:07Z","timestamp":1761294187531,"version":"build-2065373602"},"reference-count":25,"publisher":"MDPI AG","issue":"10","license":[{"start":{"date-parts":[[2020,9,23]],"date-time":"2020-09-23T00:00:00Z","timestamp":1600819200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100006108","name":"Kult\u00farna a Edukacn\u00e1 Grantov\u00e1 Agent\u00fara M\u0160VVa\u0160 SR","doi-asserted-by":"publisher","award":["011TUKE-4\/2020 - A development of the new semantic technologies in educating of young IT experts"],"award-info":[{"award-number":["011TUKE-4\/2020 - A development of the new semantic technologies in educating of young IT experts"]}],"id":[{"id":"10.13039\/501100006108","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100013693","name":"Slowakische Akademische Informationsagentur","doi-asserted-by":"publisher","award":["2019-10-15-003 - Semantic Modeling of Component-Based Program Systems under the bilateral program Aktion \u00d6sterreich--Slowakei, Wissenschafts- und Erziehungskooperation"],"award-info":[{"award-number":["2019-10-15-003 - Semantic Modeling of Component-Based Program Systems under the bilateral program Aktion \u00d6sterreich--Slowakei, Wissenschafts- und Erziehungskooperation"]}],"id":[{"id":"10.13039\/501100013693","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Johannes Kepler University Linz, Linz Institute of Technology (LIT)","award":["Project LOGTECHEDU - Logic Technology for Computer Science Education"],"award-info":[{"award-number":["Project LOGTECHEDU - Logic Technology for Computer Science Education"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Symmetry"],"abstract":"<jats:p>We present a categorical formalization of a variant of first-order logic. Unlike other texts on this topic, the goal of this paper is to give a very transparent and self-contained account without requiring more background than basic logic and set theory. Our focus is to show how the semantics of first-order formulas can be derived from their usual deduction rules. For understanding the core ideas, it is not necessary to investigate the internal term structure of atomic formulas, thus we abstract atomic formulas to (syntactically opaque) relations; in this sense, our variant of first-order logic is \u201crelational\u201d. While the derived semantics is based on categorical principles (even the duality that arises from a symmetry between two ways of looking at something where there is no reason to choose one over the other), it is nevertheless \u201cconstructive\u201d in that it describes explicit computations of the truth values of formulas. We demonstrate this by modeling the categorical semantics in the RISCAL (RISC Algorithm Language) system which allows us to validate the core propositions by automatically checking them in finite models.<\/jats:p>","DOI":"10.3390\/sym12101584","type":"journal-article","created":{"date-parts":[[2020,9,24]],"date-time":"2020-09-24T03:03:39Z","timestamp":1600916619000},"page":"1584","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["A Novel Categorical Approach to Semantics of Relational First-Order Logic"],"prefix":"10.3390","volume":"12","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9860-1557","authenticated-orcid":false,"given":"Wolfgang","family":"Schreiner","sequence":"first","affiliation":[{"name":"Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Altenbergerstra\u00dfe 69, A-4040 Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2852-9403","authenticated-orcid":false,"given":"William","family":"Steingartner","sequence":"additional","affiliation":[{"name":"Faculty of Electrical Engineering and Informatics, Technical University of Ko\u0161ice, Letn\u00e1 9, 042 00 Ko\u0161ice, Slovakia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9992-3849","authenticated-orcid":false,"given":"Valerie","family":"Novitzk\u00e1","sequence":"additional","affiliation":[{"name":"Faculty of Electrical Engineering and Informatics, Technical University of Ko\u0161ice, Letn\u00e1 9, 042 00 Ko\u0161ice, Slovakia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2020,9,23]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"341","DOI":"10.2307\/2102968","article-title":"The Semantic Conception of Truth: In addition, the Foundations of Semantics","volume":"4","author":"Tarski","year":"1944","journal-title":"Philos. Phenomenol. Res."},{"key":"ref_2","unstructured":"Schmidt, D.A. (1986). Denotational Semantics\u2014A Methodology for Language Development, Allyn and Bacon."},{"key":"ref_3","unstructured":"Awodey, S. (2010). Category Theory, Oxford University Press. [2nd ed.]."},{"key":"ref_4","unstructured":"Barr, M., and Wells, C. (1990). Category Theory for Computing Science, Prentice-Hall, Inc., Division of Simon and Schuster One Lake Street."},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Brandenburg, M. (2017). Einf\u00fchrung in Die Kategorientheorie, Springer Spektrum. (In German).","DOI":"10.1007\/978-3-662-53521-9"},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Pierce, B.C. (1991). Basic Category for Computer Scientists, MIT Press.","DOI":"10.7551\/mitpress\/1524.001.0001"},{"key":"ref_7","unstructured":"Spiwak, D.I. (2014). Category Theory for the Sciences, MIT Press."},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1111\/j.1746-8361.1969.tb01194.x","article-title":"Adjointness in Foundations","volume":"23","author":"Lawvere","year":"1969","journal-title":"Dialectica"},{"key":"ref_9","unstructured":"Jacobs, B. (1999). Categorical Logic and Type Theory, Elsevier. Studies in Logic and the Foundations of Mathematics."},{"key":"ref_10","first-page":"277","article-title":"Logic and Categories As Tools For Building Theories","volume":"27","author":"Abramsky","year":"2010","journal-title":"J. Indian Counc. Philos. Res. Issue Log. Philos. Today"},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Poign\u00e9, A. Category Theory and Logic. Proceedings of the Category Theory and Computer Programming: Tutorial and Workshop, Guildford, UK, 16\u201320 September 1985, Springer. Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-17162-2_119"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-642-12821-9_1","article-title":"Introduction to Categories and Categorical Logic","volume":"Volume 813","author":"Abramsky","year":"2010","journal-title":"New Structures for Physics"},{"key":"ref_13","unstructured":"RISCAL (2020, July 09). The RISC Algorithm Language (RISCAL). Available online: https:\/\/www3.risc.jku.at\/research\/formal\/software\/RISCAL\/."},{"key":"ref_14","first-page":"4","article-title":"Mathematical Model Checking Based on Semantics and SMT","volume":"16","author":"Schreiner","year":"2020","journal-title":"Trans. Internet Res."},{"key":"ref_15","unstructured":"Semtech (2020, July 15). Semantic Technologies for Computer Science Education. Available online: https:\/\/www3.risc.jku.at\/projects\/SemTech\/."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Nielson, H.R., and Nielson, F. (2007). Semantics with Applications: An Appetizer, Springer. Undergraduate Topics in Computer Science.","DOI":"10.1007\/978-1-84628-692-6"},{"key":"ref_17","unstructured":"Schreiner, W. (2017). The RISC Algorithm Language (RISCAL)\u2014Tutorial and Reference Manual (Version 1.0), RISC, Johannes Kepler University. Technical Report."},{"key":"ref_18","first-page":"248","article-title":"Validating Mathematical Theories and Algorithms with RISCAL","volume":"Volume 11006","author":"Rabe","year":"2018","journal-title":"Proceedings of the 11th Conference on Intelligent Computer Mathematics (CICM 2018), Hagenberg, Austria, 13\u201317 August 2018"},{"key":"ref_19","unstructured":"Schreiner, W., Brunhuemer, A., and F\u00fcrst, C. (2017, January 6). Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models. Proceedings of the Post-Proceedings ThEdu\u201917, Theorem Proving Components for Educational Software, Gothenburg, Sweden."},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Schreiner, W., Novitzk\u00e1, V., and Steingartner, W. (2019). A Categorical Semantics of Relational First-Order Logic, RISC, Johannes Kepler University. Technical Report.","DOI":"10.3390\/sym12101584"},{"key":"ref_21","unstructured":"Schreiner, W., and Steingartner, W. (2018). Visualizing Execution Traces in RISCAL, RISC, Johannes Kepler University. Technical Report."},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Steingartner, W., Eldojali, M.A.M., Radakovi\u0107, D., and Dost\u00e1l, J. (2017, January 14\u201316). Software support for course in Semantics of programming languages. Proceedings of the IEEE 14th International Scientific Conference on Informatics, Poprad, Slovakia.","DOI":"10.1109\/INFORMATICS.2017.8327275"},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"167","DOI":"10.17512\/STiCMM2017.11","article-title":"Categorical Semantics of Programming Langages","volume":"Volume 331","author":"Steingartner","year":"2017","journal-title":"Selected Topics in Contemporary Mathematical Modeling"},{"key":"ref_24","unstructured":"Steingartner, W., and Novitzk\u00e1, V. (2017, January 18\u201321). Learning tools in course on semantics of programming languages. Proceedings of the MMFT 2017\u2014Mathematical Modelling in Physics and Engineering, Poraj, Poland."},{"key":"ref_25","unstructured":"Schreiner, W., and Steingartner, W. (2018). Visualizing Logic Formula Evaluation in RISCAL, RISC, Johannes Kepler University. Technical Report."}],"container-title":["Symmetry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-8994\/12\/10\/1584\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T10:12:56Z","timestamp":1760177576000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-8994\/12\/10\/1584"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,23]]},"references-count":25,"journal-issue":{"issue":"10","published-online":{"date-parts":[[2020,10]]}},"alternative-id":["sym12101584"],"URL":"https:\/\/doi.org\/10.3390\/sym12101584","relation":{},"ISSN":["2073-8994"],"issn-type":[{"type":"electronic","value":"2073-8994"}],"subject":[],"published":{"date-parts":[[2020,9,23]]}}}