lo.logic - Why are universal introduction and existential elimination valid inference rules?

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 notin FV(Sigma)}
{Gamma; Sigma vdash forall x.; theta}$$