Henkin Witnesses

Henkin Witnesses

There is a consistent extension ${\Sigma }^{\ast }$ of $\Sigma$ in the extended language ${\mathcal{L}}^{\ast }$ , with the following property: For every formula $\phi =\phi (v)$ of ${\mathcal{L}}^{\ast }$ (not just of $\mathcal{L}$) with at most one free variable depending on $\phi$ (here it is $v$), there is a constant $c\in \mathcal{C}$ ($c$ depending on $\phi$) such that $\exists v\phi (v)\to \phi (c)\in {\Sigma }^{\ast }.$

Proof. List all formulas of ${\mathcal{L}}^{\ast }$ (not just formulas of $\mathcal{L}$) with one free variable: ${\phi }_1,{\phi }_2,\dots ,{\phi }_n,\dots$ Define a sequence of consistent extensions of $\Sigma$, in the language ${\mathcal{L}}^{\ast }$: $\Sigma =:{\Sigma }_0^{\ast }\subset {\Sigma }_1^{\ast }\subset {\Sigma }_2^{\ast }\subset \cdots \subset {\Sigma }_n^{\ast }\subset \dots ,$ by ${\Sigma }_n^{\ast }={\Sigma }_{n-1}^{\ast }\cup \{\exists v{\phi }_n(v)\to {\phi }_n(c)\}\text{for }n\ge 1,$ where (depending on $n$), $v$ is the free variable appearing in ${\phi }_n$ and $c$ is the first constant symbol in $\mathcal{C}$ not already appearing in ${\Sigma }_k^{\ast }$ for $k<n$. This is possible since only one new sentence is added at each stage, and so only a finite number of constant symbols from $\mathcal{C}$ have already been added at any (finite) stage in the process. We claim that ${\Sigma }_n^{\ast }$ is consistent for all $n$. This is true for $n=0$ since ${\Sigma }_0^{\ast }=\Sigma$ and $\Sigma$ is consistent. Next assume ${\Sigma }_{n-1}^{\ast }$ is consistent but ${\Sigma }_n^{\ast }$ is not. Then:

& \Sigma^*_{n-1} \vdash \neg (\exists v \varphi_n(v) \to \varphi_n(c)) && (\text{Theorem 3.8.2}) \\ \therefore \quad & \Sigma^*_{n-1} \vdash \exists v \varphi_n(v) \wedge \neg \varphi_n(c) && (\text{propositional logic and modus ponens}) \\ \therefore \quad & \Sigma^*_{n-1} \vdash \exists v \varphi_n(v) \wedge \neg \varphi_n(w) && (\text{in the previous derivation, replace } c \text{ everywhere by} \\ & && \text{a variable } w \text{ not previously used, free or bound}) \\ \therefore \quad & \Sigma^*_{n-1} \vdash \exists v \varphi_n(v), \quad \Sigma^*_{n-1} \vdash \neg \varphi_n(w) && (\text{propositional logic and modus ponens}) \\ \therefore \quad & \Sigma^*_{n-1} \vdash \exists v \varphi_n(v), \quad \Sigma^*_{n-1} \vdash \forall w \neg \varphi_n(w) && (\text{generalisation}) \\ \therefore \quad & \Sigma^*_{n-1} \vdash \exists v \varphi_n(v), \quad \Sigma^*_{n-1} \vdash \neg \exists w \varphi_n(w) && (\text{definition of } \forall \text{ from } \exists) \end{align*}

But $⊢\exists v{\phi }_n(v)\to \exists w{\phi }_n(w)$ and so ${\Sigma }_{n-1}^{\ast }⊢\exists w{\phi }_n(w)$ by modus ponens. This is a contradiction. Hence ${\Sigma }_n^{\ast }$ is consistent for all $n$ and so ${\Sigma }^{\ast }:={\bigcup }_{n\ge 0}{\Sigma }_n^{\ast }$ is consistent. Finally, $\mathcal{C}$ is a set of witnesses for ${\Sigma }^{\ast }$, since any formula $\phi$ from ${\mathcal{L}}^{\ast }$ with one free variable is ${\phi }_n$ for some $n$, and so a witnessing constant $c$ for $\phi$ from $\mathcal{C}$ is introduced at the $n$-th stage in the previous procedure. That is ${\Sigma }^{\ast }⊢\exists v\phi (v)\to \phi (c),$ where for each $\phi \equiv \phi (v)$, a formula with one free variable, the constant symbol $c$ depends on the previous construction process.

