Coherent space

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

For coherent spaces in topology, see spectral space.

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. The dual of a family F ⊆ ℘(C) is the family F ^⊥ of all subsets S ⊆ C orthogonal to every member of F, i.e., such that S ⊥ T for all T ∈ F. A coherent space F over C is a family of C-subsets for which F = (F ^⊥) ^⊥.

In Proofs and Types coherent spaces are called coherence spaces. A footnote explains that although in the French original they were espaces cohérents, the coherence space translation was used because spectral spaces are sometimes called coherent spaces.

References

• Girard, J.-Y.; Lafont, Y.; Taylor, P. (1989), Proofs and types (PDF), Cambridge University Press.
• Girard, J.-Y. (2004), "Between logic and quantic: a tract", in Ehrhard; Girard; Ruet; et al. (eds.), Linear logic in computer science (PDF), Cambridge University Press.
• Johnstone, Peter (1982), "II.3 Coherent locales", Stone Spaces, Cambridge University Press, pp. 62–69, ISBN 978-0-521-33779-3.