Coherent space

From Wikipedia, the free encyclopedia

In proof theory, a coherent space is a concept introduced in the semantic study of linear logic.

Let a set C be given. Two subsets S,T ⊆ C are said to be orthogonal, written S ⊥ T, if S ∩ T is ∅ or a singleton. For a family of C-sets (i.e., F ⊆ ℘(C)), the dual of F, written F ^⊥, is defined as the set of all C-sets S such that for every T ∈ F, S ⊥ T. A coherent space F over C is a family C-sets for which F = (F ^⊥) ^⊥.

[edit] References

• Girard J-Y, Lafont Y, Taylor P, Proofs and types, Cambridge Press 1989
• Girard J-Y, Between logic and quantic: a tract, manuscript December 2003