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.

  • $\begingroup$ Ugh. Silly me; the pointwise complements form a filter, not an ultrafilter. $\endgroup$
    – Cory Knapp
    Nov 29, 2009 at 17:28
  • $\begingroup$ Hi Cory. So you posted this in 2009 and I don't know if you're still around. However, I wanted to ask if you know what the connection is between so-called coherence spaces and the coherent spaces of topology, which are precisely those spaces which can be realized as the spectrum of a ring and so are very interesting indeed. Also, having closed sets be closed under arbitrary intersection is not a problem. In fact, it is REQUIRED. It might be too strong if open sets were closed under arbitrary intersection. $\endgroup$ Feb 16, 2012 at 19:37

1 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 ω2, 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.

  • $\begingroup$ Thanks! That really informative, and gives me a place to look for them in the future. $\endgroup$
    – Cory Knapp
    Dec 10, 2009 at 6:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.