Completeness, incompleteness, and what it all means: first versus second order logic

First or­der ar­ith­metic is in­com­plete. Ex­cept that it’s also com­plete. Se­cond or­der ar­ith­metic is more ex­pres­sive—ex­cept when it’s not—and is also in­com­plete and also com­plete, ex­cept when it means some­thing differ­ent. Oh, and full sec­ond or­der-logic might not re­ally be a logic at all. But then, first or­der logic has no idea what the re­als and nat­u­ral num­bers are, es­pe­cially when it tries to talk about them.

That was about the state of my con­fu­sion, and I set out to try and clear it up. Here I’ll try and share an un­der­stand­ing of what is re­ally go­ing on with first and sec­ond or­der logic and why they differ so rad­i­cally. It will be de­liber­ately in­for­mal, so I won’t be dis­t­in­guish­ing be­tween func­tions, pred­i­cates and sub­sets, and will be us­ing lit­tle no­ta­tion. It’ll be ex­actly what I wish some­one had told me be­fore I started look­ing into the whole field.

Mean­ingful Models

An old man starts talk­ing to you about ad­di­tion, sub­trac­tion and mul­ti­pli­ca­tion, and how they in­ter­act. You as­sume he was talk­ing about the in­te­gers; turns out he means the ra­tio­nal num­bers. The in­te­gers and the ra­tio­nals are both mod­els of ad­di­tion, sub­trac­tion and mul­ti­pli­ca­tion, in that they obey all the prop­er­ties that the old man set out. But no­tice though he had the ra­tio­nals in mind, he didn’t men­tion them at all, he just listed the prop­er­ties, and the ra­tio­nal num­bers turned out, very non-co­in­ci­den­tally, to obey them.

Th­ese mod­els are gen­er­ally taken to give mean­ing to the ab­stract sym­bols in the ax­ioms—to give se­man­tics to the syn­tax. In this view, “for all x,y xy=yx” is a se­ries of el­e­gant squig­gles, but once we have the model of the in­te­gers (or the ra­tio­nals) in mind, we re­al­ise that this means that mul­ti­pli­ca­tion is com­mu­ta­tive.

Similarly, mod­els can define the “truth” of sen­tences. Con­sider the fol­low­ing sen­tences:

(1) 2 has a mul­ti­plica­tive in­verse.
(2) There ex­ists a num­ber that squares to −1.
(3) 2 is not equal to zero.
(4) If a+b=0, then a2=b2.
(5) No num­ber is equal to zero.

Are these true? You and the old man would dis­agree on (1), with him say­ing yes and you say­ing no—your mod­els have en­abled you to at­tach truth-val­ues to the state­ment. You would both claim (2) is false, but there are other mod­els—such as the com­plex num­bers—where it is true. You would both claim (3) is true, but there are other mod­els—such as the field with two el­e­ments—where it is false. So truth is model de­pen­dent.

The last two are in­ter­est­ing, be­cause it turns out that (4) is true in ev­ery model, and (5) is false. State­ments like (4) and “not (5)” that are true in ev­ery model are called valid. Since they are in­de­pen­dent of the choice of mod­els, these state­ments are, in a cer­tain sense, true from pure syn­tax. Both these state­ment can also be de­duced purely from the ax­ioms. It would be nice if all valid state­ments could also be de­duced. But only first or­der logic al­lows this.

What would also be nice if you could agree on the model you’re us­ing. Maybe the old man could add “2 (and ev­ery non-zero num­ber) has a mul­ti­plica­tive in­verse”, giv­ing the field ax­ioms, and rul­ing your in­te­gers right out. But there are still many fields—the ra­tio­nals, the re­als, the com­plex num­bers, and many in be­tween. But maybe with a few more ax­ioms, you could re­ally nar­row thing downs, and treat the ax­ioms and the model in­ter­change­ably. But only sec­ond or­der logic al­lows this.

First or­der fun

