Logical structures and genus of proofs

Any arbitrarily complicated non-oriented graph, that is a graph of arbitrarily large genus, can be encoded in a cut-free proof. This unpublished result of Statman was shown in the early seventies. We provide a proof of it, and of a number of other related facts.