Understanding why does universal generalization work.

Question

Universal generalization lets us deduce $P(c)$ from $\forall xP\left(x\right)$ if we can guarantee that $c$ is an arbitrary constant, it does that by demanding the following conditions:

1) $c$ does not occur in the hypotheses or the conclusion.

2) Any Skolem constant in $P(c)$ was introduced into the derivation strictly before $c$

The first condition makes sense because $c$ in the premises or the conclusion refers to a particular entity so that shouldn't be used as an arbitrary constant, however, I'm not sure about the case concerning the second condition, except for the fact that given this $c$ cannot be a Skolem constant.

So I have a question and a fact to confirm:

How exactly does 2) help promise the arbitrariness of $c$?

This implies that $c$ must be a constant introduced due to Universal Instantiation

Answer 1

Let us begin with $\exists yP(c,y)$, where $c$ is arbitrary. If we then apply existential specification, to get $P(c,e)$, $c$ is no longer necessarily arbitrary: $e$ was chosen for a particular, even if unknown, $c$. This could make the value of $c$ dependent on $e$. Then, if you apply universal generalization, you demand that $P(c,e)$ holds for every value of $c$, not just for some specific value, relevant to $e$. This is not always true. For example, consider the following steps:

1. $\forall x\exists y(x=y)$ (premise)

2. $\exists y(c=y)$ (u.s. 1)

3. $c=e$ (e.s. 2)

4. $\forall x(x=e)$ (u.g. 3) Error!

On the other hand, if the introduction of $e$ came before the introduction of $c$, as in $\forall xP(x,e)$, then, we know that $P(c,e)$ will hold for every value of $c$, not just for a specific $c$ that depends on a specific $e$.

Answer 2

Helpful Hint: This may not be standard FOL or directly answer your question, but in a mathematical proof, if you want to prove $\forall a\in S: P(a)$, you can start by assuming $x\in S$ where $x$ is not free in any previous active statement.

Then derive $P(x)$ where any subsequently introduced assumptions have been discharged and no other free variables in $P(x)$ were introduced in subsequent statements (after $x\in S$). Then you can discharge the assumption $x\in S$ and infer that $\forall a\in S: P(a)$ where $a$ is not a variable in $P(x)$ and $a\neq S$.