Proof Systems in Relation Algebra
Lev Gordeev · Studies in fuzziness and soft computing · 2001
We expose two different notions of validity in relation algebras: one is based on Tarski’s equational calculus (say, ‘T-validity’), and the other arises by the canonical 1-order translation from the ordinary semantic validity (say, ‘t-validity’). In the first section we characterize both validities via provability in finite-variable logics and the corresponding cutfree derivability in formula-rewriting 1-order systems. In the second section we characterize T-validity via derivability in a suitable cutfree term-rewriting system in the basic algebraic language, which is equivalent to the algebraic display calculus of Gore. In the third section we address 1-order 2-variable decidability and validity using both methods.