1
$\begingroup$

By Existential Rule E4 $\mathscr B(t, t)\vdash (\exists x) \mathscr B(x, t)$. But how can we get back? How can we formalize $(\exists x) \mathscr B(x)\vdash \mathscr B(t)$? It is shown on page 74 and it is called “rule C (“C” for “choice”)".

But two questions:

  1. Designation. “… rule C deduction in a first-order theory K is defined in the following manner: $\Gamma \vdash_C \mathscr B$...” Wait a minute! What is the name of the theory? Usually $ \vdash_C$ means we have theory C, but here it looks like $ \vdash_C$ used to show that we use rule C? It is strange.
  2. “(d) there is a preceding wf $(\exists x) \mathscr E(x)$ such that $\mathscr D_i$ is $\mathscr E(d)$, where $d$ is a new individual constant (rule C).” A new individual constant? But in this case we have a new term and a new first-order theory. Why we cannot use already existing individual constant?
  • 2
    For ($2$), because properties of interpretations of existing constant symbols may already be partly or wholly determined. But the new constants need not be introduced one at a time, one can throw in "enough" of them at the beginning. Yes, we get a new language, but that will be taken care of later.2011-08-08

1 Answers 1

4

In the fourth edition, at least, the reason Mendelson uses the notation $\vdash_C$ is that he is defining a second derivability relation, which differs from his original one by allowing the use of Rule C under certain conditions. He then proves that if $\Gamma \vdash_C B$ then $\Gamma \vdash B$, which justifies why he left out Rule C in his original definition of $\vdash$. The subscript $C$ has nothing to do with a new theory, it is just a decoration.

As for why new constants are required, consider applying Rule C to the statements $(\exists x)(x = 0)$ and $(\exists x)(x = 1)$ in the presence of axioms that imply $0 \not = 1$.

  • 0
    You can't make the same constant equal both 0 and 1 if $0 \not = 1$. So if you apply Rule C to both of those formulas, you have to use different constants for them.2011-08-09