Cut-Free FOL Proof 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.
 A: 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:

*

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


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


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


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


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


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


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


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


*   $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.
