  We try to bring to light some combinatorial structure underlying formal
proofs in logic. We do this through the study of the Craig Interpolation
Theorem which is properly a statement about the structure of formal
derivations. We show that there is a generalization of the interpolation
theorem to much more naive structures about sets, and then we show how both
classical and intuitionistic versions of the statement follow by interpreting
properly the set-theoretic language.
  The theorem we present is a geometrical formulation of the well-known logical
statement and gives sufficient conditions for a system of combinatorial nature
to enjoy interpolation. Its objects might be graphs just as well as formulas or
surfaces.
  The combinatorial mappings we use correspond whenever interpreted in a
logical language to the notion of `logical flow graph' (i.e. a graph tracing
the flow of occurrences of formulas in a proof; this notion has been introduced
in (Buss, 1991). The idea of using the flow of occurrences to study the
structure of proofs was already present in (Girard, 1987) with the concept of
`proof net'.)
