3
$\begingroup$

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

  • 0
    (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.2012-05-17
  • 0
    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$2012-05-17
  • 0
    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?2012-05-17
  • 0
    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).2012-05-17
  • 0
    I don't use natural deduction, but the sequent calculus.2012-05-17
  • 2
    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.2012-05-17
  • 0
    Thank you so far! But is $(x \leq a \wedge y \leq a \wedge z \leq a)$ true at all without the $\exists$? I don't think so. Because you could add $\forall x \forall y \forall z \forall a$ in front. Did I make an error in reasoning?2012-05-17
  • 0
    The reason why this cannot happen is that there are some restrictions on when you can introduce the universal quantifier which, if you write the argument down properly, will not be met.2012-05-17
  • 0
    Thanks again for your explanation. If you can move your comment(s) to the answer section, I should be able to accept your answer, I hope.2012-05-17
  • 0
    @Apostolos Could you please promote your answer from the comments as a real answer? That way, there will be one question less on the Unanswered list.2013-05-17

1 Answers 1