# Rule C (Introduction to mathematical logic by Mendelson fifth edition)

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?
-
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. –  André Nicolas Aug 8 '11 at 0:30

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$.
“The subscript C has nothing to do with a new theory, it is just a decoration.” I agree. But using the same symbol for different purpose … I understood the Rule C as a prove for “if $\Gamma \vdash_C B$ then $\Gamma \vdash B$”. “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$.” I am sorry. I did not get it. Would you collaborate? It is very interesting, but in your example I do not see new constants. –  Victor Victorov Aug 8 '11 at 23:41
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. –  Carl Mummert Aug 9 '11 at 2:03