Describing proofs by short tautologies (Q1023053)

It is well-known that the size of Herbrand disjunction is super-exponential in the size of a proof (with cut or modus ponens). The author provides an elegant construction of a short propositional tautology similar to Herbrand disjunction and completely encoding a given proof. Assuming that a proved formula \(F\) as well as every cut formula in the proof is prenex, take all quantifier-free instances \(F_1,\ldots,F_k\) of \(F\) in the given proof, all quantifier-free instances \(C_1,\ldots,C_l\) of antecedent cut formulas and all quantifier-free instances \(D_1,\ldots,D_m\) of succedent cut formulas. The implication \((\bigvee_{i\leq l}C_i\rightarrow \&_{j\leq m}D_j)\rightarrow F_1\vee\ldots\vee F_k\) is proved by a quantifier-free derivation which encodes the previous derivation of \(F\).