Examples of theories with enough constants

91 Views Asked by At

A theory $\Gamma$ of $L$-sentences has enough constants if for every $L$-formula $\phi(x)$ with one free variable $x$, there is a constant $c$ such that $$\Gamma \vdash \exists x \phi(x) \rightarrow \phi(c).$$ For example, set $L = (0,1,+,\cdot)$ and $\Gamma=$ PA (Peano arithmetic; the axomization of $\mathbb{N})$, then $\Gamma$ doesn't have enough constants: for example, $\Gamma \vdash (\exists x) (x = 1 + 1)$ can't be reduced to a sentence with only one constant, because $2$ is not a constant of $L$.

However, to prove that a theory $\Gamma$ does have enough constants is a lot more difficult. So in order to figure out how to do just that, I'm looking for some examples of theories where this property holds, or some general line of thought when one encounters such a problem.

1

There are 1 best solutions below

2
On BEST ANSWER

There are few natural examples of such theories, if any. This is because having enough constants is a very restrictive condition: for instance, any theory in a finite language with no finite models does not have enough constants.

(By the way, things are a little better if we merely demand that whenever $T\vdash\exists x \varphi(x)$, there is a term $t$ such that $T\vdash \varphi(t)$.)

However, there is a process for turning any theory into a theory with enough constants. Given any theory $T$ in a language $L$, we can expand $L$ to a larger language $L'$ by adding constant symbols $c_{\psi}$ for every formula of the form $\psi\equiv\exists x\varphi(x)$ such that $T\vdash \psi$, and we can form a new theory $T'$ in the language $L$ by adding to $T$ axioms saying that $\varphi(c_{\exists x\varphi(x)})$ holds for all $L$-formulas $\varphi$. It should be clear that if we repeat this process infinitely many times, the resulting theory has enough constants. (Exercise: is doing this process just once enough?) This construction is a key part of the proof of the Completeness Theorem https://en.wikipedia.org/wiki/Gödel%27s_completeness_theorem.