Orthogonality relation

From LLWiki
Jump to: navigation, search

Orthogonality relations are used pervasively throughout linear logic models, being often used to define somehow the duality operator (-)\orth.

Definition (Orthogonality relation)

Let A and B be two sets. An orthogonality relation on A and B is a binary relation \mathcal{R}\subseteq A\times B. We say that a\in A and b\in B are orthogonal, and we note a\perp b, whenever (a, b)\in\mathcal{R}.

Let us now assume an orthogonality relation over A and B.

Definition (Orthogonal sets)

Let \alpha\subseteq A. We define its orthogonal set \alpha\orth as \alpha\orth:=\{b\in B \mid \forall a\in \alpha, a\perp b\}.

Symmetrically, for any \beta\subseteq B, we define \beta\orth:=\{a\in A \mid \forall b\in \beta, a\perp b\}.

Orthogonal sets define Galois connections and share many common properties.

Proposition

For any sets \alpha, \alpha'\subseteq A:

  • \alpha\subseteq \alpha\biorth
  • If \alpha\subseteq\alpha', then {\alpha'}\orth\subseteq\alpha\orth
  • \alpha\triorth = \alpha\orth
Personal tools