Is (∀)(∀) (¬ = ∨ = ) → (∀)(¬ = ∨ = ) an instance of (∀x)A → A[x:=t]?

Question

"(∀x)A → A[x:=t]" means "If a statement A is true for all x, then it must be true of any special value t that we are allowed to plug into x."

Answer 1

No, because the substitution in $A[x:=t]$ must avoid variable captures.

Different textbooks differ in exactly how they formalize this rule. (There are even some that just wave their hands apologetically and say not much more than I did here).

One fairly simple way to implement it is that you can't do $$ \bigl[ \forall x(\cdots)\bigr] [y:=t] $$ if $x$ appears in $t$ without first renaming the dummy variable $x$ in the quantifier. In that case if you want to apply your rule to the case in the question title you would get $$ \bigl[\forall x(x\ne y \lor x=y)\bigr][y:=x] \quad\equiv\quad \forall z(z\ne x \lor z=x)$$ because we first rename the dummy variable $x$ to $z$ before we can substitute the term $x$ in. This would give you the instance $$ \forall y \forall x (x\ne y \lor x=y) \to \forall z(z\ne x \lor z=x) $$ which is certainly true enough.

You could get $\forall x(x\ne x\lor x=x)$ from the conclusion of this by now instantiating $z$ to $x$, and then applying universal generalization to $x\ne x\lor x=x$.

The availability of this small detour can make it seem like the rule against variable capture is toothless in the first place, but it only works because the $\forall z$ (which was the original $\forall x$) is the top-level logical construction of the formula. If it was deeper in the structure of the formula -- say, beneath a bunch of $\to$ or $\neg$, then we couldn't just instantiate it and then re-generalize.