2
$\begingroup$

If $\varphi$ is a formula in a first order language $\mathcal{L}$ and $x$ is a variable that is not free in $\varphi$, then the following is a pure axiom

$$\varphi \to \forall x\varphi$$

The pure axioms are our building blocks for constructing the logic theorems. There are other pure axioms, e.g. the distribution axiom:

$$\forall x(\varphi \to \psi)\to (\forall x \varphi \to \forall x \psi)$$

My question is:

Why is the generalization axiom necessary? I'm sure (I believe it) it can't be proved from the other pure axioms (but I don't see why isn't this axiom a valid formula), however, it's doesn't seem to be so important in the sense that "it doesn't add any information at all", an example of such an axiom is (in informal language):

If $x=2$ then $x=2$ for all $z$.

Why is it so important? I mean, in my opinion, the other axioms (as the distribution axiom, for example) seem to be more necessary since those "talk" about variables that may be free in the considered formulas. I've seen a couple of lemmas that need the generalization axiom to be proved, but I can't get the intuition behind.

$\endgroup$
  • $\begingroup$ You can see also this post for the way to derive it. $\endgroup$ – Mauro ALLEGRANZA Apr 6 '15 at 21:22
  • $\begingroup$ Unless you are taking a credit course in formal logic, don't worry if you don't understand this Generalization Axiom. I could be wrong, but I doubt that most mathematicians have every heard of it. It really is not that difficult to make a well-founded generalizations. Just be careful about introducing new variables and the scope of those variables. $\endgroup$ – Dan Christensen Apr 7 '15 at 3:20
  • $\begingroup$ @DanChristensen Thanks for your comment. I actually understand this axiom, I understand what it says and why is it true, it's just that I couldn't imagine its capability until I've read the answers below. $\endgroup$ – Daniel Apr 7 '15 at 4:10
  • $\begingroup$ @DanielEscudero I was addressing my comment to all readers here. I should have made that clear. It just seems to me that most introductory texts on formal logic are needlessly complicated by considerations that never seem to be applicable in mathematical practice. The Generalization Axiom seems to be one of them. That's just not how mathematician actually think about generalizations. It seems to me that they think in terms of premise and conclusion. $\endgroup$ – Dan Christensen Apr 7 '15 at 4:36
  • $\begingroup$ @DanChristensen Ok, I've got you, but I couldn't understand the part "It seems to me that they think in terms of premise and conclusion". I didn't mean to be selfish, by the way. $\endgroup$ – Daniel Apr 7 '15 at 4:38
1
$\begingroup$

This axiom is "useful" in proving the Generalization Theorem :

If $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash ∀x \varphi$.

See :


There are other axiomatizations of first-order logic that avoid this "unnatural" axiom; see :

  • Joseph Shoenfield, Mathematical Logic (1967), page 21

or

$\endgroup$
  • $\begingroup$ Thanks for your answer, your reference were very useful. I've already taken a look to Enderton's book, I'll take a look to the other one and see what i can find. Thanks again. $\endgroup$ – Daniel Apr 7 '15 at 4:09
1
$\begingroup$

This answer is really just an elaboration of Mauro's answer.

To address your question as to why the Generalization axiom is necessary, we need it (or some mechanism like it) in order to prove lots of theorems that contain universal quantifiers.

Your example $(x = 2) \vdash \forall z (x = 2)$ is, as you describe, a correct but vacuous application of the Generalization axiom. But this Wikipedia example shows a nontrivial application of universal generalization. In fact, using the system in the first edition of the Enderton book cited by Mauro, the distribution axiom you cite in your question can be proven with the help of universal generalization.

Finally, you asked for the intuition behind it. Suppose we can prove $P(c)$ for an arbitrary constant $c$. Let's say we notice that we can follow the same strategy for any other constant. This means it's true for any constant we plug in. So it's safe to generalize it by adding the quantifier to get $\forall x P(x)$.

$\endgroup$
  • $\begingroup$ I must say thanks for your answer, and your clarity on it. I've read Enderton's book and the way they uses this axiom seems to be more natural for me. $\endgroup$ – Daniel Apr 7 '15 at 4:08
  • 1
    $\begingroup$ Please, note that the axiom $\alpha \to \forall x \alpha$ ($x$ not free in $\alpha$) does not license the derivation $P(c) \to \forall x P(x)$. For this derivation, see Enderton, page 123 : THEOREM 24F (GENERALIZATION ON CONSTANTS), whose proof needs the Generaization Th, and thus also the above axiom, $\endgroup$ – Mauro ALLEGRANZA Apr 7 '15 at 8:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.