Prove $\forall z\left(\left(\exists xA\rightarrow A_{x}[z]\right)\rightarrow B\right)\vDash B$

Question

I'm doing some self-exercises on mathematical logic by myself and have come across this question which I can't seem to prove:

Let $A$ be a formula with a single free variable $x$. Let $B$ be a formula also, and $z$ be a variable that does not appear in $A$ or in $B$

Prove:

$\forall z\left(\left(\exists xA\rightarrow A_{x}[z]\right)\rightarrow B\right)\vDash B$

My train of thought was this: The meaning of $A \vDash B$ is that a structure that satisfies A also satisfies B: $M \vDash A \Rightarrow M \vDash B$

With that in mind, I started trying to understand what the meaning of $ C = (\exists xA\rightarrow A_{x}[z])$ was, and came to the conclusion that if said formula C is always $True$ then I would get the following:

$(True) \rightarrow B = \urcorner(True) \vee B = (False) \vee B $

And in this situation, for a structure to satisfy C it has to satisfy B thus proving the claim.

The thing is that I don't know (or know how to prove) if C is always $True$. It seems logical in a way, since if I am replacing all free occurrences of $x$ by $z$ (which does not appear in A) then A itself doesn't really change and so C will be $True$ depending if the structure satisfies A or not.

Is my train of thought OK? or am I missing something? Is there maybe another way of proving it?

Thank you to anyone who helps!

Answer 1

I suggest to work with Rob's comment above.

We have that :

$\vDash (∃xβ → α) ↔ ∀x(β → α)$, if $x$ does not occur free in $\alpha$.

Thus : $\forall z [(\exists x A(x) \rightarrow A(x/z)) \rightarrow B]$ is equivalent to : $\exists z (A(x) \rightarrow A(x/z)) \rightarrow B$.

We have also that :

$\vDash (α → ∃xβ) ↔ ∃x(α → β)$, if $x$ does not occur free in $\alpha$.

Thus : $\exists z (A(x) \rightarrow A(x/z))$ is equivalent to : $A(x) \rightarrow \exists z A(z)$.

In conclusion, our formula is equivalent to :

$(A(x) \rightarrow \exists z A(z)) \rightarrow B$

and the antecedent is valid.

We can now use the heuristic considerations above to prove it "semantically".

Consider a structure $\mathcal M$ such that $\mathcal M \vDash \forall z [(\exists x A(x) \rightarrow A(x/z)) \rightarrow B]$.

We have two cases : if $\mathcal M \vDash B$ we are done.

Assume insted that we have : $\mathcal M \nvDash B$; but then we must have that $(\exists x A(x) \rightarrow A(x/z))[d]$ must be falsified for all $d \in |\mathcal M|$, and this is impossible.

---

We can prove with Natural Deduction that :

$\forall z [(∃xA(x) \rightarrow A(z)) \rightarrow B] \vdash B$.

Proof :

1) $\forall z [(∃xA(x) \rightarrow A(z)) \rightarrow B]$ --- premise

2) $(∃xA(x) \rightarrow A(z)) \rightarrow B$ --- from 1) by $\forall$-elimination

3) $\lnot A(z)$ --- assumed [a]

4) $\forall x \lnot A(x)$ --- from 3) by $\forall$-introduction

5) $\lnot \exists x A(x)$ --- from 4) with : $\forall x \lnot A(x) \rightarrow \lnot \exists x A(x)$ by $\rightarrow$-elimination

6) $\exists x A(x)$ --- assumed [b]

7) $\bot$ --- from 5) and 6) by $\rightarrow$-elimination

8) $A(z)$ --- from 3) and 7) by Double Negation, discharging [a]

9) $\exists x A(x) \rightarrow A(z)$ --- from 6) and 8) by $\rightarrow$-introduction, discharging [b]

10) $B$ --- from 2) and 9) by $\rightarrow$-elimination.