What does "Wenn $x$ frei für $t$ in $\phi$" mean?

Question

The (German) text reads further

Wenn $x$ frei für $t$ in $\phi$, dann $$\vdash_L \forall x \phi \rightarrow \phi \frac{t}{x}$$

The für and in are confusing me. (I am looking for an explanation in either language, not a translation.)

Answer 1

It must be "$t$ is free for $x$ in $\phi$", meaning that $t$ is subsitutable in place of $x$ in $\phi$.

In the quantifier axiom:

$(∀x)B(x) \to B[t/x]$,

we need the proviso that the term $t$ is free for [or substitutable] $x$ in $B(x)$.

Substitutability is defined in order to avoid that, substituting a term $t$ with a variable inside (e.g. $y$) in place of $x$ into $\forall x B(x)$, the (free) occurrence of $y$ into $t$ will be "captured" by a quantifier $\forall y$ present into $B$.

Consider the following example:

$\forall x \exists y \ (x < y)$,

which is true in $\mathbb N$.

Here $B(x)$ is $\exists y \ (x < y)$ and, according to the definition, $y$ is not substitutable [is not free] for $x$ in $B$. Why ?

Because the result of the substitution would be:

$\exists y \ (y < y)$

which is clearly false.

Answer 2

We can only expand on the conditions that need to hold for a substitution as this:

For any variable $y$ that occurs in the expression $t$, the variable $x$ must not occur as free variable within the scope of some $\forall y$ or $\exists y$ in the formula $\phi$.

Here's an example why this peculiar restriction is necessary: The following a true statement of PA ("the theory of $\Bbb N$") $$ \forall x\;(x>0\to\exists y\;(y+1=x))$$ If we specialize by replacing $x$ with $7$ or with $0$ or with $2z+3$, all is fine: $$ 7>0\to\exists y\;(y+1=7)$$ $$ 0>0\to\exists y\;(y+1=0)$$ $$ 2z+3>0\to\exists y\;(y+1=2z+3)$$ However, if we replace $x$ with $y+2$, disaster happens $$ y+2>0\to \exists y\;(y+1=y+2)$$