Proof in the sequent calculus

I have to prove the following in the sequent calculus:

Given

(a) $\forall x: x \leq x$

(b) $\forall x \forall y \forall z [(x \leq y \wedge y \leq z) \rightarrow x \leq z]$

(c) $\forall x \forall y \exists z [x \leq z \wedge y \leq z]$

$\Gamma := \{(a), (b), (c)\}$

Show that: $\Gamma \vdash \forall x \forall y \forall z \exists w [x \leq w \wedge y \leq w \wedge z \leq w]$

(Common rules like $\forall$-introduction and elimination and $\exists$-introduction and elimination ... etc. can be used)

I know how to prove it intuitively, (with (a) and (c), (b) is not necessary if I am not mistaken), but I have no idea for a formal proof.

Basically it should work if I got to

$\exists w [ x \leq w \wedge y \leq w \wedge z \leq w ]$

(Then I could use 3* $\forall$-introduction)

Can anyone give me a hint?

P.S.: If I eliminate the $\forall$'s:

(a) $x \leq x$

(b) $(x \leq y \wedge y \leq z) \rightarrow x \leq z$

(c) $\exists z [x \leq z \wedge y \leq z]$

-
(b) is needed. Otherwise take the relation on $3$: $\{(0,0),(1,1),(2,2),(3,3),(0,1),(1,2),(2,0)\}$. There is no element above or equal to $0,1,2$. Rethink your intuitive proof. First eliminate the universal quantifiers. You will end up with various existential sentences. Eliminate one by one the existential quantifiers to reach a conclusion with an new existential quantifier. – Apostolos May 17 '12 at 18:30
but your relation does not satisfy (c), because for $x=2$ and $y=3$ there is no $z$ s.t. $x \leq z$ and $y \leq z$ – ChristianL May 17 '12 at 18:50
Disregard $(3,3)$, that's not supposed to be there. So the relation is actually $\{(0,0),(1,1),(2,2),(0,1),(1,2),(2,0)\}$ and the domain is $3=\{0,1,2\}$. Is your system natural deduction? – Apostolos May 17 '12 at 19:11
Ok, I got that, thank you. But I still don't know how I can "reach a conclusion with an new existential quantifier", because I don't know how to get the required (additional) $z \leq w$ into the (substituted) $\exists$-statement of (c). – ChristianL May 17 '12 at 19:20
First of all you have that $\exists w(x\leq w\land y\leq w)$ and you have $\exists u(y\leq u\land z\leq u)$ and $\exists a(u\leq a\land w\leq a)$. These are direct implications of the third axiom. Now using we have that $(x\leq a\land y\leq a\land z\leq a)$ implied by the second axiom and $(x\leq w\land y\leq w)$, $(y\leq u\land z\leq u)$, $(u\leq a\land w\leq a)$ (you get these by eliminating the existential quantifiers). Then introduce an existential quantifier $\exists a(x\leq a\land y\leq a\land z\leq a)$. Then introduce the universal quantifiers. This is a sketch of the argument. – Apostolos May 17 '12 at 19:27

I'll formalize Apostolos' argument with Natural Deduction in "sequent-calculus-style" [see Dirk van Dalen, Logic and Structure, (5th ed - 2013), pages 35, 88 and 91 for the rules].

These are the rules for quantifiers :

$$(\forall I) \, \, {\Gamma \vdash \varphi(x) \over \Gamma \vdash \forall x \varphi(x)}\ x \notin FV(\psi) \, \text{for all} \,\, \psi \in \Gamma$$

$$(\forall E) \, \, {\Gamma \vdash \forall x \varphi(x) \over \Gamma \vdash \varphi(t)}\ t \, \text{free for} \, x \, \text{in} \,\, \varphi$$

$$(\exists I) \, \, {\Gamma \vdash \varphi(t) \over \Gamma \vdash \exists x \varphi(x)}\ t \, \text{free for} \, x \, \text{in} \,\, \varphi$$

$$(\exists E) \, \, {\Gamma, \varphi(x) \vdash \psi \over \Gamma, \exists x \varphi(x) \vdash \psi}\ x \notin FV(\psi) \, \text{and} \, x \notin FV(\gamma) \,\, \text{for all} \,\, \gamma \in \Gamma$$

Proof

From the rule of assumption [i.e. $\Gamma \vdash \varphi$, if $\varphi \in \Gamma$] applied to axiom (c) we derive, following Apostolos' proof, by multiple applications of ($\forall$ E) :

(1) $\Gamma \vdash ∃w(x≤w∧y≤w)$

(2) $\Gamma \vdash ∃u(y≤u∧z≤u)$

(3) $\Gamma \vdash ∃a(u≤a∧w≤a)$

(4) $\Gamma \vdash x \le w$ --- from (1) by ($\land$ E) and ($\exists$ E)

Note :

By ($\land$ E) we have :

$$\Gamma \vdash x≤w∧y≤w \over \Gamma \vdash x≤w$$

Applying "weakening" [i.e.if $\Gamma \vdash \varphi$, then $\Gamma \cup \Delta \vdash \varphi$], we get :

$$\Gamma \vdash x≤w∧y≤w \over \Gamma, x≤w∧y≤w \vdash x≤w$$

Thus, by ($\exists$ E) we have :

$$\Gamma \vdash x≤w∧y≤w \over \Gamma, ∃w(x≤w∧y≤w) \vdash x≤w$$

But by (1) : $\Gamma \vdash ∃w(x≤w∧y≤w)$, we conclude (4) : $\Gamma \vdash x≤w$.

end note.

In the same way, we have :

(5) $\Gamma \vdash w \le a$ --- from (3)

Thus :

(6) $\Gamma \vdash x \le w \land w \le a$ --- from (4) and (5) by ($\land$ I).

(7) $\Gamma \vdash x \le a$ --- from axiom (b) with multiple applications of ($\forall$ E) and (6) and ($\rightarrow$ E).

Repeating the "procedure" (4)-(7) with $y \le w$ (from (1)) and again with $z \le u$ (from (2)) we get :

(8) $\Gamma \vdash y \le a$

(9) $\Gamma \vdash z \le a$.

Now we apply ($\land$ I) twice with (7), (8) and (9) to get :

(10) $\Gamma \vdash (x \le a \land y \le a) \land z \le a$.

Thus by ($\exists$ I) :

(11) $\Gamma \vdash \exists w(x \le w \land y \le w) \land z \le w$

and finally, by multiple applications of ($\forall$ I) :

(12) $\Gamma \vdash \forall x \forall y \forall z \exists w[(x \le w \land y \le w) \land z \le w]$.

-