MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.


share|cite|improve this question

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$.

share|cite|improve this answer

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.

share|cite|improve this answer

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.