# Need Help Understanding Universal Quantifier Introduction in First-Order Logic

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.

-
"A could hold for 'x' but not for all 'x's" is not possible. The point is x is a name for an arbitrary value; if you've proved something about x without making any assumption about the value denoted by the symbol x, then it must be true for all instances for x. –  Marc van Leeuwen Aug 27 '12 at 22:26
The "where" part below each rule gets rid of the possibilities that $C$ holds for some $x$ and $A(x)$ holds for not all $x$ where the symbol $x$ refers to the same thing. The first rule says that $C$ has no free variables. That means even if $x$ appears in $C$, it must be bound, and has no relation with the same symbol $x$ that appears in $A(x)$. The same is true for the second rule. –  Tunococ Aug 27 '12 at 22:56

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$.

-
Just to add a little - the "deduction theorem" gives a link between the metatheoretic if/then and the $\to$ connective. It says that if $P \vdash Q$, where $P$ is a sentence, then $\vdash P \to Q$. The example in the question shows why the restriction on $P$ is necessary. en.wikipedia.org/wiki/Deduction_theorem –  Carl Mummert Aug 28 '12 at 2:07

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 $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.

-
This argument confuses truth and provability: "Assume that C is true. Then, by modus ponens, A is also a theorem" is nonsense -- being true does not make something a theorem. And the reason why $C\to\forall x A$ is a theorem is that there the very rule in question allows us to construct a proof of it. –  Henning Makholm Aug 28 '12 at 11:26
Thank you for your kind remark Mr. @Makholm. Of course I used both expressions ("true formula" and "theorem") as synonyms of a "provable formula". I edited my post and now everything is clear. –  Godot Aug 28 '12 at 13:57
But your reasoning still doesn't work -- it seems to assume that the meaning (and/or theoremhood) of $\phi\to\psi$ is concerned with the case that $\phi$ itself is a theorem (rather than merely being true in some particular situation). (...) –  Henning Makholm Aug 28 '12 at 15:45
By the same kind of reasoning I would be able to "prove" that $xx=1\to xx\neq 1$ ought to be a theorem in the basic theory of groups: Because I know that $xx=1$ is not a theorem (there are groups it is not valid for, so it cannot be a theorem), if I assume that $xx=1$ is a theorem, I immediately hit a contradiction which allows me to conclude anything at all -- in particular I can conclude $xx\ne 1$. So $xx=1\to xx\ne 1$ must be a theorem ?!? –  Henning Makholm Aug 28 '12 at 15:46
I don't understand your last comments. –  Godot Aug 28 '12 at 18:52