Almost a decade ago, Girard invented linear logic with the
notion of a proof-net. Proof-nets
are special graphs built from formulas, links and boxes.
However, not all nets are proof-nets.
First, they must be well constructed (we say that such graphs are proof-structures).
Second,
a proof-net is a proof-structure that corresponds to a sequential proof.
It must satisfy a
correctness criterion. One may wonder what this static criterion means
for cut-elimination.
We prove that every incorrect proof-structure (without cut) can be put
in an environment
where reductions lead to two kinds of basically wrong configurations: deadlocks
and
disconnected proof-structures. Thus, this proof says that there does not
exist a bigger class
of proof-structures than proof-nets where normalization does not lead to
obviously bad
configurations.