First or­der the­o­ries are those where you can quan­tify over the ba­sic ob­jects in your the­ory, and phrase state­ments like “all Greeks en­joy danc­ing” and “there ex­ists a blind mil­lion­aire”. This dis­t­in­guishes them from sec­ond or­der the­o­ries where you can quan­tify over higher or­der ob­jects (pred­i­cates and func­tions), phras­ing sen­ti­ments like “all na­tion­al­ities are equal” or “there ex­ists a dom­i­nant so­cial class”—in first or­der logic with hu­mans as ba­sic ob­jects, na­tion­al­ity and so­cial class are pred­i­cates, and you can’t quan­tify over them. You don’t ap­pre­ci­ate how limit­ing first or­der logic can be un­til you’ve worked with it a while; nev­er­the­less, it’s a good logic to start with and pos­sesses cer­tain key prop­er­ties not shared by higher or­der log­ics. Let’s start with the most fa­mous re­sult, the in­com­plete­ness the­o­rem.

Gödel’s in­com­plete­ness theorem

Gödel’s (first) in­com­plete­ness the­o­rem, is a the­o­rem about an ar­ith­metic but also (im­plic­itly) about a model. The im­plicit model is the nat­u­ral num­bers: any ar­ith­metic that can model them suffers from the in­com­plete­ness the­o­rem. But it is not re­ally about any model, be­yond that re­quire­ment: it’s an in­trin­sic limi­ta­tion of the sys­tem.

Let’s as­sume we have the usual (first or­der) Peano ax­ioms for or­der­ing, ad­di­tion and mul­ti­pli­ca­tion. We also need an in­finity of ax­ioms to define in­duc­tion, but that isn’t as bad as it seem: given a spe­cific sen­tence, it’s easy to check whether or not it’s an ax­iom, in a fast and effi­cient way. To no­body’s sur­prise, the nat­u­ral num­ber are a model of first or­der Peano ar­ith­metic.

And in­side this model, we can con­struct the Gödel sen­tence G, which is equiv­a­lent with “there is no proof of G”. By ‘proof’, we mean a nat­u­ral num­ber n that is the Gödel num­ber that en­codes a proof of G. Ob­vi­ously, Peano ar­ith­metic can­not prove G with­out be­ing in­con­sis­tent; but this is pre­cisely what G is say­ing, so we can ac­tu­ally see that G is true. And hence that “not G” can­not be prov­able if our ar­ith­metic is con­sis­tent. This is the in­com­plete­ness the­o­rem: nei­ther G nor “not G” are prov­able, so the proof sys­tem is “in­com­plete”.

Gödel’s com­plete­ness theorem

Enough with in­com­plete­ness; what about Gödel com­plete­ness the­o­rem? Un­like the pre­vi­ous the­o­rem, this is a state­ment about about the ax­io­matic sys­tem and all of its mod­els. It sim­ply says that if a sen­tence is valid (true in ev­ery model) for a first or­der the­ory, then it can be proved from the ax­ioms. This pro­vides a bridge be­tween the se­man­tic con­cept of “true” (true in ev­ery model) and the syn­tac­tic con­cept of prov­able (can be proved by these for­mal ma­nipu­la­tions). It also im­plies that we can enu­mer­ate all the sen­tences that are valid in a first or­der sys­tem, sim­ply by enu­mer­at­ing all the proofs.

Where does this leave the Gödel sen­tence G? We’ve seen we can’t prove it from the ax­ioms, hence it can­not be true in all mod­els. There­fore there must ex­ist a model N’ of first or­der Peano ar­ith­metic in which G is false. What does that mean? G claims that “there does not ex­ist a num­ber n with (cer­tain prop­er­ties)”, so if G is false, such an n does ex­ist. Now we know (be­cause we’ve con­structed it that way) that if that n were a nat­u­ral num­ber, then those (cer­tain prop­er­ties) means that it must en­code a proof of G. Since there is no proof of G, n can­not be a nat­u­ral num­ber, but must be an ex­tra, a non-stan­dard num­ber, from be­yond our usual uni­verse. This also means that those (cer­tain prop­er­ties) do not cap­ture what we thought they did: they only mean “en­codes a proof of G” for the stan­dard nat­u­ral num­bers.

