Orthogonality relation
From LLWiki
Revision as of 15:10, 30 September 2011 by PierreMarie Pédrot (Talk  contribs)
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.
Proposition
For any sets :
 If , then
