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.

  • 4
    $\begingroup$ "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. $\endgroup$ Aug 27, 2012 at 22:26
  • $\begingroup$ 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. $\endgroup$
    – Tunococ
    Aug 27, 2012 at 22:56

2 Answers 2


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

  • $\begingroup$ 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 $\endgroup$ Aug 28, 2012 at 2:07
  • $\begingroup$ It is, however, correct to say $\forall x.(C \to A(x)) \to (C \to \forall x.A(x))$. I think the issue isn't that $\to$ differs from $\vdash$, but rather an issue of how free variables scope relate to either of them. $\endgroup$
    – DanielV
    Sep 27, 2016 at 21:19

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.

  • $\begingroup$ 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. $\endgroup$ Aug 28, 2012 at 11:26
  • $\begingroup$ 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. $\endgroup$
    – Godot
    Aug 28, 2012 at 13:57
  • $\begingroup$ 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). (...) $\endgroup$ Aug 28, 2012 at 15:45
  • $\begingroup$ 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 ?!? $\endgroup$ Aug 28, 2012 at 15:46
  • $\begingroup$ I don't understand your last comments. $\endgroup$
    – Godot
    Aug 28, 2012 at 18:52

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .