Need Help Understanding Universal Quantifier Introduction in First-Order Logic

Question

I'm reading Mathematical Logic by Stephen Cole Kleene and I am stuck trying to understand the logic behind his rule of universal quantifier introduction.

In the text, for propositional and first-order logic, the author provides first a Hilbert-type system for deduction and then a Gentzen-type system. In the Hilbert-type system for first-order logic, he posits a universal quantifier rule, which is formulated as such:

If $C \to A(x)$
then $C \to \forall(x)A(x)$

where $C$ is a 0-place predicate/propositional variable/formula with no free variables
$A(x)$ is a unary predicate taking $x$/a formula with $x$ free

This rule is re-branded as universal quantifier introduction in the Gentzen-type system with syntax modified thus:

If $G \vdash A(x) $
then $G \vdash \forall(x)A(x)$

where $G$ is the set of assumptions with the requirement that $G$ does not contain $x$ free
and $A$ is as it was in the previous formulation

I can't seem to grasp the logic behind either formulation of this rule. It doesn't follow that $[C \to A(x)] \to [C \to \forall(x)A(x)]$ since $C$ could be true and $A$ could hold for $x$ but not for all $x$s, rendering the former implication true and the latter false which would immediately make the whole implication false. If any light could be shed on why this rule holds and maintains the soundness of the deduction, it would be much appreciated.

Answer 1

Note that neither of the two rules you quote are formulated as "$(C\to A(x))\to(C\to\forall x.A(x))$". The middle $\to$ there is not in any of the rules -- they carefully use "if ... then" rather than a symbolic "$\to$", which means that the implication they express is at the level of logic-as-a-formal-game rather than at the level of truth in a particular interpretation. By reading it as $\to$ you have inadvertently made the rules into nonsense.

What the rule tells you is that if the string of symbols $$C\to A(x)$$ is valid in the interpretation you speak about, then the string of symbols $$ C\to\forall x.A(x)$$ is also valid. This is something that holds about particular strings of symbols, some of which symbols happen to be $x$, but it's not something that holds for any particular value of $x$ -- at the levels the rules work at, $x$ is just chalk and it does not have values.

To say that $C\to A(x)$ is valid means that it evaluates to true under every assignment of its free variables. Therefore the claim "$C\to A(x)$ is valid in such-and-such interpretation" does not itself have $x$ as a free variable; it is not a claim that can even in principle be true for some but not all values of $x$ any more than it can be true for some but not all values of $q$.

Answer 2

In case of many logical systems the following metatheorem can be proved:

"if the formula $A$ is a theorem and a variable $x$ is not a constant (i.e. it does not occur freely in any of our axioms), then $\forall x A$ is also a theorem".

If, in addition, you have at your disposal the deduction theorem:

"if $C$ is a theorem in a system with axiom set enlarged by $B$ then $B\rightarrow C$ is a theorem"

then your universal quantifier rule is a simple consequence.

To be precise: suppose that $C\rightarrow A$ is a theorem in our logical system. We woud like to prove that $C\rightarrow\forall x A$ is also a theorem. Adjoin $C$ to the set of our axioms.. Then, by modus ponens, $A$ is also a theorem. Since $x$ is not a constant in our logical system we have also that $\forall x A$ is a theorem by the virtue of the metatheorem mentioned at the beggining of my answer. Hence $C\rightarrow\forall x A$ is a theorem of our logical system, thanks to the deduction metatheorem.

As you can see in order to prove that metatheorem you mentioned all you need is the deduction theorem and that simple metatheorem I beggined with.

Those metatheorems can be proved in case of Hilbert and Gentzen type systems using metareasonining about the structure of assemblies but the details of proof depend on the particular formalism chosen to encode those systems.