Orthogonality relations are used pervasively throughout linear logic models, being often used to define somehow the duality operator .
Definition (Orthogonality relation)
Let A and B be two sets. An orthogonality relation on A and B is a binary relation . We say that and are orthogonal, and we note , whenever .
Let us now assume an orthogonality relation over A and B.
Definition (Orthogonal sets)
Let . We define its orthogonal set as .
Symmetrically, for any , we define .
Orthogonal sets define Galois connections and share many common properties.
For any sets :
- If , then