Does generalization of axioms apply also to theorems?

430 Views Asked by At

In Enderton's book "A Mathematical Introduction to Logic" (second edition), he includes six axiom groups, and allows also for a generalization of those axioms such that if $\Psi$ is an axiom then $\forall x \Psi$ is also an axiom.

Is this rule also intended to apply to theorems from those axioms? In other words, if $\Psi$ is a theorem of $\Gamma$, can I conclude $\forall x\Psi$ is also a theorem?

2

There are 2 best solutions below

0
On BEST ANSWER

I have the first edition of Enderton's book, but I conjecture that what I'm about to write is also true for the second edition. The axioms are defined to be formulas of certain particular forms along with anything obtainable as generalizations of them (i.e., attaching universal quantifiers that govern the whole formula). There is no rule of inference that allows you to generalize theorems in the same way. There is, however, a metatheorem, called the Generalization Theorem, which implies, as a special case, that if a formula $\phi$ is provable from just the axioms, then so are its generalizations.

Notice, though, that the deduction of $\forall x\,\phi$ would not be just the deduction of $\phi$ followed by a single step that attaches the universal quantifier. Rather, the whole deduction of $\phi$ needs to be modified --- with universal quantifiers attached to formulas and additional lines inserted into the proof --- to produce a deduction of $\forall x\,\phi$.

Also, if you're dealing with deductions that use some hypotheses in addition to the logical axioms, then the Generalization Theorem applies only when the variable in the quantifier you want to attach is not free in any of those additional hypotheses.

7
On

If the logic in question is halfway sane (such as if its entailment relation agrees with ordinary first-order logic) then yes -- except, possibly, if $\Gamma$ contains $x$ free. You don't always get to infer $\forall x.p(x)$from $p(y)$.

Proving that this is the case depends on details of the proof system that you have not given, though. In some systems it is a primitive rule that $\psi$ entails $\forall x.\psi$.