View source for Orthogonality relation

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

{{Definition|title=Orthogonality relation|Let <math>A</math> and <math>B</math> be two sets. An '''orthogonality relation''' on <math>A</math> and <math>B</math> is a binary relation <math>\mathcal{R}\subseteq A\times B</math>. We say that <math>a\in A</math> and <math>b\in B</math> are '''orthogonal''', and we note <math>a\perp b</math>, whenever <math>(a, b)\in\mathcal{R}</math>.}}

Let us now assume an orthogonality relation over <math>A</math> and <math>B</math>.

{{Definition|title=Orthogonal sets|Let <math>\alpha\subseteq A</math>. We define its orthogonal set <math>\alpha\orth</math> as <math>\alpha\orth:=\{b\in B \mid \forall a\in \alpha, a\perp b\}</math>.

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

Orthogonal sets define Galois connections and share many common properties.

{{Proposition|For any sets <math>\alpha, \alpha'\subseteq A</math>:

* <math>\alpha\subseteq \alpha\biorth</math>
* If <math>\alpha\subseteq\alpha'</math>, then <math>{\alpha'}\orth\subseteq\alpha\orth</math>
* <math>\alpha\triorth = \alpha\orth</math>
}}