Using universal instantiation of the form ∀x(P(x) → Q(x))

Question

I am currently reading from multiple books and I am finding seeming contradictions regarding the rules by which HOW to use UI to a given of the form ∀x(P(x) → Q(x)).

From "How to Prove it" by Daniel Velleman. "you won’t be able to apply universal instantiation to a given of the form ∀x P(x) unless you have a particular value a to plug in for x, so you might want to wait until a likely choice for a pops up in the proof. For example, consider a given of the form ∀x(P(x) → Q(x)). You can use this given to conclude that P(a) → Q(a) for any a, but according to our rule for using givens that are conditional statements,this conclusion probably won’t be very useful unless you know either P(a) or ¬Q(a)."

From "Symbolic Logic" by Hardegree. "Example 3: ∀x(Fx → Gx) To obtain a substitution instance, we replace both occurrences of x by a name, the same name for both occurrences. Thus, all of the following follow by ∀O. Fa → Ga, Fb → Gb, Fc → Gc, etc."

what am I not understanding here? thanks!

Answer 1

See Velleman, page 55:

the statement $\forall x P(x)$ says that $P(x)$ is universally true.

Thus $P(x)$ must be true for every value of $x$ in the universe $U$.

Regarding universal instantiation (page 155) :

You can plug in any value, say $a$, for $x$ and use this given to conclude that $P(a)$ is true.

What is $a$ ? It seems that a "value" for a variable must be an object of the domain $U$: e.g. a number.

All this is quite "informal". In a formal settings, see some mathematical logic textbook, the universal instantiation rule "operates" with substitution of a term in place of the quantified variable $x$.

A term can be:

a variable, a constant, a "complex" term built up from variables and constants with function symbols.

In this case, the rule licenses the derivation of $P(t)$ from $\forall x P(x)$, for every term $t$ of the language.

The same in Velleman; see page 118:

if you were proving a goal of the form $\forall x \in A \ P(x)$, you would probably start by introducing a variable $x$ to stand for an arbitrary element of $A$.

Thus, if no "already given" (name of) objects are available, we can use variables.