lo.logic - Does the axiom of specification prevent writing any proof?

I think with such problems it helps to make it clear what the syntactical rules actually "mean". The rule you mention sais that - basically - if you dont have any further assumptions about a term $t$ in your proof, then you could do the same proof for any term, thus, if you can derive $Sigma vdash theta(t)$, and no further assumption is made about $t$, then the prove is independent of the actual choice of $t$, and thus, $Sigma forall x theta(x)$.

However, in general, you dont have to allow general terms $t$ - you can require $t$ to be a variable, thus having a proper notion of "free" and "bounded". This makes discussing a lot easier (and doesnt change your possibilities of deriving). If $t$ doesnt occur free anywhere in $Sigma$, then from $theta(t)$ follows $forall x theta(x)$, because $t$ is arbitrary. If $t$ occurs somewhere, but it (or - if you want - a subterm of $t$) is bound there, it also makes no problems, since then its not an assumption about $t$. For example, $exists n forall m (m notin n)$ proclaims the existence of an empty set, but makes no proposition about $n$ itself.

Now, since $theta[x_2]$ has $x_2$ as the only free variable - as you said - your $t$ cannot occur freely in $theta[x_2]$, except for $t=x_2$. But if $t=x_2$, you still have no problem, since $x_2$ is bound in the axiom. Thus, you have no problems. Hope this could help you.

• Next nt.number theory - Irreducibility of polynomials in two variables
• Previous complex geometry - Newlander-Nirenberg for surfaces