This seems some­what trou­bling, that Peano ar­ith­metic would ad­mit two dis­tinct mod­els and fail to say what we thought it said; but it gets worse.

The Löwen­heim–Skolem theorem

The Löwen­heim–Skolem the­o­rem says that if any countable first or­der the­ory (such as Peano ar­ith­metic) has an in­finite model, then it has a model for ev­ery size (“car­di­nal­ity”) of in­finity. There­fore first or­der Peano ar­ith­metic has to have many, many mod­els; at a min­i­mum, it has to have a model of same size as the re­als.

This also means that no mat­ter how much first or­der in­for­ma­tion we add to Peano ar­ith­metic, we can­not re­strict it to only be­ing about the nat­u­ral num­bers; the mod­els and the ax­ioms can never be in­ter­change­able. But it gets still worse.

Un­countable mod­els of Peano ar­ith­metic are bad enough, but it turns out that Peano ar­ith­metic also has many other countable mod­els—mod­els of same size as the nat­u­ral num­bers, but weirdly differ­ent. Weirdly is an apt sum­ma­tion of these mod­els where nei­ther mul­ti­pli­ca­tion nor ad­di­tion can be com­puted.

So first or­der Peano ar­ith­metic is not re­ally about the nat­u­ral num­bers at all—but about the nat­u­ral num­bers and all these strange countable and un­countable mod­els that we can’t re­ally de­scribe. Maybe sec­ond or­der the­o­ries will do bet­ter?

Se­cond or­der scariness

In sec­ond or­der the­o­ries, we can fi­nally do what we’ve been itch­ing to do: ap­ply the ex­is­ten­tial and uni­ver­sal quan­tifiers to pred­i­cates, func­tions, sets of num­bers and ob­jects of that ilk. We can triumphantly toss away the in­finitely many ax­ioms needed to define in­duc­tion in first or­der Peano ar­ith­metic, and re­place them with a sim­ple:

  • “Every (non-empty) set of num­bers has a least el­e­ment.”

This, as ev­ery schoolboy should know, is enough to uniquely define the nat­u­ral num­bers. Or is it?

The im­por­tance of semantics

That sen­tence re­mains a se­ries of squig­gles un­til we’ve de­cided what those squig­gles ac­tu­ally mean. This takes on an ex­tra im­por­tance in sec­ond or­der logic that it didn’t have in first or­der. When we say “ev­ery set of num­bers”, what do we mean? In terms of mean­ing and mod­els, what mod­els are we go­ing to be con­sid­er­ing?

The first idea is the ob­vi­ous one: “ev­ery set of num­bers” means, duh, “ev­ery set of num­bers”. When we spec­ify a model, we’ll give the ‘uni­verse of dis­course’, the ba­sic ob­jects (maybe the nat­u­ral num­bers or the re­als), and the quan­tifier ‘ev­ery’ will range over all pos­si­ble sub­sets of this uni­verse (ev­ery sub­set of the nat­u­ral or real num­bers). This is called the full or stan­dard se­man­tics for sec­ond or­der ar­ith­metic, and the mod­els are called full mod­els.

But note what we have done here: we have brought in ex­tra in­for­ma­tion to clar­ify what we are talk­ing about. In or­der to defined full se­man­tics, we’ve had to bring set the­ory into the mix, to define all these sub­set. This caused Quine to ac­cuse sec­ond or­der logic of not be­ing a logic at all, but a branch of set the­ory.

Also with all these Rus­sell Para­doxes fly­ing around, we might be a bit wary of jump­ing im­me­di­ately into the ‘ev­ery set’ se­man­tics. Maybe in­stead of defin­ing a model by just giv­ing the ‘uni­verse of dis­course’, we would want to also define the sub­sets we are in­ter­ested in, list­ing ex­plic­itly all the sets we are go­ing to al­low the quan­tifiers to range over.

But this could get ridicu­lous—do we re­ally want a model which in­cludes the nat­u­ral num­bers, but only al­lows us to quan­tify over the sets {1, 7, 13908}, {0} and the empty set? We can define, for in­stance, what an even num­ber is (a num­ber that is equal to two times some­thing), and so why can’t we get the set of even num­bers into our model?

Henkin semantics

We re­ally want our ‘uni­verse of quan­tifi­able sets’ to in­clude any set we can define. It turns out this some­thing we can get from in­side sec­ond-or­der logic, by us­ing the com­pre­hen­sion ax­ioms. They roughly say that “any set/​pred­i­cate we can define, is in the uni­verse of sets/​pred­i­cates we can quan­tify over”. There are in­finitely many such com­pre­hen­sion ax­ioms, cov­er­ing each defi­ni­tion.

Then Henkin se­man­tics is sec­ond-or­der logic, with all the com­pre­hen­sion ax­ioms, and no fur­ther re­stric­tions on the pos­si­ble mod­els. Th­ese ‘Henkin mod­els’ will have both a defined uni­verse of dis­course (the list of ba­sic ob­jects in the model we can quan­tify over) and a defined ‘uni­verse of sets/​pred­i­cates’ (a list of sets of ba­sic ob­jects that we can quan­tify over), with the com­pre­hen­sion ax­ioms mak­ing sure they are com­pat­i­ble. Though they are called ‘Henkin se­man­tics’, they could re­ally be called ‘Henkin syn­taxes’, since we aren’t giv­ing any ex­tra re­stric­tions on the mod­els apart from the in­ter­nal ax­ioms.

It should be noted that a full model (where the ‘uni­verse of sets’ in­clude all pos­si­ble sub­sets) au­to­mat­i­cally obeys the com­pre­hen­sion ax­ioms, since it can quan­tify over ev­ery set. So ev­ery full model in a Henkin model, and it might seem that Henkin se­man­tics are a sim­ple ex­ten­sion of full se­man­tics, and that they have a greater ‘ex­pres­sive power’. Few things could be fur­ther from the truth.

First or sec­ond or­der?

If the old man of pre­vi­ously had claimed “ev­ery num­ber is even”, and, when challenged with “3″ had re­sponded “3 is not a num­ber”, you might be jus­tified in ques­tion­ing his grasp of the mean­ing of ‘ev­ery’ and ‘num­ber’. Similarly, if he had said “ev­ery (non-empty) set of in­te­gers has a least el­e­ment,” and when challenged with “the nega­tive in­te­gers” had re­sponded “that col­lec­tion is not a set”, you would also ques­tion his use of ‘ev­ery’.

Similarly, since Henkin se­man­tics al­lows us to re­strict the mean­ing of “ev­ery set”, de­pend­ing on the model un­der con­sid­er­a­tion, state­ments such as “ev­ery set is blah” are much weaker in Henkin se­man­tics than in full se­man­tics. For in­stance, take the ax­ioms for an or­dered field, and add:

  • “Every (non-empty) bounded set has a supre­mum”

As ev­ery school­girl should know, this is enough to model the real num­bers… in full se­man­tics. But in Henkin se­man­tics, ‘ev­ery bounded set’ can mean ‘ev­ery defin­able bounded set’ and we can take the ‘defin­able re­als’ as a model: the supre­mum of a defin­able set is defin­able. And this does not in­clude all the real num­bers; for a start, the defin­able re­als are countable, so there are far fewer of them than there are re­als.

This may seem a fea­ture, rather than a bug. What are these strange, ‘non-defin­able re­als’ that clut­ter up the place; why would we want them any­way? But the defin­able re­als are just one Henkin model of these ax­ioms, there are oth­ers perfectly valid mod­els, in­clud­ing the re­als them­selves. So these ax­ioms have not al­lowed us, in Henkin se­man­tics, to pick out one par­tic­u­lar model.

