Prove the formula $(\exists x A(x) \to B) \to \forall y (A(y) \to B)$

Question

I need to prove the following formula $$(\exists x A(x) \to B) \to \forall y (A(y) \to B)$$ Where $y\notin \mbox{free}(A)$ and $y\notin \mbox{free}(B)$

Axioms that I use.

1. $A \to (B \to A)$

2. $(A \to B) \to ( (A \to (B \to C)) \to (A \to C))$

3. $(\lnot B \to A) \to ((\lnot B \to \lnot A) \to B)$

4. $\forall x_i A(x_i) \to A(t)$ where $A$ is wf and $t$ is free for $x_i$ in $A$

5. $\forall (x_i) (A \to B) \to (A \to \forall x_i B)$ where $x_i$ is not bounded in $B$

Rules of inferences are Gen and Modus Ponens.

Here's my try.

$1. \vdash \lnot \forall x \lnot A(x)$ (premise)

$2. \vdash \lnot \forall x \lnot A(x) \to B $ (premise)

$3. \vdash B$ (1 and 2 m.p.)

Lemma 0: $ \lnot \forall x \lnot A(x) \vdash A(t)$

Suppose that

$1. \lnot \forall x \lnot A(x), \lnot A(t) \vdash \lnot A(t)$ (premise)

$2. \vdash \forall x \lnot A(x)$ (Gen 1.)

$3. \vdash \lnot \forall x \lnot A(x)$ (premise)

Contradiction. So

$4. \lnot \forall x \lnot A(x) \vdash A(t)$

End of Lemma 0

$5. \vdash A(t)$ (1. and Lemma 0)

$6. \vdash (B \to (A(t) \to B))$ (A1)

$7. \vdash A(t) \to B$ (3 and 6 m.p.)

$8. \vdash \forall y (A(y) \to B$) (Gen 7.)

$9. \vdash (\lnot \forall x \lnot A(x) \to B) \to \forall y (A(y) \to B$) (Deduction theorem)

But I think I left an error in the step 7. Everything below that is true, only if $\lnot \forall x \lnot A(x)$ is true.

Maybe there's an easier way?

P.S: $\exists$ is an abbreviation for: $\lnot \forall \lnot$ (Thanks to @MauroALLEGRANZA)

Answer 1

Lines 8 and 9 are fine ... but your Lemma is not. What you need to show is $A(t) \vdash \neg \forall x \neg A(x)$, so that together with $\neg \forall x \neg A(x) \rightarrow B$ you can get $A(t) \rightarrow B$ and then apply 8 and 9.

Also, while I don't know the exact notation of your system, I find the way you introduce premises suspect. For example, you write:

$1. \vdash \lnot \forall x \lnot A(x)$ (premise)

Given the $\vdash$, that looks like a theorem, not a premise. I would suspect that something like:

$1. \lnot \forall x \lnot A(x) \vdash \lnot \forall x \lnot A(x)$ (premise)

or simply

$1. \lnot \forall x \lnot A(x) $ (premise)

would be called for.