nLab
arrow structure

Arrow frames, arrow languages, arrow models and arrow logics

Idea

These structures are intended to allow one to talk about ‘all such objects as may be represented in a picture by arrows’, (Venema).

Arrow frames

Definition

An arrow frame is a frame, 𝔉=(W,C,R,I)\mathfrak{F} = (W, C, R, I ), such that CC is a ternary relation, (so CW×W×WC\subseteq W \times W \times W), RR is a binary relation, and II a unary one, so IWI\subseteq W.

Gloss

The interpretation intended for these relations is similar to the structure of a groupoid, but from a relational point of view.

  • For C(a,b,c)C(a,b,c) think a=bca = b\star c, ‘the’ composite of bb and cc, but, of course, aa need not be uniquely defined by this;

  • For R(a,b)R(a,b), think bb is a ‘reverse’ arrow for aa;

  • For I(a)I(a) i.e. aIa\in I, think aa is an ‘identity arrow’.

This defines a frame by a relational signature. It does not specify any formulae to be satisfied, nor is there a valuation around to give some ‘meaning’ to the structure.

Arrow languages

The arrow language follows the general form of the modal languages, but note that there are several ‘arities’ of relation in the structure, so we need several different types of modal operators.

Definition

The arrow language is defined by the rule

ϕ::=p¬ϕϕ 1ϕ 2ϕψϕ1,\phi ::= p \mid \bot \mid \neg \phi \mid \phi_1 \vee \phi_2 \mid \phi\circ \psi \mid \otimes\phi\mid 1',

where the pp are the propositional variables, as usual, and in addition

  • 11' is ‘identity’ and is a nullary modality or modal constant;

  • \otimes (an unfortunate notation, but which seems fairly standard in the sources used for this) is the ‘converse’ operator and is a ‘diamond’, i.e. a unary operator, and

  • \circ is the ‘composition operator’ and is a dyadic operator.

The possible interpretations or readings of these include

11' is SKIP;

ϕ\otimes \phi is phiphi conversely; and

ϕψ\phi\circ \psi is ‘first ϕ\phi then ψ\psi’.

Arrow models

The usual rules for modal semantics apply. An arrow model, 𝔐\mathfrak{M}, consists of an arrow frame, 𝔉=(W,C,R,I)\mathfrak{F} = (W, C, R, I ), (and a valuation VV, which plays a somewhat behind the scenes role in this general situation). In what follows, aWa\in W,

  • 𝔐,a1\mathfrak{M},a \models 1' if and only if IaIa;

  • 𝔐,aϕ\mathfrak{M},a \models \otimes\phi if and only if 𝔐,bϕ\mathfrak{M},b \models\phi for some bb with RabR a b;

  • 𝔐,aϕψ\mathfrak{M},a \models\phi\circ \psi if and only if 𝔐,bϕ\mathfrak{M},b \models\phi and 𝔐,cψ\mathfrak{M},c \models\psi for some b,cb,c with CabcC a b c.

References

A general treatment of these ideas can be found in

  • P. Blackburn, M. de Rijke and Y. Venema, Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53, 2001,

whilst a short introduction is

  • Y. Venema, A crash course in Arrow Logic, in: M Marx, L Pólos and M Masuch (editors), Arrow Logic and Multi-Modal Logic, Studies in Logic, Language and Information, CSLI Publications, Stanford (1996) 3–34.

Revised on December 24, 2010 07:47:12 by Toby Bartels (75.88.75.53)