I'm gonna study following lemma:

$\Sigma \vdash \theta \Longleftrightarrow \Sigma \cup \{\neg \theta\} \vdash \perp$, where $\perp$ is a always-false sentence.

In example 1:

$\vdash[(\forall x)P(x)] \rightarrow [(\exists x)P(x)]$

We're gonna show:

$[(\forall x)P(x)] \vee \neg [(\exists x)P(x)] \vdash \perp$


$[(\forall x)P(x)] \vee \neg[(\exists x)P(x)] \vdash \perp$

$[(\forall x)P(x)] \vee [(\forall x) \neg P(x)] \vdash \perp$

$(\forall x)[P(x) \vee \neg P(x)] \vdash \perp$

$True \vdash \perp$

As $True \rightarrow False$ is false!...

And the problem's raised from example 2:

If I'm gonna show:

$[(\forall x)(\forall y)P(x,y)] \vdash [(\forall y)(\forall z)P(z,y)]$

It's the same as:

$\vdash [(\forall x)(\forall y)P(x,y)] \rightarrow [(\forall y)(\forall z)P(z,y)]$


$\vdash [(\forall x)(\forall y)P(x,y)] \vee \neg [(\forall y)(\forall z)P(z,y)]$

$\vdash [(\forall x)(\forall y)P(x,y)] \vee [(\exists y)(\exists z) \neg P(z,y)]$

I'm stuck here...

So, I'm using the lemma wrong. What's wrong with my utilization?

  • $\begingroup$ @MauroALLEGRANZA: Yes... I meant it... update to follow precise notation is applied. $\endgroup$ – Roboticist Feb 5 '17 at 19:53
  • $\begingroup$ And $\text {True} \to \text {False}$ is false. $\endgroup$ – Mauro ALLEGRANZA Feb 5 '17 at 19:53
  • $\begingroup$ If you want to show $\vdash (∀x)P(x) \to (∃x)P(x)$ you have to consider its negation : $\lnot [(∀x)P(x) \to (∃x)P(x)]$ and show that it implies $\bot$. $\endgroup$ – Mauro ALLEGRANZA Feb 5 '17 at 19:56
  • $\begingroup$ @MauroALLEGRANZA: So: $\vdash \Sigma \rightarrow \theta$ is not the same as $\Sigma \vdash \theta$? Right? $\endgroup$ – Roboticist Feb 5 '17 at 19:59
  • $\begingroup$ ???? Example 1) First line : Ok. Second line, it must be : $¬[(∀x)P(x)→(∃x)P(x)] \vdash \bot$ i.e. $¬[¬(∀x)P(x) ∨ (∃x)P(x)] \vdash \bot$. $\endgroup$ – Mauro ALLEGRANZA Feb 5 '17 at 20:02

Let's start from scratch...

We want to use the meta-theorem:

$Σ ⊢ θ$ iff $Σ ∪ \{ ¬θ \} \vdash \bot$,

to prove that : $\vdash (∀x)P(x) → (∃x)P(x)$.

Thus, we can apply the above lemma with $\Sigma = \emptyset$, and we have to prove that:

$\lnot [ (∀x)P(x) → (∃x)P(x) ] \vdash \bot$.

That is : $(∀x)P(x) \land \lnot (∃x)P(x) \vdash \bot$.

This is quite intuitive: we cannot satisfy simultaneously $(∀x)P(x)$ and $\lnot (∃x)P(x)$.

But in order to establish a derivability relation, we have to use some proof system, like Natural Deduction:

1) $(∀x)P(x) \land \lnot (∃x)P(x)$ --- premise

2) $\lnot (∃x)P(x)$ --- from 1) by $\land$-elim

3) $(∀x)P(x)$ --- from 1) by $\land$-elim

4) $P(a)$ --- from 3) by $\forall$-elim

5) $(∃x)P(x)$ --- from 4) by $\exists$-intro

$\bot$ --- from 2) and 5).

Conclusion: we have used a complex detour to derive a very simple result.

From 3) and 5) above we can directly conclude with: $(∀x)P(x) \vdash (∃x)P(x)$ and thus, by $\to$-intro, we get:

$\vdash (∀x)P(x) \to (∃x)P(x)$.

  • $\begingroup$ Thanks a bunch. So, to handle the second example, I should use that quantifier elimination technique (like yours) and generate them again, deductively, under new variables from $x$ and $y$ to $y$ and $z$. Is it correct? $\endgroup$ – Roboticist Feb 5 '17 at 22:15
  • $\begingroup$ Like this: math.stackexchange.com/questions/831751/… ? $\endgroup$ – Roboticist Feb 5 '17 at 22:33
  • $\begingroup$ @Roboticist - Exactly. $\endgroup$ – Mauro ALLEGRANZA Feb 6 '17 at 7:33
  • $\begingroup$ I much appreciate for your help... $\endgroup$ – Roboticist Feb 6 '17 at 7:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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