  We uncover a close relationship between combinatorial and syntactic proofs
for first-order logic (without equality). Whereas syntactic proofs are
formalized in a deductive proof system based on inference rules, a
combinatorial proof is a syntax-free presentation of a proof that is
independent from any set of inference rules. We show that the two proof
representations are related via a deep inference decomposition theorem that
establishes a new kind of normal form for syntactic proofs. This yields (a) a
simple proof of soundness and completeness for first-order combinatorial
proofs, and (b) a full completeness theorem: every combinatorial proof is the
image of a syntactic proof.
