Cut-Free FOL Proof

Question

I have a sequent that I’ve been puzzling over and was wondering if anyone can help me out.

I’m trying to prove ⊢∃x∀y(Fx->Fy). I’ve already been able to prove it using the Cut Rule, but I can’t seem to prove it without.

I used (Fx v ~Fx)⊢∃x∀y(Fx->Fy) and ⊢(Fx v ~Fx) to prove it with Cut.

I keep getting stuck without using the Cut Rule after doing ∀-Right and ∃-Right to get Fx->Fy. Any help would be appreciated.

Answer 1

As @peterwhy points out, this is the good old Drinker Paradox. You didn't tell us which specific sequent system you're using, but a variant of the following strategy should work in just about any common sequent calculus. Read it upside down, as you would a non-branching proof tree:

1.    $\vdash \exists x. \forall y. Fx \rightarrow Fy$ (conclusion)

2.    $\vdash \exists x. \forall y. Fx \rightarrow Fy, \forall y. Ft \rightarrow Fy$    (by $\exists R$ setting $x:= t$)

3.    $\vdash \exists x. \forall y. Fx \rightarrow Fy,\ Ft \rightarrow Fy$    (by $\forall R$)

4.    $\vdash \exists x. \forall z. Fx \rightarrow Fz,\ Ft \rightarrow Fy$    (by renaming the $\forall$-bound variable $y$ to $z$)

5.    $\vdash \forall z. Fy \rightarrow Fz,\ Ft \rightarrow Fy$    (by $\exists R$ setting $x := y$)

6.    $\vdash Fy \rightarrow Fz,\ Ft \rightarrow Fy$    (by $\forall R$)

7.    $Fy\vdash Fz,\ Ft \rightarrow Fy$ (by $\rightarrow R$)

8.    $Fy,\ Ft \vdash Fz,\ Fy$    (by $\rightarrow R$)

9.    $Fy,\ Ft \vdash Fz,\ Fy$    (by the axiom rule on $Fy$).

The key to this proof is that $(A \rightarrow C) \vee (C \rightarrow B)$ is a propositional tautology: we reduce the problem to an instance of this tautology by step 6.