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

Question

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

Answer 1

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