Proof Sketch
A proof of the non-trivial direction of the theorem can be constructed according to the following steps:
- If the formula is valid, then by completeness of cut-free sequent calculus, which follows from Gentzen's cut-elimination theorem, there is a cut-free proof of .
- Starting from above downwards, remove the inferences that introduce existential quantifiers.
- Remove contraction-inferences on previously existentially quantified formulas, since the formulas (now with terms substituted for previously quantified variables) might not be identical anymore after the removal of the quantifier inferences.
- The removal of contractions accumulates all the relevant substitution instances of in the right side of the sequent, thus resulting in a proof of, from which the Herbrand disjunction can be obtained.
However, sequent calculus and cut-elimination were not known at the time of Herbrand's theorem, and Herbrand had to prove his theorem in a more complicated way.
Read more about this topic: Herbrand's Theorem
Famous quotes containing the words proof and/or sketch:
“If we view our children as stupid, naughty, disturbed, or guilty of their misdeeds, they will learn to behold themselves as foolish, faulty, or shameful specimens of humanity. They will regard us as judges from whom they wish to hide, and they will interpret everything we say as further proof of their unworthiness. If we view them as innocent, or at least merely ignorant, they will gain understanding from their experiences, and they will continue to regard us as wise partners.”
—Polly Berrien Berends (20th century)
“We criticize a man or a book most sharply when we sketch out their ideal.”
—Friedrich Nietzsche (1844–1900)