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