0
$\begingroup$

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.

$\endgroup$
5
  • 1
    $\begingroup$ 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$. $\endgroup$ Commented Apr 27, 2021 at 7:57
  • $\begingroup$ 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. $\endgroup$ Commented Apr 27, 2021 at 7:59
  • $\begingroup$ 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). $\endgroup$ Commented Apr 27, 2021 at 8:01
  • 1
    $\begingroup$ @MauroALLEGRANZA About the page number, I mixed up the page number by the pdf page number.Sorry about that. $\endgroup$ Commented Apr 27, 2021 at 9:19
  • $\begingroup$ @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? $\endgroup$ Commented Apr 27, 2021 at 9:24

1 Answer 1

2
+50
$\begingroup$

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$.

$\endgroup$
10
  • $\begingroup$ 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? $\endgroup$ Commented Apr 27, 2021 at 11:17
  • $\begingroup$ @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)$. $\endgroup$ Commented Apr 27, 2021 at 12:03
  • $\begingroup$ "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 ? $\endgroup$ Commented Apr 27, 2021 at 13:00
  • $\begingroup$ @Prithubiswas - Rule C definition (page 82) point 3. $\endgroup$ Commented Apr 27, 2021 at 13:14
  • 1
    $\begingroup$ @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$. $\endgroup$ Commented Apr 28, 2021 at 10:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .