“Soft”.$\Gamma\vdash\phi$ implies $\Gamma\vDash\phi$ . For every structure $\mathfrak{A}$ for the language without $P$ and $s:V\rightarrow|\mathfrak{A}|$ such that $\vDash_{\mathfrak{A}}\Gamma[s]$ , consider corresponding structure $\mathfrak{A}'$ for the language with $P$ , which extends $\mathfrak{A}$ by defining $P^{\mathfrak{A}}=\emptyset$ . Then $\vDash_{\mathfrak{A}'}\Gamma[s]$ (as no wff in $\Gamma$ uses $P$ ), and, hence, $\vDash_{\mathfrak{A}'}\phi[s]$ , implying $\vDash_{\mathfrak{A}}\phi[s']$ (for the same reason). Therefore, $\Gamma\vDash\phi$ in the language without $P$ , and $\Gamma\vdash\phi$ .

“Hard”.$\Gamma\vdash\phi$ implies that there is a deduction of $\phi$ from $\Gamma$ that may use $P$ . We show that the deduction can be changed to one not containing $P$ . Every occurrence of $Pt_{1}\ldots t_{n}$ in the deduction is an atomic subformula, which is a part of the modus ponens rule or a valid logical axiom, so that we can hope to change it to another atomic formula throughout the deduction and preserve the validity of reasoning. So, suppose that we change every occurrence of $Pt_{1}\ldots t_{n}$ to $Qu_{1}\ldots u_{m}$ in every formula $\psi$ of the deduction, we call it $\psi_{Q}^{P}$ , and we will see, what properties of such substitution we need to ensure. First, we consider logical axioms.

1. $\psi$ is a tautology. Then, by substituting an atomic formula by another one in all places, $\psi_{Q}^{P}$ remains a tautology.
2. $\psi$ is $\forall x\alpha\rightarrow\alpha_{t}^{x}$ where $t$ is substitutable for $x$ in $\alpha$ .$\psi_{Q}^{P}$ is $\forall x\alpha_{Q}^{P}\rightarrow(\alpha_{Q}^{P})_{t}^{x}$ where $t$ must be substitutable for $x$ in $\alpha_{Q}^{P}$ . The only case where $t$ is not substitutable for $x$ in $\alpha_{Q}^{P}$ , is where there is a subformula $\forall y\beta_{Q}^{P}$ such that $y\neq x$ , $x$ is free in $\beta_{Q}^{P}$ , and $y$ occurs in $t$ . If $t$ (containing $y$ ) is substitutable in $\forall y\beta$ , then $x$ is not free in $\beta$ . Therefore, to ensure that our substitution does not create a substitutability problem, we just need to make sure that $Qu_{1}\ldots u_{m}$ does not contain new (free) variables that occur anywhere as the subject of substitution. For example, we may use the same terms as in $P$ (if we have another $n$ -place predicate $Q$ ), or use variables that do not occur in the deduction at all.
3. $\forall x(\alpha\rightarrow\beta)\rightarrow(\forall x\alpha\rightarrow\forall x\beta)$ becomes $\forall x(\alpha_{Q}^{P}\rightarrow\beta_{Q}^{P})\rightarrow(\forall x\alpha_{Q}^{P}\rightarrow\forall x\beta_{Q}^{P})$ .
4. If $\psi$ is $\alpha\rightarrow\forall x\alpha$ where $x$ does not occur free in $\alpha$ , then $\psi_{Q}^{P}$ becomes $\alpha_{Q}^{P}\rightarrow\forall x\alpha_{Q}^{P}$ where $x$ does not occur free in $\alpha_{Q}^{P}$ if $Qu_{1}\ldots u_{m}$ does not contain new (free) variables that occur anywhere as a quantified variable.
5. $x=x$ remains the same.
6. $x=y\rightarrow\alpha\rightarrow\alpha'$ remains the same if $\alpha\neq Pt_{1}\ldots t_{n}$ , otherwise it becomes $x=y\rightarrow Qu_{1}\ldots u_{m}\rightarrow(Qu_{1}\ldots u_{m})'$ where we need to define the meaning of $(Qu_{1}\ldots u_{m})'$ . We will get back to this later.

Second, if $\psi$ is obtained by modus ponens, then it must have been derived from some $\delta$ and $\delta\rightarrow\psi$ , which become $\delta_{Q}^{P}$ and $\delta_{Q}^{P}\rightarrow\psi_{Q}^{P}$ , respectively, implying $\psi_{Q}^{P}$ by modus ponens, as long as $\delta_{Q}^{P}\rightarrow\psi_{Q}^{P}$ is the same as $(\delta\rightarrow\psi)_{Q}^{P}$ .

Overall, we need to ensure the following properties of substitution: in substitution of $Pt_{1}\ldots t_{n}$ by $Qu_{1}\ldots u_{m}$ , we need that a) $Qu_{1}\ldots u_{m}$ does not introduce any new (compared to $Pt_{1}\ldots t_{n}$ ) free variable $x$ that occurs anywhere in $\alpha_{t}^{x}$ or $\forall x$ , and b) the substitution is carried out in such a way that $(\alpha\rightarrow\beta)_{Q}^{P}$ is always the same as $(\alpha_{Q}^{P}\rightarrow\beta_{Q}^{P})$ , and similar for $\neg$ and $\forall$ . In particular, this concerns all axioms. We can see that the only potentially problematic axiom group is axiom group 6, where we need to ensure that $((Pt_{1}\ldots t_{n})')_{Q}^{P}$ always equals $(Qu_{1}\ldots u_{m})'$ , i.e. if $Pt'_{1}\ldots t'_{n}$ is obtained from $Pt_{1}\ldots t_{n}$ by substituting $y$ for $x$ at some places, then $(Pt'_{1}\ldots t'_{n})_{Q}^{P}$ is also obtained from $(Pt_{1}\ldots t_{n})_{Q}^{P}$ by substituting $y$ for $x$ at some places.

In fact, it seems that if, for example, the language has the equality symbol, we can do something as simple, as substituting $z=z$ for all $Pt_{1}\ldots t_{n}$ regardless of the terms, where $z$ is a variable that does not occur in any wffs in the deduction. Indeed, $z=z$ does not introduce any new free variables that were used at any places in the deduction, and any non-prime formula of axiom group 6 becomes $x=y\rightarrow z=z\rightarrow z=z$ , which is fine. If the equality is not in the language, then we may use any other predicate symbol $Q$ and substitute $Qz\ldots z$ for $Pt_{1}\ldots t_{n}$ (there has to be at least one $Q$ different from $P$ , as otherwise, there would not be any atomic formulas in which $P$ does not occur).