Preservation theorems for Tarski's relation algebra

Abstract

We investigate a number of semantically defined fragments of Tarski's algebra of binary relations, including the function-preserving fragment. We address the question whether they are generated by a finite set of operations. We obtain several positive and negative results along these lines. Specifically, the homomorphism-safe fragment is finitely generated (both over finite and over arbitrary structures). The function-preserving fragment is not finitely generated (and, in fact, not expressible by any finite set of guarded second-order definable function-preserving operations). Similarly, the total-function-preserving fragment is not finitely generated (and, in fact, not expressible by any finite set of guarded second-order definable total-function-preserving operations). In contrast, the forward-looking function-preserving fragment is finitely generated by composition, intersection, antidomain, and preferential union. Similarly, the forward-and-backward-looking injective-function-preserving fragment is finitely generated by composition, intersection, antidomain, inverse, and an `injective union' operation.

Figures (2)

• Figure 1: Structure $C_m^\vee$
• Figure 2: Structure satisfying $\psi(a,a)$.

Theorems & Definitions (21)

• Theorem 1.1: vBenthem1998:bisimulation
• Theorem 2.1: Tarski1987:formalization
• Theorem 2.2: Tarski41:RALowenheim1915
• Theorem 3.1
• proof
• Theorem 4.1
• Lemma 4.2
• proof
• proof : Proof of Theorem \ref{['thm:main']}
• Theorem 4.3