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.
 A: 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}$$
A: 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
