# Interpretation of generality introduction rule

I have been reading Kleene's "Introduction to Metamathematics" Chapter 5 Section 24 where it is stated that $$A(x) \vdash \forall xA(x)$$ is a deduction rule. I was wondering on the interpretation of this rule and its analog in informal mathematics. For me, I interpret it as that if some statement $$A$$ for some variable $$x$$ is true then it is true for all $$x$$, but it does not make sense for me because, for example, if $$A$$ is " is prime " then for some number it is true that it is prime but for all numbers that is not true.

• I share your doubt. For example, if we assume $x=y$, should this permit the deduction that $\forall x (x=y)$ ? Sep 21, 2018 at 4:10
• See related post Elliott Mendelson's definition of logical consequence Sep 21, 2018 at 6:04
• Already discussed into the post A problem with the Gen rule in Kleene's Mathematical Logic Sep 21, 2018 at 6:05
• You have to read the peculiar IM's def of a free var held constant (instead of varie): see page 95, their use in the formulation of Deduction Theorem for predicate calculus (page 96) and the Examples 2,3, and 4 page 149. Sep 21, 2018 at 7:19
• @Mauro ALLEGRANZA Thanks for the links for related posts. I am not sure I understand your comment about variable being held constant. It is necessary only when the formula is being discharged, but nothing is discharged in this deduction rule. Sep 21, 2018 at 15:04

No, the interpretation is not just for some free variable $$x$$, rather for any free variable $$x$$.

The free variable $$x$$ is required to be arbitrary within the domain.   So it cannot have any restrictions assumed.

$$\dfrac{\Sigma\vdash P(a)}{\Sigma\vdash \forall x~P(x)}\qquad\text{when a is an arbitrary free variable}$$

• How do you encode that variable is arbitrary in logic? Sep 21, 2018 at 15:11
• @DanielsKrimans - we encode it with the proviso : "$a$ not free in $\Sigma$" Sep 26, 2018 at 12:05

If $$A(x)$$ holds without any additional assumption n $$x$$ then $$A(x)$$ holds for all $$x$$, i.e., $$\forall xA(x)$$. For example, in the the realm of natural numbers $$\tag1 x+1=1+x$$ differs from $$\tag2 x\text{ is prime}$$ insofar as only the former holds without additinal assumptions on what $$x$$ is. Hence, we are only allowed to infer $$\tag3 \forall x\colon x+1=1+x.$$

• how do you encode ''without additional assumptions on $x$'' in logic? Sep 21, 2018 at 15:08

I was wondering on the interpretation of this rule and its analog in informal mathematics.

The vast majority of published mathematical proofs are rigorous but nonetheless "informal" proofs. If proofs in "informal mathematics" are your primary interest, books on metamathematics or mathematical logic are not the best place to start.

When writing mathematical proofs, the only time you really need to make a universal generalization is when discharging a premise. If, for example, you want to prove $$\forall x: [x\in S \implies P(x)]$$ by direct proof, you can start with the premise $$x\in S$$ where $$x$$ is a free variable. Then prove that $$P(x)$$ is true where no free variables other than $$x$$ are occurs in $$P(x)$$. Then you can conclude, as required, that $$\forall x: [x\in S \implies P(x)]$$ where $$x$$ is a bound variable. Then you will have then effectively discharged the initial premise.

There are, of course, several variations including proofs by contradiction and proofs nested within proofs, but the basic principle demonstrated in this example will still hold.