2

On page 123, A Mathematical Introduction to Logic, Herbert B. Enderton（2ed)(A part of proof 24F,"GENERALIZATION ON CONSTANTS")

$\alpha$ is a logical axiom, then $\alpha^{c}_{y}$ is also a logic axiom.(Read the list of logical axioms and note that introducing a new variable will transform a logical axiom into another one.)

I can't understand what principle guarantee $\alpha^{c}_{y}$ is a axiom.

$c$ is a constant symbol that occur in $\alpha$, and $y$ is a variable that is substitutable for $c$ in $α$.

The logical axioms are then all generalizations of wffs of the following forms, where $x$ and $y$ are variables and $α$ and $β$ are wffs(well-formed formula):

  1. Tautologies(in the sense of propositional logic);
  2. $∀ x α →α^x_ t $, where $t$ is substitutable for $x$ in $α$($α^x_ t$ is the formula derived from $\alpha$ by replacing $x$ by a term $t$);
  3. $∀ x(α→β)→( ∀ x α→∀x β)$;
  4. $α→∀x α$, where $x$ does not occur free in $α$.
Metta World Peace
  • 6,403
  • Sorry, what is 'wff'? And the notation $\alpha^x_t$ is not that familiar (at least to me), though implicitly one can guess what it is.. – Berci Feb 19 '13 at 10:17
  • @Berci: My bad. I've fixed it. – Metta World Peace Feb 19 '13 at 10:28
  • One more question: in steps 2.--4., is it meant so that 'if $\forall x,\alpha$ is logical axiom then $\alpha^x_t$ is a logical axiom too', or simply the implication formula $\forall x,\alpha\to\alpha^x_t$ itself is a logical axiom for all (w.f.) $\alpha$? – Berci Feb 19 '13 at 11:09
  • @Berci:The latter one. – Metta World Peace Feb 19 '13 at 11:11
  • In that sense I see very few chance that $\alpha^c_y$ itself will be a logical axiom, but will be derivable from those, using Modus Ponens.. – Berci Feb 19 '13 at 11:25

2 Answers2

3

Remember each of the groups of logical axioms is an infinite list of axioms. If you start with a tautology $\gamma$ and you replace a constant in it with a new variable, the result $\gamma_y^c$ is still a tautology. The same is true for the other axiom groups - if you take an axiom $\gamma$ in any of these groups, and replace a constant with a new variable, then $\gamma^c_y$ will also be an axiom in the same group. Perhaps you are confused because $\alpha$ is used to refer to an arbitrary axiom, but it is also used as a variable for defining the axioms. When Enderton talks about $\alpha$ being a logical axiom he means that $\alpha$ is the entire logical axiom, not just a piece of one. Also note that, on p. 123, the variable being introduced did not appear in the formula previously, so there is no danger of the new variable clashing with other variables in the formula.

A particular example in group 2: because $$ (\forall x)[(c+1)*x = c*x + 1*x] \to [(c+1)*z = c*z + 1*z] $$ is a logical axiom (which you can check it is, in the appropriate language), then $$ (\forall x)[(y+1)*x = y*x + 1*x] \to [(y+1)*z = y*z + 1*z] $$ is also a logical axiom. If the original is $\gamma$, the latter is $\gamma^c_y$.

Carl Mummert
  • 81,604
1

To add more clarification, take group 2 for example. Suppose we have an axiom $\forall x\alpha \rightarrow \alpha ^x _t $, and we want to prove that $(\forall x\alpha \rightarrow \alpha ^x _t )^c_y = \forall x\alpha ^c_y \rightarrow \alpha ^{xc}_{ty} $ is also an axiom, then there are 2 possible situations:

  1. c does not occur in $t$, then $\alpha ^{xc}_{ty}=\alpha^{cx}_{yt}$. Hence $\forall x\alpha ^c_y \rightarrow \alpha ^{xc}_{ty}=\forall x(\alpha ^c_y) \rightarrow (\alpha ^{c}_{y})^x_t$, which is obviously an axiom in group 2.
  2. c occurs in $t$, then we take $t'=t(c/y)$ where $t(c/y)$ is the wff derived from $t$ by replacing the $c$ in $t$ by $y$. Then $\forall x\alpha ^c_y \rightarrow \alpha ^{xc}_{ty}=\forall x(\alpha ^c_y) \rightarrow (\alpha ^{c}_{y})^x_{t'}$ is again an axiom of group 2.

Axioms in other groups can be done in similar manners. Hope this helps.

Michael
  • 407