is the following a derived rule of our logic? $A\to B \vdash (\exists x)A\to B$, provided $x$ is not free in $B$? I'm working through Ex 3 of Section 8.3 of Mathematical Logic by G.Tourlakis, page 208:
Is the following schema a derived rule of our logic? $A\to B \vdash (\exists x)A\to B$, provided $x$ is not free in $B$?
I wanted to validate my reason as to why not:
Consider the above rule:
$$A\to B\vdash (\exists x) A\to B$$
$\Leftrightarrow$ (Definition of $\exists$)
$$A\to B\vdash \lnot(\forall x) \lnot A\to B$$
$\Leftrightarrow $ (Tautological implication $\vdash p\to q\equiv \lnot q \to \lnot p$)
$$\lnot B \to \lnot A\vdash \lnot B \to \lnot\lnot(\forall x) \lnot A$$
$\Leftrightarrow $ (Deducation Theorem)
$$\lnot B, \lnot A\vdash \lnot\lnot(\forall x) \lnot A$$
$\Leftrightarrow $ (Double Negation)
$$\lnot B, \lnot A\vdash (\forall x) \lnot A$$
Need to show "Strong Generalization": $A\vdash (\forall x)A$
Proof - Hilbert style
(1) $\lnot A$ (premise)
(2) $\top \to \lnot A$ (1 with Tautology $\vdash \lnot A \equiv (\top \to \lnot A)$, and Eqn)
(3) $\top \to (\forall x)\lnot A$ (2 with rule stated above: $\lnot A\vdash (\forall x)\lnot A$)
(4) $(\forall x)\lnot A$ (3 with Tautology used in 3 $\vdash (\forall x)\lnot A \equiv (\top \to(\forall x)\lnot A) $)
Therefore we have "Strong Generalization" $A\vdash (\forall x)A$ with "$A$-part" as $\lnot A$.
 A: The rule is not valid in Tourlakis' system.
The purported rule is the "dual" of that of Ex.8.3.2 and the reason is the same.
Consider e.g.

$0=0 \to x=0 \vdash 0=0 \to (\forall x)(x=0)$

and interpret it in $\mathbb N$.
We have that $\nvDash_{\mathbb N} (0=0 \to x=0) \to (0=0 \to (\forall x)(x=0))$ because in this interpretation the antecedent is True for some possible value of $x$ while the consequent is False [compare with Example 8.1.7, page 200].
This sows that, also if the proviso : $x$ is not free in $A$ is satisfied, we have : $A \to B \nvDash A \to (\forall x)B$, and thus - by Soundness of the calculus - we have :

$A \to B \nvdash A \to (\forall x)B$.

In the same way :

$A \to B \nvdash (\exists x)A \to B$.


Compare with the valid rule of Coroll.6.5.5 [page 179] :

If $x$ does not occur free either in $\Gamma$ or in $B$, then $\Gamma \vdash A \to B \text {  iff  } \Gamma \vdash (\exists x) A \to B$.

The reason is with the semantical specifications [page 196] for formulas with free variables :

An interpretation $\mathfrak D$ gives meaning to all nonlogical symbols of the alphabet as follows :

(1) For each free variable $x$, $x^{\mathfrak D}$ is some member of [the domain] $D$.


And [page 201] :

If $A^{\mathfrak D}= \text t$, for some [formula] $A$ and $\mathfrak D$, we will say that $A$ is true in the interpretation $\mathfrak D$ or that $\mathfrak D$ is a model of $A$.


As the text suggests, if the above rule for $\forall$ would be valid, we can use it to prove the invalid [page 147] : $\dfrac {A}{(\forall x) A}$.
