Let $A$ be some hypotheses, $A_1=A\cup\{\exists xp(x)\rightarrow p(c)\}$. Then, if $A$ is free of contradiction, so is $A_1$.

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.

• 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. Sep 18 at 22:24
• "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. Sep 19 at 7:45
• 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$. Sep 19 at 7:57
• @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)$? Sep 19 at 9:12
• See so.called Theorem on constants. Sep 19 at 9:28