@techreport{RISC5900,author = {Wolfgang Schreiner and Valerie Novitzká and William Steingartner},
title = {{A Categorical Semantics of Relational First-Order Logic}},
language = {english},
abstract = {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.},
year = {2019},
month = {March},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {first-order logic, formal semantics, category theory, RISC Algorithm Language (RISCAL)},
sponsor = {OEAD WTZ project SK 14/2018 “SemTech — Semantic Technologies for Computer Science Education” and JKU LIT project LOGTECHEDU “Logic Technology for Computer Science Education”},
length = {34}
}