# How to verify satisfialibility in a model? (Confusions with Gödel's Completeness Theorem)

I just cannot believe that Gödel's Completeness Theorem is right.

Let say we fixed some first order logic with some structure. Theorem claims that for any sentence $P$ in this logic we have that

$$\vdash P\iff \mathcal{M}\vDash P \hspace{5pt}\text{for every model}\hspace{5pt}\mathcal{M}.$$ My doubts are due to the definitions of above symbols.

$\vdash P$ means that there is a formal proof of $P$ with respect to the classical logic.

$\mathcal{M}\vDash P$ means that $P$ is true in $\mathcal{M}$. Which means that $P$ treated as formula is satisfied for any assignment of values $g.$ It is denoted as $\mathcal{M},g\vDash P.$ Satisfaction as written in this fine site is defined recursively. Consider just first step of recursion, i.e. $$M,g\vDash R(\tau_1,\dots,\tau_k) \hspace{5pt}\text{iff}\hspace{5pt}(I^g_F(\tau_1),\dots,I^g_F(\tau_k))\in F(R)$$ where $R$ is some relation from structure of first order logic and $I^g_F,F$ are parts of interpretation.

I see the problem cause in some models $(I^g_F(\tau_1),\dots,I^g_F(\tau_k))\in F(R)$ may be undecidable. In fact consider $R$ to be relation $=.$ We can end up with set theoretical situation $\mathfrak{c}=\aleph_1.$ One cannot tell if this hold or not.

In short $\vdash P$ seems to be very concrete definition with clear ways of verification. On the other hand $\mathcal{M} \vDash P$ tells us nothing how check anything in model.

Please tell me what is wrong with this reasoning.

