Describing proofs by short tautologies (Q1023053)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Describing proofs by short tautologies |
scientific article |
Statements
Describing proofs by short tautologies (English)
0 references
10 June 2009
0 references
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\).
0 references
proof theory
0 references
Herbrand's theorem
0 references
cut-elimination
0 references