This seems fa­mil­iar: the first or­der Peano ax­ioms also failed to spec­ify the nat­u­ral num­bers. The fa­mil­iar­ity is not an illu­sion: Henkin se­man­tics is ac­tu­ally a first or­der the­ory (a ‘many sorted’ one, where some classes of ob­jects have differ­ent prop­er­ties). Hence the com­plete­ness the­o­rem still ap­plies: any re­sult true in ev­ery Henkin model, can be proved from the ba­sic ax­ioms. But this is not much help if we have many mod­els, and un­for­tu­nately the Löwen­heim–Skolem the­o­rem also still ap­plies: if we have one in­finite model, we have many, many oth­ers. So not only do we have the countable ‘defin­able re­als’ and the re­als them­selves as mod­els but larger ‘hy­per­re­als’ and ‘su­per­re­als’ with many more el­e­ments to them.

Skolem’s paradox

In fact, Henkin se­man­tics can be­have much worse than stan­dard first or­der logic, as it can ex­press more. Ex­press more—but ul­ti­mately, not mean more. For in­stance, in sec­ond or­der lan­guage, we can ex­press the sen­tence “there ex­ists an un­countable set”. We could start by defin­ing an in­finite set as one with a one-to-one cor­re­spon­dence with a strict sub­set of it­self, á la Can­tor. We could define an un­countable in­finite set as one that has a sub­set that is also in­finite, but that doesn’t have a one-to-one cor­re­spon­dence with it (the sub­set is of lower car­di­nal­ity). There are other, prob­a­bly bet­ter, ways of phras­ing the same con­cept, but that will do for here.

Then ba­sic sec­ond or­der logic with Henkin se­man­tics and the ad­di­tional ax­iom “there ex­ists an un­countable set” cer­tainly has a model: the re­als, for in­stance. Then by the Löwen­heim–Skolem the­o­rem, it must have a countable model.

Wait a mo­ment there. A logic that as­serts the ex­is­tence of an un­countable set… has a countable model? This was Skolem’s para­dox, and one of his ar­gu­ments against first or­der logic. The ex­pla­na­tion for the para­dox in­volves those one-to-one cor­re­spon­dences men­tioned above. An un­countable set is an in­finite set with­out any one-to-one func­tions to any countable set. But in a Henkin model ‘any one-to-one func­tion’ means ‘any one to one func­tion on the list of al­low­able func­tions in this model’. So the ‘un­countable set’ in the countable model is, in fact, countable: it has one-to-one func­tions to other countable set. But all these func­tions are banned from the Henkin model, so the model can­not see, in­ter­nally, that that set is ac­tu­ally countable.

So we can ex­press a lot of state­ments in Henkin se­man­tics—“ev­ery bounded set has a supre­mum”, “there ex­ists an un­countable set”—but these don’t ac­tu­ally mean what we thought they did.

Full sec­ond or­der semantics

Hav­ing ac­cepted the ac­cu­sa­tions of sneak­ing in set the­ory, and the dis­turb­ing fact that we had to bring in mean­ing and se­man­tics (by ex­clud­ing a lot of po­ten­tial mod­els), rather than rely­ing on the syn­tax… what can we do with full sec­ond or­der se­man­tics?

Well, for start, fi­nally nail down the nat­u­ral num­bers and the re­als. With sec­ond or­der Peano ar­ith­metic, in­clud­ing the sec­ond or­der in­duc­tion ax­iom “ev­ery (non-empty) set of num­bers has a least el­e­ment”, we know that we have only one (full) model: the nat­u­ral num­bers. Similarly, if we have the ax­ioms for an or­dered field and toss in “ev­ery bounded set has a supre­mum”, then the re­als are the only full model that stands up.

