# A “formalistic” variant of the Gödel completeness theorem

A week ago I asked this at MathStackExchange, but without success.

I think, the following variant of the Gödel completeness theorem must be true, but I can't find the references. I would be grateful if specialists in logic could give me them (or enlighten me in case that something must be corrected).

A question. Joseph Shoenfield in his "Mathematical logic" (section 4.7) gives a definition of an interpretation of a theory in another theory. This notion allows to define a model of a first order theory $T$ as its interpretation in some variant of an axiomatic set theory, say, in MK (or in ZFC, I don't think that this choice is important.). (I understand that this is not the custom in mathematical logic, but I invite readers to look at this way, I will explain my motives later.)

Suppose now that we have a first order theory $T$. We define its model in MK in the way I described above, and consider the class ${\mathcal M}_T$ of all models of $T$ in MK. Each model $M\in {\mathcal M}_T$ can be considered as another first order theory, an extension by definitions of the theory MK in the sense of Kenneth Kunen's "Foundations of mathematics" (section II.15).

Moreover, we can add the symbol ${\mathcal M}_T$ into the signature of MK and the definition of ${\mathcal M}_T$ into the list of axioms of MK, and we'll get another first order theory, an extension by definition of MK. Let us denote this new first order theory by MK+${\mathcal M}_T$.

Now let us take a formula $\varphi$ in $T$. It has an analog $\varphi_M$ in each model $M\in {\mathcal M}_T$, and we can consider a formula $\varphi^*$ in MK+${\mathcal M}_T$ which states that

$\forall M\quad M\in {\mathcal M}_T\Rightarrow \varphi_M$

My question is if the following proposition is true (up to some possible specifications):

Proposition. A formula $\varphi$ is deducible in $T$ if and only if the corresponding formula $\varphi^*$ is deducible in MK+${\mathcal M}_T$.

As far as I understand, this can be considered as a "weakened analog" of the Gödel completeness theorem, and the stronger one must state the same about all the formulas $\varphi$ simultaneously.

About my motives. This comes from one of my questions at MathOverflow. I believe, there must be a way to explain mathematical logic such that the references to sets and functions appear after the axiomatic construction of the set theory (and not before, as it is now). I am not a specialist in Logic (my field is Analysis), but I am interested in this because (I teach logic sometimes, and) I am writing a textbook on university mathematics where I am planning to add a chapter about Set theory and mathematical logic. From the discussion at MathOverflow I got an impression that the idea to simplify the exposition is not hopeless, it is possible to explain everything inside the standard principle that

a mathematician can't use a term before giving a precise definition.

That is why in my text (I wrote already a draft of this chapter) Set theory preceeds mathematical logic, so that I can use the notions of set and function after their formal definition. But my problem is a lack of references. I would appreciate very much if somebody could help me with this.

EDIT 01.04.2018. Recently one of my friends showed me an article by K.Smorynski in Handbook of Mathematical Logic (edited by Jon Barwise) where he formulates a statement which he calls "the Hilbert-Bernays theorem" (Theorem 6.1.1 in volume 4) and which as far as I understand is equivalent to the following:

If a formal theory $T$ is consistent then it has an interpretation in PA.

I believe this is more or less equivalent to what Matt F. suggests in his answer:

If a formal theory $T$ is consistent then it has an interpretation in MK.

And if somebody could give me a reference to this statement (with a proof), this, I believe, will be a proper solution to what I need. Does anybody know such a reference?

• @SergeiAkbarov: no time to engage with the question proper; seems not off-topic to extend well-wishes to you and your book-project: If, as you say, you "add a chapter about set theory and mathematical logic. [..] make a textbook that includes all mathematics taught [..] first years in universities and [..] present it [..] rigorous[ly]" and even include serious logic (beyond superficial syntactic rules and 'truth-table-proofs'), then your book will be sort-of a 'first'. The neglect of logic in 'first-year' is an anomaly in mathematics currently. In the middle ages there was the 'trivium'. Oct 8 '17 at 14:43
• @PeterHeinig, actually, what I ask in this question is now the only obstacle for presenting the final variant of the book (up to the inevitable corrections of mistakes, adding pictures, and so on). Logic can be taught at the first year, at least when I was a student it was like this. Oct 8 '17 at 14:57
• I think you'll have to use some kind of encoding/Godel numbering to implement the process you describe in the first half (quite possibly this is what you had in mind, but you make it sound as if small modifications to the language already sufficed to be able to express ".. is an interpretation of $T$" in first order logic). Oct 8 '17 at 18:55
• @ChristianRemling I thought the encoding is necessary when we try to formulate this result "for all formulas $\varphi$ simultaneously", but if we fix one formula $\varphi$ we can do everything without the encoding. That is not true? Oct 8 '17 at 19:10
• @SergeiAkbarov: I'm no expert either, but I don't see how you could do this without encoding, for all sorts of reasons (the interpretations of $T$ are theories themselves, not things sitting inside one fixed theory, how do you formalize the Shoenfield definition without encoding, how do you quantify over $M$, as you do later, without encoding). Oct 8 '17 at 19:20

This proposition is equivalent to $Con(MK)$. I'll make free use of the fact that $MK$ can prove the soundness of first-order logic. I'll also use the abbreviation $M(\varphi)$ to mean the interpretation of $\varphi$ under $M$, e.g. if the language of $T$ is the language of groups, and $M$ is the interpretation of $T$ with the symmetric group $S_3$, and $\varphi = \forall x, xx=1$, then $M(\varphi) = \forall x \in S_3, xx=1$.

Suppose we have the proposition. Then the case $T=\emptyset$, $\varphi = \bot$ gives $Con(MK)$.

Now suppose we have $Con(MK)$ and want to prove the proposition.

The easy direction is that if $\varphi$ is deducible (i.e. $T \vdash \varphi$), then so is $\varphi^*$ (i.e. $MK+T^* \vdash \varphi^*$).

The harder direction is that if $\varphi$ is not deducible (i.e. $T \nvdash \varphi$), then neither is $\varphi^*$ (i.e. $MK+T^* \nvdash \varphi^*$).

First, if $\varphi$ is not deducible, then there is a model $M$ of $T+\neg \varphi$. We can prove this just by formalizing Henkin's proof of the completeness theorem. In particular $MK \vdash M(\neg\varphi^*)$.

Now, suppose $MK+T^*\vdash \varphi^*$. Then $MK\vdash M(\neg\varphi^*)$, and $MK\vdash M(\varphi^*)$. But this is impossible by the consistency of $MK$, so $MK+T^*\nvdash \varphi^*$ as desired.

• Matt, I don't understand something. Why the existense of a model for $T+\neg\varphi$ leads to the sequents $MK+{\mathcal M}_T\vdash\neg\varphi^*$ and $MK+{\mathcal M}_T\vdash\varphi^*$? Oct 9 '17 at 7:12
• @Matt F. Since $MK$ is itself a first-order theory, doesn't $MK$ + $\mathcal M_{T}$ presuppose $MK$ has a model (i.e. one can have the case where one has the theory $MK$ + $\mathcal M_{MK}$ since $\mathcal M_{T}$ is supposed to be the symbol for all models of first-order theories $T$)? Is the presupposition that $MK$ has a model problematic? Oct 9 '17 at 7:23
• (cont.) (I.e., if it can be shown that $MK$ + $\mathcal M_{ T}$ is itself a first-order theory). Oct 9 '17 at 7:33
• Matt, here is a mistake: the existence of a model for $T+\neg\varphi$ doesn't imply the deducibility of the sequent $MK+{\mathcal M}_T\vdash\neg\varphi^*$. For example, if $T$ is a formal theory of groups and $\varphi$ states that "the group is commutative", then of course there are models for $T+\neg\varphi$ (i.e. the examples of non-commutative groups), but the sequent $MK+{\mathcal M}_T\vdash\neg\varphi^*$, which means that "each group is non-commutative", is not deducible. Oct 9 '17 at 16:31
• @SergeiAkbarov, this is now corrected Oct 10 '17 at 11:24