How to complete the follow natural deduction in bottom-up method

98 Views Asked by At

I'm confuse about how to proceed with the follow natural deduction. I'm following the bottom-up method. Any suggestion will be welcome, but I think it's almost finished.

hypotheses found: [∀x∃y ¬α(x, y)] , [∃x∀yα(x, y)] , [∀yα(x, y)]

____________________________
[∃x∀yα(x, y)]       ⊥
____________________________e∃
              ⊥
____________________________I¬
         ¬∃x∀yα(x, y)
____________________________I→
∀x∃y ¬α(x, y) → ¬∃x∀yα(x, y)
1

There are 1 best solutions below

0
On BEST ANSWER

What you did goes in the right direction!

Following up your attempt, you need to prove a contradiction $\bot$, and the way to prove a contradiction (thanks to the rule $\lnot_E$) is to prove both a formula $\varphi$ and its negation $\lnot \varphi$, using the hypotheses you have. In your hypotheses, you have $\forall y \,\alpha (x,y)$ and $\forall x \exists y \,\lnot \alpha(x,y)$, thus it would be enough to find a way to eliminate the quantifiers to make the contradiction $\alpha (x,y)$ and $\lnot \alpha (x,y)$ emerge.

Taking into account the informal idea above, a derivation in natural deduction for the formula $\forall x \exists y \, \lnot \alpha (x,y) \to \lnot \exists x \forall y \, \alpha (x,y)$ should have the following structure:

\begin{equation} \dfrac{[\exists x \forall y \, \alpha (x,y)]^\circ \qquad \dfrac{\overset{\vdots \, ?}{\lnot \alpha(x,y)} \qquad \dfrac{[\forall y \, \alpha(x,y)]^\bullet}{\alpha(x,y)}\forall_E}{\bot}\lnot_E }{\dfrac{\dfrac{\bot}{\lnot \exists x \forall y \, \alpha (x,y)}\lnot_I^\circ}{\forall x \exists y \, \lnot \alpha (x,y) \to \lnot \exists x \forall y \, \alpha (x,y)}\to_I^*}\exists_E^\bullet \end{equation}

Now a difficult arises: from the hypothesis $\forall x \exists y \, \lnot \alpha(x,y)$ you get (reading the derivation top-down) $\exists y \, \lnot \alpha(x,y)$ via the rule $\forall_E$, but from $\exists y \, \lnot \alpha(x,y)$ how can you get $\lnot \alpha(x,y)$? (See the vertical dots in the pseudo-derivation above.) The rule $\exists_E$ is a bit tricky, and it does not allow the variable $y$ to be free in its conclusion, so $\lnot \alpha (x,y)$ cannot be the conclusion of the rule $\exists_E$ we use to eliminate the existential quantifier from $\exists y \, \lnot \alpha(x,y)$. What can you do?

The solution is easy: you internalize the subderivation with conclusion $\bot$ (the conclusion of the rule $\lnot_E$ in the pseudo-derivation above) inside the subderivation we use to eliminate the existential quantifier from $\exists y \, \lnot \alpha(x,y)$. Therefore, a derivation in natural deduction for the formula $\forall x \exists y \, \lnot \alpha (x,y) \to \lnot \exists x \forall y \, \alpha (x,y)$ is the following:

\begin{equation} \dfrac { [\exists x \forall y \, \alpha (x,y)]^\circ \qquad \dfrac { \dfrac {[\forall x \exists y \, \lnot \alpha(x,y)]^*} {\exists y \, \lnot \alpha(x,y)} \forall_E \qquad \dfrac { [\lnot \alpha(x,y)]^\# \qquad \dfrac {[\forall y \, \alpha(x,y)]^\bullet} {\alpha(x,y)} \forall_E } {\bot} \lnot_E} {\bot} \exists_E^\# } { \dfrac { \dfrac {\bot} {\lnot \exists x \forall y \, \alpha (x,y)} \lnot_I^\circ } { \forall x \exists y \, \lnot \alpha (x,y) \to \lnot \exists x \forall y \, \alpha (x,y) } \to_I^* } \exists_E^\bullet \end{equation}

The symbols $*$, $\#$, $\circ$ and $\bullet$ mark when the hypotheses have been discharged.