This im­me­di­ately im­plies that full sec­ond or­der se­man­tics are not com­plete, un­like Hekin se­man­tics and first or­der the­o­ries. We can see this from the in­com­plete­ness re­sult (though don’t con­fuse in­com­plete­ness with non-com­plete­ness). Take sec­ond or­der Peano ar­ith­metic. This has a Gödel state­ment G which is true but un­prov­able. But there is only one model of sec­ond or­der Peano ar­ith­metic! So G is both un­prov­able and true in ev­ery model for the the­ory.

It may seem sur­pris­ing that com­plete­ness fails for full se­man­tics: af­ter all, it is true in Henkin se­man­tics, and ev­ery full model is also a Henkin model, so how can this hap­pen? It de­rives from the re­stric­tion of pos­si­ble mod­els: com­plete­ness means that ev­ery sen­tence that is true in ev­ery Henkin model, must be prov­able. That does not mean that ev­ery sen­tence that is true in ev­ery full model, must also be prov­able. The G sen­tence is in­deed false in some mod­els—but only in Henkin mod­els that are not full mod­els.

The lack of com­plete­ness means that the truths of sec­ond or­der logic can­not be enu­mer­ated—it has no com­plete proof pro­ce­dure. This causes some to re­ject full sec­ond or­der logic on these grounds. Others ar­gued that com­plete­ness is not the im­por­tant fac­tor, but rather de­cid­abil­ity: list­ing all the prov­able state­ments might be light en­ter­tain­ment, but what we re­ally want is an al­gorithm to be able to prove (or dis­prove) any given sen­tence. But the Church-Tur­ing the­o­rem demon­strates that this can­not be done, in ei­ther first or sec­ond or­der logic: hence nei­ther sys­tem can claim to be su­pe­rior in this re­spect.

Higher-or­der logic within full sec­ond or­der logic

Higher or­der logic is the next step up—quan­tify­ing over pred­i­cates of pred­i­cates, func­tions of func­tions. This would seem to make ev­ery­thing more com­pli­cated. How­ever there is a re­sult due to Hin­tikka that any sen­tence in full higher or­der logic can be shown to be equiv­a­lent (in an effec­tive man­ner) with a sen­tence in full sec­ond or­der logic, us­ing many-sort­ing. So there is, in a cer­tain sense, no need to go be­yond, and the im­por­tant de­bate is be­tween first or­der and full sec­ond or­der logic.

Conclusion

So, which logic is su­pe­rior? It de­pends to some ex­tent on what we need it for. Any­thing prov­able in first or­der logic can be proved in sec­ond or­der logic, so if we have a choice of proofs, pick­ing the first or­der one is the bet­ter op­tion. First or­der logic has more pleas­ing in­ter­nal prop­er­ties, such as the com­plete­ness the­o­rem, and one can pre­serve this in sec­ond or­der via Henkin se­man­tics with­out los­ing the abil­ity to for­mally ex­press cer­tain prop­er­ties. Fi­nally, one needs to make use of set the­ory and se­man­tics to define full sec­ond or­der logic, while first or­der logic (and Henkin se­man­tics) get away with pure syn­tax.

On the other hand, first or­der logic is com­pletely in­ca­pable of con­trol­ling its in­finite mod­els, as they mul­ti­ply, un­countable and gen­er­ally in­com­pre­hen­si­ble. If rather that look­ing at the logic in­ter­nally, we have a par­tic­u­lar model in mind, we have to use sec­ond or­der logic for that. If we’d pre­fer not to use in­finitely many ax­ioms to ex­press a sim­ple idea, sec­ond-or­der logic is for us. And if we re­ally want to prop­erly ex­press ideas like “ev­ery (non-empty) set has a least el­e­ment”, “ev­ery an­a­lytic func­tion is uniquely defined by its power se­ries”—and not just ex­press them, but have them mean what we want them to mean—then full sec­ond or­der logic is es­sen­tial.

EDIT: an ad­den­dum ad­dresses the prob­lem of us­ing set the­ory (a first or­der the­ory) to define sec­ond or­der logic.