# Thread: Help with using Herbrand's Theorem

1. ## Help with using Herbrand's Theorem

I need to prove using Herbrand's Theorem the following. I've tried in a few directions (and solved a few other problems using the theorem), but can't solve this one.

Any directions will be greatly appreciated!

2. Just reproducing the theorem in a larger size:

$(\forall x)(x=0)\vee(\exists y)(x=s(y))$
$\vdash(\forall x)((x=0)\vee(x=s(0))\vee(\exists y)(x=s(s(y))))$.

Is that correct?

Question: does the initial for all x apply to the entire disjunct before the $\vdash$ symbol?

I'm afraid I can't be of much more use than this. Herbrand's theorem is beyond what I've done in logic.

3. ## Fixed question

$(\forall x) ((x=0)\vee(\exists y)(x=s(y)))$

$\vdash (\forall x) ((x=0)\vee(x=s(0))\vee(\exists y)(x=s(s(y))))$

Thanks for noting the problem

4. When you say "use Herbrand's theorem" do you mean that you need to perform this proof in some particular kind of sequent calculus?

Otherwise, in ordinary natural deduction, a proof is easy:

Suppose x is not 0 nor the successor of 0. Then there is a z such that x is the successor of z. But such z is itself either 0 or a successor. But z can't be 0, since x is not the successor of 0. So let z be the successor of y. So x is the successor of the successor of y. Then fill out the routine quantifer and sentential logic steps to complete the proof.