Why are universal introduction and existential elimination valid inference rules?

Question

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.

Answer 1

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

Answer 2

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