Orthogonality relation

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$