# Confusion about steps of proof of rule C.

This question is from Introduction to Mathmatical Logic" by Elliot Mendelson , forth edition , page 83.Introduction to Mathmatical Logic

I am somewhat confused about some steps of the proof of rule C in the book.Here are the steps I am confused about:

1."We replace $$d_k$$ everywhere by a variable $$z$$ that does not occur in the proof" I don't get intuitively how this line is justified syntactically.What does it mean by "does not occur in the proof"?. Also, what "proof" they are exactly talking about?

2.

and, by Gen,
$$\Gamma , \mathscr C_1(d_1),...,\mathscr C_{k-1}(d_{k-1}) \vdash (\forall z)(\mathscr C_k(z) \to \mathscr B)$$ Hence, by Exercise $$2.32(d)$$, $$\Gamma , \mathscr C_1(d_1),...,\mathscr C_{k-1}(d_{k-1}) \vdash (\exists y_k)\mathscr C_k(y_k) \to \mathscr B$$

I understand the use of Exercise $$2.32(d)$$ .What I don't understand is , how they were able to replace $$z$$ with $$y_k$$ ?

3.

But, $$\Gamma , \mathscr C_1(d_1),...,\mathscr C_{k-1}(d_{k-1}) \vdash (\exists y_k)\mathscr C_k(y_k)$$

I have no idea how this line is derived.

• Page 90? Having said that, we have two proof systems: the "basic one, with MP and Gen as only rules of inference, and the corresponding $\vdash$ relation, and a new one, where we have three rules: the previous two plus Rile C, with $\vdash_C$. Commented Apr 27, 2021 at 7:57
• The gist is Prop.2.10 (page 82): if $\Gamma \vdash_C B$, then $\Gamma \vdash B$. Thus, the prop will start from a derivation that uses Rule C and will produce a new derivation of the same end-formula that does not use it. Commented Apr 27, 2021 at 7:59
• So, to replace $d$ everywhere means that we have the original proof $\vdash_C$ that uses an individual constant $d$ and we replace in the sequence of formulas (the derivation) every occurrence of $d$ with $z$ (new individual variable). Commented Apr 27, 2021 at 8:01
• @MauroALLEGRANZA About the page number, I mixed up the page number by the pdf page number.Sorry about that. Commented Apr 27, 2021 at 9:19
• @MauroALLEGRANZA Regarding my 1. question , I found a similar post about it you answered Confused by a step in the 'Rule C' proof in Mendelson's Logic Textbook.In that post , you showed semantically the justtification of 1.Now,do I have to use completeness thoerems to prove it syntatically , or is there another way which don't require completeness theorems? Commented Apr 27, 2021 at 9:24

To 1)

We we have two proof systems: the "basic" one, with $$\text {MP}$$ and $$\text {Gen}$$ as only rules of inference, with the corresponding derivability relation $$\vdash$$, and a new one, where we have three rules: the previous two plus $$\text {Rule C}$$, with $$⊢_C$$.

Prop.2.10 (page 82) says: if $$Γ ⊢_C B$$, then $$Γ ⊢ B$$. The proposition starts from a derivation that uses $$\text {Rule C}$$ and will produce a new derivation of the same end-formula that does not use it.

To replace $$d$$ everywhere means that, starting from the original $$⊢_C$$ derivation that uses the individual constant $$d$$, we have to replace in the sequence of formulas, starting from the first formula where $$d$$ occurs, every occurrence of $$d$$ with a new individual variable $$z$$.

We have to convince ourselves that this move is correct: $$d$$ is new, and thus no formulas in $$\Gamma$$ con use it.

Adding $$d$$, we can use it in instances of logical axioms; but the replacement of $$d$$ with $$z$$ will produce correct instances of logical axioms.

$$\text {MP}$$ is not affected; the only care must regards $$\text {Gen}$$, and here we have the proviso in the statement of $$\text {Rule C}$$.

In conclusion (assuming for simplicity that we have only one use of $$\text {Rule C}$$ in the derivation), starting from $$\Gamma \vdash_C B$$ we have: $$\Gamma \vdash C(z) \to B$$.

To 2)

Variable $$z$$ is new in the derivation; thus, it occurs nowhere in $$\Gamma$$ and we can "genaralize" it: $$\Gamma \vdash \forall z (C(z) \to B)$$.

Then we apply Coroll. 2.32 (d) to get: $$\Gamma \vdash \exists z C(z) \to B$$, because $$z$$ does not occur in $$B$$ [recall that $$d$$ does not occur in $$B$$].

But we can always "rename" a bound variable, provided that we do not violate the proviso regarding the free for condition [in a nutshell: $$\forall x B(x) \vdash B(y) \vdash \forall z B(z)$$].

Thus, we "restore" the original variable $$y$$ of $$\exists y C(y)$$ to get:

$$\Gamma \vdash \exists y C(y) \to B$$.

To 3)

Now the final step. The original proof $$\Gamma \vdash_C B$$ used $$\text {Rule C}$$ because somewhere in the derivation there were a formula $$\exists y C(y)$$ and $$\text {Rule C}$$ was used to introduce the new step $$C(d)$$.

But if $$\exists y C(y)$$ occurred in some step of the original derivation, either (i) $$\exists y C(y) \in \Gamma$$ or (ii) $$\Gamma \vdash \exists y C(y)$$.

In both cases:

$$\Gamma \vdash \exists y C(y)$$.

Thus, from:

n) $$\Gamma \vdash \exists y C(y) \to B$$,

and

n+1) $$\Gamma \vdash \exists y C(y)$$,

by $$\text {MP}$$ we have:

n+2) $$\Gamma \vdash B$$.

• Understood everything except ... How do I justify substituing $z$ for $d$ for axioms (A4) and (A5).Also I will never need completeness theorems for the proof of rule C, right? Commented Apr 27, 2021 at 11:17
• @Prithubiswas - in what sense? (A4) is $\forall x A(x) \to A(t)$. Thus, if in the original derivation you have used $\forall x A(x) \to A(d)$ now you have to use $\forall x A(x) \to A(z)$. Commented Apr 27, 2021 at 12:03
• "MP is not affected; the only care must regards Gen" Wait, why do we have to put care regards Gen , isn't it as simple as justify substituting $z$ for $d$ for the MP case , or is there a special twist ? Commented Apr 27, 2021 at 13:00
• @Prithubiswas - Rule C definition (page 82) point 3. Commented Apr 27, 2021 at 13:14
• @Prithubiswas - of course YES. The def of Rule C asks for "$d$ new". Thus, the first use of Rule C introduce $d_1$ new; with a second use of Rule C you cannot use it again (because it is nor more new) so you have to introduce $d_2$ that must be new, and thus different from $d_1$. Commented Apr 28, 2021 at 10:00