In the system QS we have the following axiom
$$(A \to \forall vA)$$ if $v$ does not occur free in $A$.
This more or less feels intuitive however the explanation given in the text is confusing me. The text is Metalogic by Hunter (page 167).
The reason for the restriction on this axiom is that without it we should have the following formula, for example, as an axiom:
$$Fx_1 \to \forall x_1 Fx_1$$
That formula is not logically valid. (Take the domain $D$ as the set of natural numbers and $'F'$ as 'is even'. Then the sequence $\langle 2,2,2,\ldots \rangle$, for example, does not satisfy the formula.
The issue I have is.... I'm not sure why the sequence does not satisfy the formula. Is $x_1$ a sequence or the first element of the sequence. If the latter then clearly $2$ is even but not just any number is even, obviously. If the former, then in what sense is a sequence 'even'. Well.... I clearly don't understand what's going on, because this should be straight forward. Thanks for any clarification!
Why the formula $Fx_1 → ∀x_1Fx_1$ is not valid ?
Valid means: true in every interpretation with every variable assignment.
Consider the following interpretation; domain $\mathbb N$ and the predicate $Fx$ interpreted as "$x$ is even".
The sequnce $s = \langle 2,2,\dots \rangle$ satisfies $Fx_1$, because it assigns the value $2$ to $x_1$, and $2$ is even, but it does not satisfies $∀x_1Fx_1$.
This is so [see page 147] because not every sequence differing from $s$ at most for the value assigned to $x_1$ satisfies $Fx_1$: consider the sequence $s'= \langle 3,2,\dots \rangle$.
In conclusion, we have found an interpretation and a variable assignment such that the antecedent of the formula is true while the consequent is false, and thus such that the formula is false.
Obviously, we want that the logical axiom schema produce only valid instances; this is the reason for the restriction on $x$ not being free in axiom schema: