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?
$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – André Nicolas Aug 8 '11 at 0:30
4
$\begingroup$

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

$\endgroup$
  • $\begingroup$ “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. $\endgroup$ – Victor Victorov Aug 8 '11 at 23:41
  • $\begingroup$ 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. $\endgroup$ – Carl Mummert Aug 9 '11 at 2:03

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.