Consider each formula $\psi$ in the derivation ${\Sigma }_{n-1}^{\ast }⊢\exists v{\phi }_n(v)\wedge \neg {\phi }_n(c)$. If $\psi$ contains one or more occurrences of $c$, denote $\psi$ by $\psi (c)$ and denote the changed formula in the proposed derivation for ${\Sigma }_{n-1}^{\ast }⊢\exists v{\phi }_n(v)\wedge \neg {\phi }_n(w)$ by $\psi (w)$. Now consider all the ways in which the formula $\psi$ (or $\psi (c)$) can occur (as described in Definition 2.19) in the derivation ${\Sigma }_{n-1}^{\ast }⊢\exists v{\phi }_n(v)\wedge \neg {\phi }_n(c)$, and can then change after replacing $c$ by $w$ in the proposed derivation ${\Sigma }_{n-1}^{\ast }⊢\exists v{\phi }_n(v)\wedge \neg {\phi }_n(w)$. If $\psi (c)$ is a propositional axiom (Definition 2.3) then so is $\psi (w)$, since it is similarly constructed from the same propositional tautology. If $\psi (c)$ is a logical axiom of type (2.1) then so is $\psi (w)$, since it also is constructed as in (2.1). If $\psi (c)$ is a logical axiom of type (2.2) then again so is $\psi (w)$, as it is also constructed as in (2.2). If the term $t$ contains $c$ then it will change to contain $w$, but the new $t$ will still be substitutable for $v$ as in (2.2) and footnote 1, since $w$ does not occur in $\psi (c)$ by choice of $w$. If $\psi$ is an equality axiom then it does not contain any constant symbols, including $c$, and so $\psi$ is unchanged in the proposed derivation ${\Sigma }_{n-1}^{\ast }⊢\exists v{\phi }_n(v)\wedge \neg {\phi }_n(w)$. If $\psi \in {\Sigma }_{n-1}^{\ast }$ then $c$ does not occur in $\psi$ by choice of $c$ in (3.14), and so again $\psi$ is unchanged. If $\psi (c)$ is obtained by modus ponens or generalisation from previous formulas in the derivation of ${\Sigma }_{n-1}^{\ast }⊢\exists v{\phi }_n(v)\wedge \neg {\phi }_n(c)$, then $\psi (w)$ is similarly obtained by modus ponens or generalisation from previous formulas in the derivation of ${\Sigma }_{n-1}^{\ast }⊢\exists v{\phi }_n(v)\wedge \neg {\phi }_n(w)$. We need to be a little careful here. We passed from ${\phi }_n(v)$ to ${\phi }_n(c)$ to ${\phi }_n(w)$. Moreover, $c$ and $v$ (as a free variable) do not occur in ${\phi }_n(w)$. It follows that $v$ is free for $w$ in the sense of the universal instantiation axiom (2.2) and so \vdash \forall w \neg \varphi_n(w) \to \neg \varphi_n(v) $$$$ v \text{ not free in } \varphi_n(w), \vdash \forall v (\forall w \neg \varphi_n(w) \to \neg \varphi_n(v)) $$$$ \vdash \forall w \neg \varphi_n(w) \to \forall v \neg \varphi_n(v) $$$$ \vdash \neg \forall v \neg \varphi_n(v) \to \neg \forall w \neg \varphi_n(w) \text{propositional axioms} $$$$\vdash \exists v \varphi_n(v) \to \exists w \varphi_n(w)