Suppose that we have a set $\Phi$ of sentences over a first-order language $\mathcal{L}$ and that $\Phi$ is consistent. Suppose we have another first-order language $\mathcal{L}'$ such that $\mathcal{L}'$ is an expansion of $\mathcal{L}$, in the sense that $\mathcal{L}'$ contains extra variables, constant symbols, relation symbols, and function symbols. Then is it true that $\Phi$ is consistent when considered as a set of sentences over $\mathcal{L}'$? This seems to be intuitively true since $\Phi$ does not say anything about the new variables, constants, relations, and functions.

I tried to approach it by assuming for the sake of a contradiction that $\Phi$ was inconsistent when considered as a set of sentences over $\mathcal{L}'$, so that there is a proof $\psi_1,\ldots, \psi_n=\bot$ of $\bot$ where $\psi_i$ is either an element of $\Phi$, an axiom in the language of $\mathcal{L}'$, or the result of Modus Ponens or of Generalization. If I can turn this into a proof in $\mathcal{L}$, then I would reach a contradiction; if $\psi_i$ is an element of $\Phi$, then there's nothing to do, and replacing each axiom in the language of $\mathcal{L}'$ with an appropriate axiom in the language of $\mathcal{L}$. When assuming that $\mathcal{L}$ already have infinitely-many variables, constant symbols, relation symbols, and function symbols, we can replace every one of the axioms in the language of $\mathcal{L}'$ by replacing the finitely-many symbols that show up in these axioms that are not in $\mathcal{L}$ with corresponding symbols in $\mathcal{L}$ that do not show up in any steps of the proof or $\Phi$. This produces a proof for $\bot$ from $\Phi$ in the language of $\mathcal{L}$.

However, the definition of first-order language I am using is that $\mathcal{L}=(L_1,L_2,L_3,L_4,L_5,L_6)$ where

  • $L_1$ is an infinite set of variable symbols.
  • $L_2$ is the set $\{\forall,\exists, \wedge,\vee,\neg\,\rightarrow,\leftrightarrow,\bot,\top\}$.
  • $L_3$ is the set $\{ (,),,,=\}$ (i.e. it contains the left and right parentheses, the comma, and equals sign).
  • $L_4$ is the set of constant symbols.
  • $L_5$ is a set of relation symbols, natural number pairs.
  • $L_6$ is a set of function symbols, natural number pairs.

There is nothing in these definitions for me to assume that there are infinitely-many constant symbols, relation symbols (for each arity, or natural number), or function symbols (for each arity, or natural number). For this reason, it is convenient to assume that there are infinitely-many of each of these things, or is there another approach to proving the statement.

As some final context, the question came up when trying to show that adding Henkin witnesses to a consistent set of sentences $\Phi$ over $\mathcal{L}$ by expanding both $\Phi$ and $\mathcal{L}$ produced a consistent set over the new language.

  • $\begingroup$ There is no need to replace any symbols in axioms of $\mathcal L'$, is there? $\endgroup$ – Hagen von Eitzen Aug 5 '14 at 11:13
  • $\begingroup$ @HagenvonEitzen I figured it was necessary to ensure that proof only involved sentences of $\mathcal{L}$, since there could be new axioms like $(c=c)$, where $c$ is a new constant symbol (this is an axiom in the particular system I have). Admittedly, these axioms might not add anything to a proof, but they can be stuck in proofs without affecting it, thus making the proof not be entirely written in $\mathcal{L}$. Maybe I'm missing something fundamental though $\endgroup$ – Hayden Aug 5 '14 at 11:20
  • $\begingroup$ You expand the language, but you do not add new rules or axioms; the only case (as per your comment above) is with new instances of axioms (like : $c=c$). But the purported proof of $\bot$ in the expanded language can be "converted" into a proof of $\bot$ into the "restricetd" one replacing each occurrence of a new constant with a free var not used in the proof (and there are infinitely many oof them). Thus, if $\bot$ is derivable in the expanded language, it is so also in the original one. $\endgroup$ – Mauro ALLEGRANZA Aug 5 '14 at 13:39
  • $\begingroup$ @MauroALLEGRANZA I think what you say needs a little bit more work. Suppose you have $f(c)=f(c)$ somewhere in your proof, where $f$ is only in the expanded language. Just replacing $c$ by quantifying out won't solve your problem. $\endgroup$ – UserB1234 Aug 5 '14 at 17:45
  • $\begingroup$ @DanulG - you are right: I was sloppy in my comment. I've only paraphrased Mendelson's proof (Lemma 2.15) used in the context of Henkin's construction. But I think that the argument still works for new terms (and not only constants) because we can still replace new terms used in the proof of $\bot$ in the expanded language with new variables. $\endgroup$ – Mauro ALLEGRANZA Aug 6 '14 at 14:46

As I said in my comment to Mauro, just replacing constants all over the place with variables doesn't work; Suppose you have $f(c)=f(c)$ somewhere in your proof, where $f$, a function symbol, is only in the expanded language. Now replacing $c$ by quantifying out won't solve your problem, i.e. it doesn't get rid of $f$ from the proof of the contradiction, which is what you want.

Here is where completeness kicks in: Suppose you do the usual proof of Godel's completeness theorem (A key step in this proof is, as you point out in your question, is the consistency of a set of sentences when the language is expanded by the addition of new constant symbols). Now it is easy to take a model of $\Phi$ (as an $L$-theory) and make it in to a model of $\Phi$ as an $L'$-theory by interpreting the new symbols as follows;

Additional constant symbol: interpreted by any element of the model.

Additional relation symbol: interpreted by use of the empty relation.

Additional function symbol: interpreted as a constant function.

This reflects your intuition, adding new symbols without adding new axioms means that nothing needs to change in the behavior of the model. However this gets around the question I mentioned at the beginning, i.e. getting rid of new function (and relation symbols from the proof), which as you saw isn't as easy as just quantifying things out with new variables.

In this case we can even bypass the use of the compactness theorem, which is the go to tool for model theorists in these situations. (It is pretty much the go to tool in almost all of model theory)

  • $\begingroup$ Yes, the addition of a trifecta of functional, relational, and constant symbols together does seem to add an annoyance. At least for just having constant symbols - which deals with the context of adding Henkin witnesses - Mauro's comment answers it quite well, and having this is enough to prove the Completeness Theorem using the Henkin construction, which can then be used, as you say, to finish it off. Thanks for the insights! $\endgroup$ – Hayden Aug 5 '14 at 19:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.