Hilbert style: $\vdash\lnot\forall xB\to\exists x \lnot B$

Question

Prove $\vdash\lnot\forall xB\to\exists x \lnot B$

Knowing this $\exists xB(x)\iff\lnot\forall x\lnot B(x)$ as definition, using Modus ponens and Generalization rule.

Proof

$\lnot\forall xB\iff\exists x\lnot B$ therefore $\lnot\forall xB\to\exists x \lnot B$

Is the proof correct?

Answer 1

In order to prove something with Mendelson's system, you have to re-use previous proved results.

You need Lemma 1.11 (a) [ page 31 ]: $\vdash \lnot \lnot \mathcal B \to \mathcal B$, as well as Lemma 1.11 (e) : $\vdash (\mathcal B \to \mathcal C) \to (\lnot \mathcal C \to \lnot \mathcal B)$.

Proof sketch:

1) $\vdash \lnot \lnot \mathcal B \to \mathcal B$ --- Lemma 1.11 (b)

2) $\vdash \forall x \ (\lnot \lnot \mathcal B \to \mathcal B)$ --- from 1) by Gen

3) $\vdash \forall x \lnot \lnot \mathcal B \to \forall x \mathcal B$ --- from 2) by Ex.2.27 (a) [ page 73 ]: $\vdash \forall x \ (\mathcal B \to \mathcal C) \to (\forall x \mathcal B \to \forall x \mathcal C)$ and MP

4) $\vdash \lnot \forall x \mathcal B \to \lnot \forall x \lnot \lnot \mathcal B$ --- from 3) and Lemma 1.11 (e) by MP

5) $\vdash \lnot \forall x \mathcal B \to \exists \lnot \mathcal B$ --- from 4) and abbreviation.