Witness constants and Henkin theories

Let $L$ be a set signature having at least one constant and $H$ a set of $L$-sentences. Call $H$ Henkin in the witness-axiom sense if for every existential sentence $\mathrm{\exists }x\varphi$ of $L$, some constant $c$ of $L$ satisfies

$((\mathrm{\exists }x\varphi )\to \varphi [c\mathrm{/}x])\in H\mathrm{.}$

Here $\mathrm{FV}(\varphi )\subseteq \{x\}$, and $\varphi [c\mathrm{/}x]$ replaces the free occurrences only. A constant has no free variables, so it is free for $x$ and the result is a sentence. Instances with parameters are obtained first by replacing their other free variables by closed terms; no open formula is inserted into the sentence theory. Implication has the fixed primitive expansion $\mathrm{\neg }(\psi \wedge \mathrm{\neg }\theta )$ of Terms and formulas as finite set codes.

This condition does not itself require consistency, deductive closure or decisions of all sentences. These are additional hypotheses of the later Henkin truth results. The source's term “Henkin set” packages those additional conditions with witnesses for true existential sentences; this item deliberately isolates the witness-axiom condition promised here.

For an arbitrary starting signature, adjoin a seed constant $c_{\ast }$ and then disjoint tagged layers of witness constants, naming each new constant by its stage and the existential sentence for which it is introduced. Every later layer is disjoint from earlier ones and from the original symbols. The seed guarantees at least one closed term even for an empty signature. This specifies the language expansion and possible witness axioms, without asserting their consistency or the existence of a completion.

Conventions and prerequisites: Set signatures and finite syntax strings, Free variables and free-for substitution, Theories, models and semantic consequence.