Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I have to prove the following in the sequent calculus:


(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]$

share|cite|improve this question
(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$$


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

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.