provability of a formula with occurrence of both types of quantifiers?

Question

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$

So:

$[(\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)]$

So:

$\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?

@MauroALLEGRANZA: Yes... I meant it... update to follow precise notation is applied. — , Feb 05 '17 at 19:53
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$. — Mauro ALLEGRANZA, Feb 05 '17 at 19:56
@MauroALLEGRANZA: So: $\vdash \Sigma \rightarrow \theta$ is not the same as $\Sigma \vdash \theta$? Right? — , Feb 05 '17 at 19:59
???? 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$. — Mauro ALLEGRANZA, Feb 05 '17 at 20:02

score 0 · Accepted Answer · answered Feb 05 '17 at 21:39

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

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? — , Feb 05 '17 at 22:15
Like this: http://math.stackexchange.com/questions/831751/interchange-quantifiers-using-the-generalization-theorem?rq=1 ? — , Feb 05 '17 at 22:33

1 Answers1