Does the axiom of specification prevent writing any proof?

Question

In set theory, the axiom of specification says that $\forall x_0\exists x_1\forall x_2\left(x_2\in x_1\leftrightarrow x_2\in x_0\land\theta\left[x_2\right]\right)$, where $\theta\left[x_2\right]$ is any formula that has $x_2$ as the only free variable.

In first order logic, the rule of universal introduction says that if $\Sigma\vdash\phi\left[t\right]$ then $\Sigma\vdash\forall x\phi\left[x/t\right]$, where $\Sigma$ is a set of axioms, $\phi$ is any formula that has $x$ as the only free variable and $t$ is any term. There is one restriction: $t$ cannot appear in $\Sigma$.

The problem is that, in set theory, every instance of the axiom of specification belong to $\Sigma$; in particular, instances of the axiom of specification in which a term appears belong to $\Sigma$. So every term appears in $\Sigma$, and you cannot use the rule of universal introduction at all. Without that rule, no relevant proof can be written down as far as I know.

I'm not sure if the question is clear enough; please let me know if it isn't.

Thanks.

Answer 1

Your definition of the rule of universal introduction is wrong. The usual rule for universal introduction says that if $\Sigma\vdash\phi$ and $x$ is a variable that does not occur free in $\Sigma$ then $\Sigma\vdash\forall x.\phi$. (There is a variant system that does not have the freeness condition, but then there needs to be a restriction on the deduction theorem.)

You seem to be mixed up with the universal elimination rule which says that $\vdash(\forall x.\phi) \Rightarrow \phi[x\mapsto t]$ for any term $t$.

Answer 2

It's been a good five years or so since I've done logic, so this is only a rough sketch:

The unintuitive point in formalizing proofs is that ᵩ(t), where t is a variable (what you call a "term"), while not making grammatical sense (it's not a sentence), should be thought of as meaning ∀x. ᵩ(x). This is what you called "the rule of universal introduction".

"t cannot appear in $\Sigma$" is just a formality. You can read that as "t cannot appear unbound in $\Sigma$". The axiom of specification for a specific ᵩ(t), uses ᵩ(x) for some bound variable. So no problem arises.

I hope that helps. I would be more explicit, but as I said it's been a while since I've really had to deal with the details of logic.

Answer 3

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 \not\in 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.