• Re: your second-to-last paragraph, I'd say that's the hallmark of a certain type of great theorem: it shows that two radically different ideas are actually the same! – Noah Schweber Jan 16 '17 at 2:24
• It follows from the recursive def'n of satisfaction, and the law of the excluded middle, that a model $M$ which is a set must satisfy $[P]$ or must satisfy $[\neg P]$ where [P] is a code for a sentence. Codes for sentences are also defined recursively without actually making sentences about sentences. it may not be possible to decide from our axioms whether or not $[P]$ is satisfiable by a set-model. – DanielWainfleet Jan 16 '17 at 2:29
• I think you're muddling the issue by thinking about what you can "check" in a model. It may be true that you're handed a very weird model and have no idea how to tell if a formula holds in it; but that's totally irrelevant to the completeness theorem. – Malice Vidrine Jan 16 '17 at 4:22
• @Hurkyl To be honest, I disagree. The fact that provability and truth get conflated is in general a sign of poor reasoning, not mathematical prescience. I think there is no reason - looking at a specific proof system - to be confident that we've "found all the necessary rules of inference" (especially when you tries to cook up a "homebrew" deduction system for a class, and one of your students points out that it's not actually complete - not that I've ever done that before :P). Remember that completeness doesn't say "there is a complete proof system," but "this one is complete". (cont'd) – Noah Schweber Jan 16 '17 at 16:48
• I find the statement "there is a complete proof system" already to be extremely counterintuitive (on the face of it, satisfiability - even granting Lowenheim-Skolem! - is only $\Sigma^1_1$), and pinning down a specific proof system as complete to be downright bizarre. Of course, one's mileage varies, but I have a lot of sympathy for the OP. – Noah Schweber Jan 16 '17 at 16:50

I would say you are right - there is no reason to expect Goedel's completeness theorem to be true!

Except for the proof.

I consider the completeness theorem to be the most counterintuitive result in basic logic, far more so than the incompleteness theorem (whose surprisingness is in fact debatable. As you say, it shows that a very concrete statement "$T\vdash \varphi$" is equivalent to a seemingly-much-more-complicated statement "Every model of $T$ satisfies $\varphi$", and the complexity of the latter is suggested by the fact that, for fixed $M$ and $\varphi$, the question "Does $M\models\varphi$?" is in general of very high complexity.

One way to think about what happens is this: telling whether every model of $T$ satisfies $\varphi$ can be easier than telling if a specific model of $T$ satisfies $\varphi$. Specific models can be quite complicated; however, every theory will also have models which are "reasonably simple" (see below for more on this). These models will often be unnatural, but they exist, and they bear on the question of whether $T\models\varphi$; and it is these models, essentially, that make the question an answerable one.

Having acknowledged that GCT is counterintuitive, let me now try to convince you that it's true.

We'll prove the contrapositive: that if $T\cup\{\neg\varphi\}$ is consistent, then we can build a model $M$ of $T$ with $M\not\models\varphi$. Note that this makes our job much easier - we only have to build one model! And even though the general problem "Does $N\models \psi$?" is extremely complicated, the specific question we're interested in ("Does $M\models\varphi$?") may not be so bad.

Here's the natural construction to look at: take the set of terms in the language of $T$, and "mod out" by $(T\cup\{\neg\varphi\})$-provable equivalence. E.g. in an appropriate theory of arithmetic, "$1+1$" and "$(1+1)\times 1$" are terms which are provably equal, so they represent the same equivalence class. It's not hard to show that the operations and relations of the language are well-defined on these equivalence classes. So there's a natural structure assigned to the theory $T\cup\{\neg\varphi\}$; if you think about it for a bit, it should become plausible that this is in fact a model of $T\cup\{\neg\varphi\}$!

. . . Of course, it's not, though. The proof isn't that simple. But the idea is right, it just needs some work. Some of this work involves improving the theory $T\cup\{\neg\varphi\}$ itself ($T\cup\{\neg\varphi\}$ might not "decide" certain important questions; alternatively, the language of $T\cup\{\neg\varphi\}$ might not "have enough terms" to build the structure we want); the other part of the work involves working with the specific properties of the provability relation "$\vdash$". (See e.g. these two questions, respectively.)

Aside: "simple" models. (No, I don't mean that kind of simplicity.) The proof of the Completeness Theorem gestured vaguely at above is a construction of a model - albeit one that is not computable. But we can ask how noncomputable it is. It turns out that it is actually not very noncomputable - namely, we have:

Suppose $T$ is a countable theory in a countable language. Then there is a model of $T$ which is low relative to $T$.

Here, "low" is a computability-theoretic property: a set $X$ is low if the halting problem relative to $X$ is no more complicated than the classical halting problem. Lowness relative to $A$ is defined similarly. By comparison, the question "Does $T$ prove $\varphi$?" is at the level of the halting problem relative to $T$; so actually, we're building a model that is simpler than the original provability question!

Note that one consequence of GCT is that questions like "Does $2^{\aleph_0}=\aleph_1$?" will never arise when trying to answer questions like "Does every model of $T$ satisfy $\varphi$?"

But this is just a result about first-order logic! For general logics, set-theoretic issues can indeed crop up.

A great example of this is second-order logic (with the standard, as opposed to Henkin, semantics; the Henkin semantics makes it essentially equivalent to first-order logic). Second-order logic allows you to quantify over relations and functions on the domain, in addition to individuals (which is what first-order logic lets you quantify over). For instance, there is a second-order sentence true in exactly the infinite structures: it looks like "There is an injective, non-surjective function," or more formally $$\exists F[\forall x, y(F(x)=F(y)\implies x=y)\wedge \exists z\forall x(F(x)\not=z)].$$ So Compactness immediately fails for second-order logic. But the one that takes the cake is:

There is a sentence $\chi$ in second-order logic, which is a validity (= true in every structure) if and only if the Continuum Hypothesis is true.

This takes a bit of work to prove; if you're interested, I'll add its construction in detail.

My point is that set-theoretic issues do indeed come up when trying to analyze the satisfaction relation for arbitrary logics; but GCT shows that first-order logic is especially nice. And this is, indeed, a very nontrivial fact!

If you're interested in comparing first-order logic with other logics, you may be interested in abstract model theory!

• I love this answer. The contrapositive approach to the proof makes everything much clearer. I am also shocked that the constructed model is low with respect to T. Can you coock up some simple example where inequality between computability is strict? I will leave aspects of second-order logic for now. My brain already hurts. – Fallen Apart Jan 16 '17 at 15:33
• @FallenApart "Can you cook up some simple example where inequality between computability is strict?" Probably, but I'm not sure I understand the question - are you asking for an example of a computable theory with no computable models, for example? (If so, ZFC is an example.) Or are you asking something else? – Noah Schweber Jan 16 '17 at 16:50

Notice that the right side says "for every model $\mathcal{M}$". If something is undecidable, then it will be true for some models and false for others. So the right side fails, and so does the left side, i.e., there is no formal proof of an undecidable statement in first-order logic. This is all as expected.

• I have problem that some sentences may be undecidible in a model. But right now after @DanSimons's answer I think we assume that any sentence in a model is true or false. (which in fact follows from assumtion that formula is sattisfied or not satissfied). – Fallen Apart Jan 16 '17 at 15:44

I see the problem cause in some models $(I^g_F(\tau_1),\dots,I^g_F(\tau_k))\in F(R)$ may be undecidable.

I think you are confusing provability with satisfaction, since for any particular model a sentence will always either be true or false. Undecidability applies to provability, since it may be the case that a sentence is true in some models and not others.

We can end up with set theoretical situation $\mathfrak{c}=\aleph_1$. One cannot tell if this hold or not.

We can tell if it holds for some particular model. Remember that Godel and Cohen together showed that CH holds in some models of ZFC and not others. Completeness simply says that this one fact is enough to prove that CH is independent of ZFC.

• "for any particular model a sentence will always either be true or false". Is it an assumption? Do we assume that sentences in a fixed model follow rules of classical logic? – Fallen Apart Jan 16 '17 at 15:40