Am I missing something in the definition of universal generalization?

Question

Today I came across the definition of universal generalization in first-order logic.

The definition in my script goes as follows (translated):

If we know, that for any element $a \in X: P(a)$ is true, we can conclude, that $\forall x \in X:P(x)$ is true.

Now for my question: Is it legitimate when I just write: $\forall a \in X:P(a)\rightarrow \forall x \in X: P(x)$

This definition of mine seems redundant to me, and therefore I have doubts that it is right. Is it the same, or did I get something wrong?

Answer 1

The meaning of $\forall$ is given in natural language. "$\forall$" and "$\text{for all/any/each}$" live in different realms. Natural language has meaning before we start constructing the formalism, and so it can be used to give the semantics of "$\forall$" without being circular or redundant.

Your translated bit of text is saying the following, written as an inference rule

$$ \frac{\text{For all elements $a$ in $X$, $P(a)$ holds}}{\forall x \in X \mathop. P(x)} $$

By writing down $\forall a \in X \mathop. P(a) \implies \forall x \in X \mathop. P(x)$ and concluding that it holds, you have used the above inference rule.

Answer 2

Is it legitimate when I just write: $\forall a \in X:P(a)\rightarrow \forall x \in X: P(a)$

It would less confusing if you wrote equivalently: $\forall a \in X:P(a)\rightarrow \forall x \in X: P(b)$

This implication is not necessarily true. It would be true if $X=\{b \}$. It would be false if we had $X=\{c\}$, $c \neq b$ and $\neg P(b)$.