# Why are universal introduction and existential elimination valid inference rules?

I'm studying the inference rules of natural deduction for the first-order logic. I cannot understand why universal introduction and existential elimination are valid rules. The first one says that if $\Sigma\models\theta[k/x]$ then $\Sigma\models\forall x\theta[x]$; the second one says that if $\Sigma\models\exists x\theta[x]$ then $\Sigma\models\theta[k/x]$.

Universal introduction would allow the following deduction: if $1$ is odd, then every number is odd. Existential elimination would allow the following deduction: if there exists an odd number, then $2$ is odd.

I read about some restrictions you should check before applying such rules, but they are also not so clear to me.

Some notes about the notation I used: $\Sigma$ is a set of sentences; $\theta$ is a formula such that the only free variable is $x$ and such that $x$ is not in the set of bounded variables; $\theta[k/x]$ is the formula you obtain from $\theta[x]$ by substituting every free instance of $x$ with $k$; of course, $x$ is a variable and $k$ is a constant.

Thanks.

-
Certainly 1 is not a free variable. – Harry Gindi Feb 4 '10 at 13:20

You are getting tripped up by some very traditional, yet very bad, notation.

The $k$ in these formulas are not true constants of the domain of individuals, but rather are Skolem constant. The idea is that if we have, say, the knowledge that an existential formula $\exists x. \theta(x)$ is true, we can treat it as if it were the formula $\theta(k)$, where $k$ is some particular arbitrary constant about which we know nothing. Conversely, if we know that $\theta(k)$ holds for any arbitrary constant $k$, then we can conclude $\forall x.\; \theta(x)$. These made-up constants are called Skolem constants.

If we explicitly manage the free variables with a context of free variables $\Gamma$, then the introduction and elimiantion rules look the way you expect, and agree with Andrej Bauer's rules.

$$\frac{\Gamma; \Sigma \vdash \forall x.\theta(x) \qquad FV(t) \subseteq \Gamma} {\Gamma; \Sigma \vdash \theta(t)}$$

$$\frac{\Gamma, x; \Sigma \vdash \theta \qquad \qquad x \not\in FV(\Sigma)} {\Gamma; \Sigma \vdash \forall x.\; \theta}$$

-
Andrej probably just realized that the first question was about introduction, so he deleted all of his answers and comments. – Harry Gindi Feb 4 '10 at 13:41
Well, that seemed like the best thing to do. Why would I spread my own confusion? – Andrej Bauer Feb 4 '10 at 13:49
I wasn't faulting you for it, I was just letting Neel know where your answer went, since he noted your post in his. – Harry Gindi Feb 4 '10 at 14:19
@NeelKrishnaswami: Do you know any good book or set of notes that uses a coherent notation and deals with Skolem constants? Thanks. – Francesco Turco Feb 4 '10 at 14:31
But is the notation really bad? Surely this method is used throughout ordinary mathematical practice. For example, a group theorist wants to prove that every group has a certain property, so she says "Let G be a group..." and then proves it just for G. To conclude that every group has the property is exactly the universal introduction rule as stated. – Joel David Hamkins Feb 4 '10 at 22:00

In FOL there is no such existential elimination rule which would be generally valid. Although there are some cases where such a rule is indeed valid, for example some logic programs, for arbitrary theories the inference rule does not hold.

A simple counter example is the following theory:

p(a) \/ p(b)

Although we have the following consequence:

p(a) \/ p(b) |= exists x p(x)

We neither have one of the following consequences:

p(a) \/ p(b) |\= p(a)

p(a) \/ p(b) |\= p(b)

Both consequences have a countermodel. For example the first consequence doesn't hold for a model where p(a) is false and p(b) is true. In such a model the disjunction is true, but the first consequence is false. Similarly a countermodel for the second consequence can be found.

Bye

-