See Wolfgang Rautenberg, A Concise Introduction to Mathematical Logic, (3rd ed - 2010).

I've a problem in "decrypting" the statement and the proof of a theorem [see page 97] :

Let $\mathcal L$ be a language and $c$ a constant symbol. $\mathcal L_c$ is the result of adjoining $c$ to $\mathcal L$.

Let $\alpha {z \over c }$ denote the formula arising from $\alpha$ by replacing $c$ with the variable $z$, and put $X {z \over c } := \{ \alpha {z \over c } | \alpha \in X \}$. $c$ then no longer occurs in $X {z \over c }$.

Lemma 2.1 (on constant elimination). Suppose $X \vdash_{\mathcal L_c} \alpha$. Then $X {z \over c } \vdash_{\mathcal L} \alpha {z \over c }$ for almost all [emphasis added] variables $z$.

Proof by rule induction in $\mathcal L_c$. If $\alpha \in X$ then $\alpha {z \over c } \in X {z \over c }$ is clear; [...].

[Consider the induction step on ($\forall_1$).] Let $\alpha, {t \over x }$ be collision-free, $X \vdash_{\mathcal L_c} \forall x \alpha$, and assume that $X {z \over c } \vdash_{\mathcal L} (\forall x \alpha) {z \over c }$ for almost all $z$. In addition, we may suppose that $z \notin var \{ \forall x \alpha, t \}$ for almost all $z$. [...]

The rules of the system are a version of natural deduction rules for $\land$ and $\lnot$ [see page 92] like :

$${X \vdash \alpha, \beta \over X \vdash \alpha \land \beta }\, \, (\land_1)$$

$${X \vdash \alpha \land \beta \over X \vdash \alpha, \beta }\, \, (\land_2)$$

and a couple of rules for the quantifier $\forall$ :

$${X \vdash \forall x \alpha \over X \vdash \alpha {t \over x } }\, \, (\alpha, {t \over x } \, \text{collision-free}) \, \, (\forall_1)$$

$${X \vdash \alpha {y \over x } \over X \vdash \forall x \alpha }\, \, (y \, \text{not free in} \, X \cup \alpha) \, \, (\forall_2)$$

plus the (Initial Rule) :

$${\over X \vdash \alpha }\, \, (\alpha \in X) \, \, \text{(IR)}$$

and the monotonicity rule :

$${X \vdash \alpha \over X' \vdash \alpha }\, \, (X \subseteq X') \, \, \text{(MR)}$$


Thanks to the comment below, the above Lemma can be stated more "conventionally" as :

Suppose $X \vdash_{\mathcal L_c} \alpha$. Then $X {z \over c } \vdash_{\mathcal L} \alpha {z \over c }$ for all variables $z$, provided that $z$ is not free in $X$ nor in $\alpha$.

Due to the fact that a proof is a finite object, we can have only a finite number of free variables used in $X \vdash_{\mathcal L_c} \alpha$.

Thus, the lemma holds for "all but finitely many" variables $z$, i.e.for "almost all" variables $z$.

  • 2
    $\begingroup$ "Almost all" sometimes means "all but finitely many" - could that be the meaning here? $\endgroup$ – Matthew Towers May 17 '14 at 15:22
  • $\begingroup$ @mt_ - It is possible... but I'm not able to grasp the "role" of this limitation in the theorem above. Are you saying that it is a "convoluted" way to exclude the (finitely many) free variables that may be present in $\alpha$ ??? $\endgroup$ – Mauro ALLEGRANZA May 17 '14 at 15:27
  • 1
    $\begingroup$ Suppose $\lnot(z=c)$ is part of the formula. We really don't want to replace $c$ by $z$. $\endgroup$ – André Nicolas May 17 '14 at 15:30
  • $\begingroup$ @MauroALLEGRANZA: I have never taught the subject using natural deduction, so am assuming that the treatment of variables is not different in a significant way from the usual. Though I was a bit perturbed by $\alpha[z/c]$ where I would have used $\alpha[c/z]$. $\endgroup$ – André Nicolas May 17 '14 at 15:38
  • $\begingroup$ @AndréNicolas - this is only a "typographical" issue; in the book it is used $\alpha {z \over c}$. I arbitrarely decided (in order to save time) to write it as $\alpha[z/c]$. The meaning is [page 97] : "Let $\alpha {z \over c}$ (read “α z for c”) denote the formula arising from α by replacing c with the variable z." $\endgroup$ – Mauro ALLEGRANZA May 17 '14 at 15:43

Your Answer

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

Browse other questions tagged or ask your own question.