A Novel Categorical Approach to Semantics of Relational First-Order Logic

Symmetry

William Steingartner¹  Valerie Novitzká¹  Wolfgang Schreiner² 

[1] Faculty of Electrical Engineering and Informatics, Technical University of Košice, Letná 9, 042 00 Košice, Slovakia;Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Altenbergerstraße 69, A-4040 Linz, Austria;

关键词: category;    functor;    RISCAL;    relation;    relational first-order logic;    semantics;   

DOI  :  10.3390/sym12101584

来源: DOAJ

【 摘 要 】

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 “relational”. While the derived semantics is based on categorical principles, it is nevertheless “constructive” 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.

【 授权许可】

Unknown