I'm confused by an exercise. Here is how it goes.

Let $A$ be some hypotheses, $A_1=A\cup\{\exists xp(x)\rightarrow p(c)\}$, where $c$ is a constant that does not appear in $p(x)$. Prove that if $A\,\nvdash\bot$, so does $A_1$.

Proof given by the textbook: Suppose $A_1\vdash\bot$, then $A\,\vdash\neg(\exists xp(x)\rightarrow p(c))$ (proof by contradiction). From here we have the following proof from $A$: \begin{align}{ ......\\ \neg(\exists xp(x)\rightarrow p(c)),\\ \exists xp(x)\wedge\neg p(c),\\ \exists xp(x),\\ \neg p(c),\\ \neg p(y),\qquad\text{y is a variable that does not appear in any formula in this proof till this point}\\ \forall y\neg p(y),\\ ......\text{(some obvious use of axioms here)}\\ \exists xp(x)\wedge\neg \exists xp(x). }\end{align} Therefore, $A\,\vdash\bot$.

My question: why is it allowed to substitute the constant with a new variable? Do I misunderstand the concept of 'constant'?

Context: The book is mainly about ZFC, thus merely introduces classical first-order logic briefly. I can't find anything from it to justify such substitutions. Plus, the contradiction $A\,\vdash\bot$ seems easily avoided when there are more than $1$ object in the system.

  • $\begingroup$ You'll get a better answer if you tell us what book you are using. The exercise doesn't look right as stated, if $c$ appears in $A$, then $A_1$ might be inconsistent while $A$ is consistent. $\endgroup$
    – Rob Arthan
    Sep 18 at 22:24
  • $\begingroup$ "why is it allowed to substitute the constant with a new variable?" The variable is new in the sense that it occurs nowhere in the formulas involved in the proof. Thus, it is like a constant. $\endgroup$ Sep 19 at 7:45
  • $\begingroup$ The proof seems part of so-called Henkin's completeness proof. If so, the requirement is that $c$ is new, i.e. it does not occur into $A$. $\endgroup$ Sep 19 at 7:57
  • $\begingroup$ @MauroALLEGRANZA It does make sense that $c$ must be new. But how does this allow me to substitute $c$ with a variable $y$? Is it because if $A\vdash q(c)$, then $q(c)$ must come from $\forall yq(y),\,\forall yq(y)\rightarrow q(c)$, so I can track back to $q(y)$ or $\forall yq(y)$? $\endgroup$
    – kotowh
    Sep 19 at 9:12
  • $\begingroup$ See so.called Theorem on constants. $\endgroup$ Sep 19 at 9:28


You must log in to answer this question.

Browse other questions tagged .