8

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?

Sergei Akbarov
  • 7,274
  • @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'. – Peter Heinig Oct 08 '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. – Sergei Akbarov Oct 08 '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). – Christian Remling Oct 08 '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? – Sergei Akbarov Oct 08 '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). – Christian Remling Oct 08 '17 at 19:20
  • @ChristianRemling I don't see a problem. Take for example the "formal group theory" as $T$. It's easy to define the class ${\mathcal M}_T$ "of all groups" in MK (as triples $M=(G,\cdot,1)$ with the necessary properties). Then we can take as $\varphi$ a statement like "the group is commutative" (this is not true, but this is a formula in $T$). There is no problem in formulating $\varphi$ in the language of MK for all elements of the class ${\mathcal M}_T$. – Sergei Akbarov Oct 08 '17 at 19:26
  • I don't need the encoding, but I suspect that perhaps there are no other references, except those where what I am asking about is deduced as a corollary from "the general Gödel theorem" (formulated with the help of the encoding). I would be grateful for these references as well. Of course, I would prefer the texts where what I need is proved directly, without encoding, but if nobody thought about this in the way I describe, any references will do, including the intricated ones. – Sergei Akbarov Oct 08 '17 at 20:10
  • Are you looking for the conservativity of extensions by definitions? These are meta-theorems which say that adding new function symbols and relations that name objects proved to exist uniquely is harmless. Logicians wrongly make everyone believe that this means that a proper theory of definitions has no place in logic. I wrote a little program that applies the theorems to unfold the axioms of set theory just in terms of $\in$, see here (PDF at the end). – Andrej Bauer Oct 08 '17 at 23:00
  • @AndrejBauer I am afraid, I didn't understand your point. Is this related to what I am asking about? – Sergei Akbarov Oct 09 '17 at 07:27
  • No, it's related to the side comments you made about writing a textbook. – Andrej Bauer Oct 09 '17 at 07:33
  • @AndrejBauer, perhaps, we could discuss this in a chat or anywhere else. What you say is interesting, but I must say I don't understand it. In particular, this statement: "Logicians wrongly make everyone believe that this means that a proper theory of definitions has no place in logic." – Sergei Akbarov Oct 09 '17 at 07:38
  • Sure, how do we start a chat? – Andrej Bauer Oct 09 '17 at 08:16
  • Andrej, I don't know how this is organized here. And we should also agree when we will start this chat. Actually, I am busy today until evening. – Sergei Akbarov Oct 09 '17 at 08:33
  • Let us continue this discussion in chat. – Andrej Bauer Oct 09 '17 at 08:39
  • The chat works, and it need not be interactive, although that is desirable. Maybe in the chat you can write down a time when we could meet and I will try to be there. – Andrej Bauer Oct 09 '17 at 08:40
  • It might be clearer to call these "syntactic models", going through the question text to replace "model" with "syntactic model" as appropriate. –  Oct 09 '17 at 11:09
  • @ChristianRemling I understood your doubts: if the number of axioms of the theory $T$ is infinite, then we need encoding in the Gödel style. My reasoning works only for finite number of axioms (and finite signature). – Sergei Akbarov Oct 09 '17 at 16:25
  • @SergeiAkbarov: In fact, I had more basic concerns, but as I said, I didn't really think it through and you may well be right. In your example of groups, it's straightforward to say everything in terms of sets (one set $G$, and a subset of $G\times G\times G$, giving the group operation), but it doesn't seem so clear (to me) how you do this for interpretations. – Christian Remling Oct 09 '17 at 16:33
  • Christian, I think, this example with groups can be a guiding idea: just try to express all what you need in the language of MK, and you'll see that everything works. You can define the class ${\mathcal M}_T$ of all groups (like I told before, as triples with the necessary properties; it is easy because in almost all books groups are defined like this, not as a first order theory but as sets with a supplementary structure). But this is easy only when the set of axioms (and the signature) is finite. If it is infinite, then (formally) we need coding. – Sergei Akbarov Oct 09 '17 at 16:43
  • What is the background theory to be used when proving your proposition? PA? ZFC? KM? – Joel David Hamkins Apr 01 '18 at 14:08
  • @Joel, I am trying to use the Morse-Kelley theory, because I need it further for the purposes of Analysis (ZFC and the others are not sufficient for me). – Sergei Akbarov Apr 01 '18 at 14:19
  • So you use MK both as the background theory and as an object theory here? – Joel David Hamkins Apr 01 '18 at 14:20
  • @Joel, excuse me, perhaps I did not understand. I consider an arbitrary first order theory $T$ and I am trying to prove that a formula $\varphi$ is deducilble in $T$ iff it is deducible in each interpretation of $T$ in MK. What is object and what is background here? – Sergei Akbarov Apr 01 '18 at 14:24
  • Exactly. That proposition, which you stated in the question and which you have just stated in your comment---in which theory are we to prove this proposition? That is the background or meta theory. – Joel David Hamkins Apr 01 '18 at 15:01
  • Joel, I thought we are in MK. We construct the class ${\mathcal M}_T$ of models for $T$ in MK, and after that everything happens in MK (or if you wish, in $MK+{\mathcal M}_T$). – Sergei Akbarov Apr 01 '18 at 16:12
  • Well, clearly you need Con(MK) in the meta theory to have any chance at proving the proposition. – Joel David Hamkins Apr 02 '18 at 14:10
  • From my perspective, your question is all about the interaction of the meta-theory and the object theory and the way that the background theory is treated as an object theory, and it seems important to set things up more carefully and precisely in order to have a meaningful question. – Joel David Hamkins Apr 02 '18 at 14:13

1 Answers1

2

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.

Sergei Akbarov
  • 7,274
  • 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^$? – Sergei Akbarov Oct 09 '17 at 07: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? – Thomas Benjamin Oct 09 '17 at 07:23
  • (cont.) (I.e., if it can be shown that $MK$ + $\mathcal M_{ T}$ is itself a first-order theory). – Thomas Benjamin Oct 09 '17 at 07: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. – Sergei Akbarov Oct 09 '17 at 16:31
  • @SergeiAkbarov, this is now corrected –  Oct 10 '17 at 11:24
  • @MattF., I only now understood what you said. (After correcting your answer.) But now a question arises about a reference for this: "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." Do you know it? – Sergei Akbarov Apr 01 '18 at 13:42
  • @SergeiAkbarov, it’s a straightforward formalization: the theory T is a set of strings of symbols, and the elements of the model M are also strings of symbols. I have no research-level reference, but someone unfamiliar with the basic formalization required could start with https://en.m.wikipedia.org/wiki/Implementation_of_mathematics_in_set_theory. –  Apr 01 '18 at 18:01
  • Matt, I must either find a reference which will satisfy the publisher, or prove this myself. Of course, I would prefer the first, and that is why (being not a specialist in this field) I am postponing this work with accurate proof, but an amazing thing is that for several months I can't find such a reference. :) – Sergei Akbarov Apr 01 '18 at 18:08
  • Ok. But a reference on basic formalization is a question for MathStackExchange rather than MathOverflow. –  Apr 01 '18 at 18:14
  • OK, I'll ask them if there will not be answer here. – Sergei Akbarov Apr 01 '18 at 18:26