Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

1 Answer 1

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

share|improve this answer
    
“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

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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