Coherent spaces

Question

In Proofs and Types, Girard discusses coherent (or coherence) spaces, which is defined as a set family which is closed downward ($a\in A,b\subseteq a\Rightarrow b\in A$), and binary complete (If $M\subseteq A$ and $\forall a_1,a_2\in M (a_1\cup a_2\in A)$, then $\cup M\in A$)

It was informally related to topological spaces. Anyway, I have a couple pretty general questions: Are they particularly useful outside of type theory? Perhaps more specifically, do coherent spaces show up in topology?

The last one raises up a philosophical question I've been pondering: Why is it that some structures seem to show up all over the place, while others that seem like they "should" be more or less equivalently useful don't seem to show up much at all? An example would be matroids versus topologies. I feel, morally, that matroids should be more useful than they seem to be.

The last question probably doesn't have any sort of solid answer, but it would be nice to hear some thought from people with a stronger background.

Cheers and thanks, Cory

Edit: After thinking about this some more, it has occurred to me that coherent spaces are a sort of "dual" to ultrafilters. I really don't have the background to be terribly formal, but, let me try to explain:

Let $(X,C)$ be a coherent space, and call the elements of $C$ "open" (I think the analogy is justified, because adding $X$ to $C$ makes it a topology), then the closed sets form an ultrafilter. The one problem is that the closure under intersection is a bit strong (the set of closed sets is closed under arbitrary intersections). On the other hand, if $(X,U)$ is an ultrafilter, the set of complements of open sets almost forms a coherent space-- but the conditions on unions is just a little too weak.

So, my next question is: Has this link been explored at all? Is there even anything there to explore?

Thanks again.

Answer 1

An analogue of your coherence spaces are used extensively in set theory, particularly with the method of forcing, the set-theoretic technique often used to prove statements independent of ZFC. But there is a variation, in that the coherence clause is weakened to cover only some M, such as M of a certain size.

For example, in the standard forcing argument to add κ many generic Cohen reals, one considers the partial order consisting of all finite partial functions from (ω x κ) to {0,1}. This collection of partial functions satisfies your properties, if we restrict to finite M, since the union of a set of partial functions is a function if and only if these functions are coherent, in the sense that any two of them agree. If F is a maximal filter on this partial order, then the union of F is a function fully from (ω x κ) to {0,1}. If the filter is what is known as V-generic, then the slices of this function adds κ many new Cohen reals. If κ is at least ω₂, then one can argue that CH fails in the resulting forcing extension.

Many forcing notions have the form of partial functions from one set to another, restricted by size or by other features, and so they also satisfy the corresponding restricted version of your Coherence space.