Arrow Logic

Origin. Venema and others developed arrow logic (1990s). Modal logic of transitions/arrows. Combines aspects of relation algebra and modal logic. Models binary relations as first-class objects. Foundation for dynamic semantics and process algebra connections.

Models. Logic where arrows are primitive. Standard modal: nodes with accessibility. Arrow logic: arrows/transitions are the objects. Arrows have source, target; can compose. Models processes, transitions, relations as entities.

Formalism.

Arrow frames: F = (W, C, R, I) where:

W: set of arrows
C ⊆ W³: composition (aCb,c = "a∘b = c")
R ⊆ W²: reversal (aRb = "a is converse of b")
I ⊆ W: identity arrows

Arrow models: M = (F, V) with V: Prop → P(W). Formulas describe sets of arrows.

Operators:

φ ⊗ ψ: there exist composable arrows a,b with a∈⟦φ⟧, b∈⟦ψ⟧, a∘b = current
φ⁻¹: converse arrows
ι: identity arrows
◇φ: "diamond" relation to φ-arrows

Semantics: M, a ⊨ φ ⊗ ψ iff ∃b,c. C(b,c,a) ∧ M,b ⊨ φ ∧ M,c ⊨ ψ M, a ⊨ φ⁻¹ iff ∃b. R(a,b) ∧ M,b ⊨ φ M, a ⊨ ι iff I(a)

Connection to relation algebra: Arrow logic is modal correspondent of relation algebra. Composition, converse, identity match RA operations.

Symbols.

Symbol	Unicode	Name	Meaning
⊗	U+2297	Circled times	Composition: the arrow splits into two composable arrows
⁻¹	—	Converse	The arrow reversed
ι	U+03B9	Greek small iota	Identity arrows
◇	U+25C7	White diamond	Some related arrow
□	U+25A1	White square / Box	All related arrows
∘	U+2218	Ring operator	Composition of arrows in the metalanguage
W	—	Universe	The set of arrows, taken as primitive objects
C	—	Composition	Ternary relation: C(b,c,a) means b∘c = a
R	—	Reversal	Binary relation pairing an arrow with its converse
I	—	Identity	The set of identity arrows
F, M	—	Frame, model	Arrow frame; arrow frame with a valuation
V	—	Valuation	Sends a proposition letter to a set of arrows
⟦ ⟧	U+27E6, U+27E7	Mathematical white square brackets	The set of arrows satisfying a formula
⊆	U+2286	Subset of or equal to	C ⊆ W³, R ⊆ W², I ⊆ W
∈	U+2208	Element of	Arrow belonging to the extension of a formula
∃	U+2203	There exists	Quantifier in the truth clauses
∧	U+2227	Logical and	Conjunction in the truth clauses
⊨	U+22A8	Satisfaction	Truth of a formula at an arrow
P(W)	—	Power set	Range of the valuation

Metatheory. Basic arrow logic over arbitrary arrow frames is finitely axiomatizable and decidable, and the reason is visible in the truth clauses: the composition clause quantifies under the atom C(b,c,a) and the converse clause under R(a,b), each of which contains every free variable of its scope, so the standard translation lands in the guarded fragment of first-order logic, decidable by Andréka, van Benthem and Németi (1998) and EXPTIME-complete at bounded arity by Grädel (1999). The decidability depends on not requiring composition to be associative or arrows to be actual pairs. Over square frames, where arrows are pairs and composition is genuine relational composition, arrow validity coincides with the equational theory of representable relation algebras, which Tarski proved undecidable and Monk (1964) proved not finitely axiomatizable; that theory is in turn the three-variable fragment of first-order logic, which fixes arrow logic's expressive ceiling.

Applies to. Process algebra semantics. Automata theory. Dynamic logic foundations. Relation-based reasoning. Category theory connections. Transition systems.

Limitations. The decidability comes from weakening the models rather than from a better algorithm: arrow frames need not be frames of actual binary relations, C need not be associative, and composites need be neither unique nor existent, so the complete axiomatization is complete for a class containing frames that no relation algebra represents. Insisting on the intended pair frames restores associativity and immediately loses both decidability and finite axiomatizability, and there is no middle class known to be both natural and well behaved — this is the representation problem of relation algebra, inherited whole. Being a modal language, arrow logic is invariant under arrow bisimulation, so it cannot count arrows, express cardinality, or distinguish frames that bisimulation identifies. And what it does express is confined to the three-variable fragment, which excludes ordinary relational conditions whose statement needs four variables.