Consistent Henkin theory with language that has only one constant symbol

first-order-logiclogicpredicate-logic

as the title says, I am looking for a consistent Henking theory (either a complete or an incomplete one, or both of them) whose language has only one constant symbol (but may have more predicate- and/or function symbols).

I'd be thankful for any help or hint!

Best Answer

The example spaceisdarkgreen gave is in fact essentially the only one: take $$\varphi(x)\equiv (\exists y(y\not=c)\implies x\not=c).$$ Then $\Sigma\vdash\exists x\varphi(x)$, and so if $\Sigma$ is to have the Henkin property we must have $\Sigma\vdash\varphi(c)$. But $\Sigma\vdash \varphi(c)\iff \forall y(y=c)$. So $\Sigma$ describes the one-element structure (precisely: every model of $\Sigma$ has a single element, named by $c$).


A less trivial (in this context) notion of Henkin theory is gotten by replacing "constant symbol" by "term" in the definition: that is, requiring that for each formula $\varphi$, there be some (variable-free, or "closed") term $t$ such $$\Sigma\vdash\exists x\varphi(x)\iff\varphi(t).$$ Here, having a single constant symbol isn't too much of a problem, since we can still produce lots of terms by using function symbols.

Related Question