# 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.

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.

• Hold on a minute. What does it even mean to speak of prov­ing some­thing in sec­ond-or­der logic? First or­der has var­i­ous de­duc­tion sys­tems for it, which we usu­ally don’t bother to men­tion by name be­cause they’re all equiv­a­lent. How does one ac­tu­ally perform de­duc­tions in proofs in sec­ond-or­der logic? I was un­der the im­pres­sion that sec­ond-or­der logic was purely de­scrip­tive (i.e. a lan­guage to write pre­cise state­ments which then may judged true or false) and did not al­low for de­duc­tion. After all, to perform de­duc­tions about sets, one will need some sort of the­ory of how the sets work, no? And then you may as well just do set the­ory—which is af­ter all how we gen­er­ally do things...

• Proofs in sec­ond-or­der logic work the ex­act same way as proofs in first-or­der logic: You prove a sen­tence by be­gin­ning with ax­ioms, and con­struct the sen­tence us­ing in­fer­ence rules. In first-or­der logic, you have in­di­vi­d­u­als, func­tions (from in­di­vi­d­u­als to in­di­vi­d­u­als), terms, and pred­i­cates (loosely speak­ing, func­tions from in­di­vi­d­u­als to truth val­ues), but may only quan­tify over in­di­vi­d­u­als. In sec­ond-or­der logic, you may also quan­tify over pred­i­cates and func­tions. In third-or­der logic, you add func­tions of func­tions of in­di­vi­d­u­als, and, in fourth-or­der logic, the abil­ity to quan­tify over them. This con­tinues all the way up to omega-eth or­der logic (a.k.a.: higher-or­der logic), where you may use func­tions of ar­bi­trary or­ders. The ax­ioms and in­fer­ence rules are the same as in first-or­der logic.

Wait, I said noth­ing about sets above. Sets are no prob­lem: a set con­tain­ing cer­tain el­e­ments is equiv­a­lent to a pred­i­cate which only re­turns true on those el­e­ments.

I also lied about it be­ing the same as first-or­der logic—a cou­ple are added. One very use­ful ax­iom scheme is com­pre­hen­sion, which roughly means that you can find a pred­i­cate equiv­a­lent to any for­mula. You can think of this as be­ing an ax­iom schema of first-or­der logic, ex­cept that, since it can­not be stated un­til fourth-or­der logic, it con­tains no ax­ioms in first-or­der logic.

(My for­mal logic train­ing is pri­mar­ily in Church’s the­ory of types, which is very similar to higher-or­der logic [though su­perfi­cially ex­tremely differ­ent]. I prob­a­bly mixed-up ter­minol­ogy some­where in the above.)

• The com­pre­hen­sion ax­iom schema (or any other con­struc­tion that can be used by a proof checker al­gorithm) isn’t enough to prove all the state­ments peo­ple con­sider to be in­escapable con­se­quences of sec­ond-or­der logic. You can view the sys­tem you de­scribed as a many-sorted first-or­der the­ory with sets as one of the sorts, and no­tice that it can­not prove its own con­sis­tency (which can be rephrased as a state­ment about the in­te­gers, or about a cer­tain Tur­ing ma­chine not halt­ing) for the usual Goedelian rea­sons. But we hu­mans can imag­ine that the in­te­gers ex­ist as “hunks of Plato­plasm” some­where within math, so the con­sis­tency state­ment feels ob­vi­ously true to us.

It’s hard to say whether our in­tu­itions are jus­tified. But one thing we do know, prov­ably, ir­re­vo­ca­bly and for­ever, is that be­ing able to im­ple­ment a proof checker al­gorithm pre­cludes you from ever get­ting the claimed benefits of sec­ond-or­der logic, like hav­ing a unique model of the stan­dard in­te­gers. Any­one who claims to tran­scend the reach of first-or­der logic in a way that’s rele­vant to AI is ei­ther de­lud­ing them­selves, or has made a big break­through that I’d love to know about.

• The com­pre­hen­sion ax­iom schema (or any other con­struc­tion that can be used by a proof checker al­gorithm) isn’t enough to prove all the state­ments peo­ple con­sider to be in­escapable con­se­quences of sec­ond-or­der logic.

In­deed, since the sec­ond-or­der the­ory of the real num­bers is cat­e­gor­i­cal, and since it can ex­press the con­tinuum hy­poth­e­sis, an or­a­cle for sec­ond-or­der val­idity would tell us ei­ther that CH or ¬CH is ‘valid’.

(“Set the­ory in sheep’s cloth­ing”.)

• If I un­der­stand cor­rectly, you are say­ing that higher or­der logic can­not prove all the­o­rems about the in­te­gers that ZFC can. That’s a very un­in­ter­est­ing state­ment. Since higher or­der logic was proven con­sis­tent* with ZFC, it is strictly weaker. Se­cond or­der logic, is, of course, strictly weaker than 4th or­der logic, which is strictly weaker than 6th or­der logic, and so on, and is thus much weaker than higher-or­der logic.

I’ve never heard it claimed that sec­ond-or­der logic has a unique model of the stan­dard in­te­gers. Ac­tu­ally, I’ve never heard of the stan­dard in­te­gers—do you mean a unique stan­dard model of the in­te­gers? I hope not, as we ac­tu­ally can get a unique stan­dard model of the in­te­gers in a sys­tem with ma­chine-check­able proofs. See “To Truth Through Proof” by Peter An­drews. It’s omit­ted in the Google Books pre­view, but I be­lieve the proof is on page 327; i lent out my copy and can­not check. (It, nat­u­rally, does not have a unique gen­eral model, so this not of huge prac­ti­cal sig­nifi­cance.)

* I have not ac­tu­ally read that, and should not re­ally say that. How­ever, type the­ory with an ax­iom of in­finity, which is strictly stronger than type the­ory with­out an ax­iom of in­finity, which can ex­press all state­ments of higher-or­der logic, has been proven con­sis­tent. Also, any proof in higher or­der logic can be triv­ially con­verted into a proof of nth-or­der logic for some n, which can be shown con­sis­tent in (n+2)th-or­der logic.

• We don’t seem to un­der­stand each other yet :-(

If I un­der­stand cor­rectly, you are say­ing that higher or­der logic can­not prove all the­o­rems about the in­te­gers that ZFC can.

The ar­gu­ment wasn’t spe­cific to ZFC or HOL, it was in­tended to ap­ply to any sys­tem that can have a proof checker.

Ac­tu­ally, I’ve never heard of the stan­dard in­te­gers—do you mean a unique stan­dard model of the in­te­gers?

Sorry, I screwed up the word­ing there, meant to say sim­ply “unique model of the in­te­gers”. Peo­ple of­ten talk about “stan­dard in­te­gers” and “non­stan­dard in­te­gers” within mod­els of a first-or­der ax­iom sys­tem, like PA or ZFC, hence my screwup. “Stan­dard model” seems to be an un­re­lated con­cept.

I’ve never heard it claimed that sec­ond-or­der logic has a unique model of the stan­dard in­te­gers.

The origi­nal post says some­thing like that, search for “we know that we have only one (full) model”.

• The ar­gu­ment wasn’t spe­cific to ZFC or HOL, it was in­tended to ap­ply to any sys­tem that can have a proof checker.

Point­ing out the Gödelian limi­ta­tions of all sys­tems with re­cur­sively enu­mer­able ax­ioms doesn’t seem like much of crit­i­cism of the sys­tem of nth-or­der logic I men­tioned. Now I have less of an idea of what you’re try­ing to say.

By the way, I think he’s us­ing “full model” to mean “stan­dard model.” Pre­sum­ably, the stan­dard in­te­gers are the stan­dard model that satis­fies the Peano ax­ioms, while non­stan­dard in­te­gers are any other satis­fy­ing model (see http://​​en.wikipe­dia.org/​​wiki/​​Non-stan­dard_model_of_ar­ith­metic ).

• Now I have less of an idea of what you’re try­ing to say.

Not much, ad­mit­tedly :-) The in­ter­est­ing ques­tion to me is how to make a com­puter un­der­stand “in­te­gers” the way we seem to un­der­stand them. It must be pos­si­ble be­cause hu­mans are not mag­i­cal, but sec­ond-or­der logic doesn’t seem to help much.

• Com­put­ers can prove ev­ery­thing about in­te­gers that we can. I don’t see a prob­lem here.

• If the hu­man and the com­puter are us­ing the same for­mal sys­tem, then sure. But how does a hu­man ar­rive at the be­lief that some for­mal sys­tem, e.g. PA, is “re­ally” talk­ing about the in­te­gers, and some other sys­tem, e.g. PA+¬Con(PA), isn’t? Can we for­mal­ize the rea­son­ing that leads us to such con­clu­sions? Point­ing out that PA can be em­bed­ded in some larger for­mal sys­tem, e.g. ZFC, doesn’t seem to be a good an­swer be­cause that larger for­mal sys­tem will need to be jus­tified in turn, lead­ing to an in­finite regress. And any­way hu­mans don’t seem to be born with a be­lief in ZFC, so some­thing else must be go­ing on.

• We form be­liefs about math­e­mat­ics the same way we form be­liefs about ev­ery­thing else: heuris­tic-based learn­ing al­gorithms. We typ­i­cally ac­cept things based on in­tu­ition and in­duc­tive in­fer­ence un­til trained to rely on proof in­stead. There is noth­ing stop­ping a com­puter from form­ing math­e­mat­i­cal be­liefs based on statis­ti­cal in­fer­ence rather than log­i­cal in­fer­ence.

Have a look at ex­per­i­men­tal math­e­mat­ics or prob­a­bil­is­tic num­ber the­ory for some re­lated ma­te­rial.

• Say­ing “heuris­tic-based learn­ing al­gorithms” doesn’t seem to com­press prob­a­bil­ity mass very much. It feels like skip­ping over the mys­te­ri­ous part. How ex­actly do we write a pro­gram that would ar­rive at the ax­ioms of PA by us­ing statis­tics? I think if we did that, then the pro­gram prob­a­bly wouldn’t stop at PA and would come up with many other in­ter­est­ing ax­ioms, so it could be a use­ful break­through.

• Yes, but the point is that we are learn­ing fea­tures from em­piri­cal ob­ser­va­tions, not us­ing some magic de­duc­tion sys­tem that our com­put­ers don’t have ac­cess to. That may only be one bit of in­for­ma­tion, but it’s a very im­por­tant bit. This skips over the mys­te­ri­ous part in the ex­act same way that “elec­tri­cal en­g­ineer­ing” doesn’t an­swer “How does a CPU work?”—it tells you where to look to learn more.

I know far less about em­piri­cal math­e­mat­ics than about logic. The only thing along these lines I’m fa­mil­iar with is Dou­glas Le­nat’s Au­to­mated Math­e­mat­i­cian (which is only semi-au­to­mated). A quick search for “au­to­mated math­e­mat­i­cian” on Google Scholar gives a lot of more re­cent work, in­clud­ing a 2002 book called “Au­to­mated the­ory for­ma­tion in pure math­e­mat­ics.”

• But how does a hu­man ar­rive at the be­lief that some for­mal sys­tem, e.g. PA, is “re­ally” talk­ing about the in­te­gers, and some other sys­tem, e.g. PA+¬Con(PA), isn’t? Can we for­mal­ize the rea­son­ing that leads us to such con­clu­sions?

Well, hu­man be­ings are ab­duc­tive and com­pu­ta­tional rea­son­ers any­way. I think our men­tal rep­re­sen­ta­tion of the nat­u­ral num­bers is much closer to be­ing the do­main-the­o­retic defi­ni­tion of the nat­u­ral num­bers as the least fixed point of a finite set of con­struc­tors.

Note how least fixed-points and ab­duc­tive, com­pu­ta­tional rea­son­ing fit to­gether: a sen­si­ble com­plex­ity prior over com­pu­ta­tional mod­els is go­ing to as­sign the most prob­a­bil­ity mass to the sim­plest model, which is go­ing to be the least-fixed-point model, which is the stan­dard model (be­cause non­stan­dard nat­u­rals will re­quire ad­di­tional bits of in­for­ma­tion to spec­ify their con­struc­tors).

A similar pro­ce­dure, but with a coin­duc­tive (great­est-fixed-point) defi­ni­tion that in­volves nat­u­rals as pa­ram­e­ters to the data con­struc­tors, will give you the real num­bers.

• I was un­der the im­pres­sion that sec­ond-or­der logic was purely de­scrip­tive (i.e. a lan­guage to write pre­cise state­ments which then may judged true or false) and did not al­low for de­duc­tion.

There ex­ist de­duc­tive sys­tems for sec­ond or­der logic.

• Right. There ex­ist de­duc­tive sys­tems, plu­ral. Are they equiv­a­lent, like the ones for first-or­der logic are? As I un­der­stand it, If you want to do de­duc­tion in sec­ond-or­der logic, you need to spec­ify a de­duc­tive sys­tem; you can’t just do de­duc­tion in sec­ond-or­der logic alone. Whereas in first-or­der logic there’s no need to spec­ify the de­duc­tive sys­tem be­cause they’re all equiv­a­lent.

• Right. There ex­ist de­duc­tive sys­tems, plu­ral. Are they equiv­a­lent, like the ones for first-or­der logic are?

Good ques­tion. I don’t know the an­swer. If they’re not equiv­a­lent, then I see your point.

• The differ­ent de­duc­tive sys­tems de­scribed there (can’t ac­cess the link, wikiped closed) all seem the same—they differ only in the ax­ioms they use, which isn’t re­ally a differ­ence in de­duc­tive sys­tems.

• But the ques­tion is, start­ing from the same ax­ioms—not log­i­cal ax­ioms, not ax­ioms of the de­duc­tive sys­tems, but the ax­ioms of what­ever it is you’re try­ing to rea­son about—would they pro­duce the same the­o­rems?

• Wikipe­dia is ac­cessible if you dis­able JavaScript (or use a mo­bile app, or just Google cache).

• If any­one is cu­ri­ous, I’m down­vot­ing ev­ery­one in this thread—not only is this a ter­rible place to dis­cuss SOPA and black­out cir­cum­ven­tions (se­ri­ously, we can’t wait a day and get on with our lives?), there’s already a SOPA post in Dis­cus­sion.

• If any­one is cu­ri­ous, I’m down­vot­ing ev­ery­one in this thread

A policy that any­one who re­sponds to com­ments from the ‘re­cent com­ments’ page can be ex­pected to find con­temptible.

• Or just wait for the page to load, then click the Cross but­ton be­fore the black­out page loads.

The black­out is a lie.

Edit: Ap­par­ently, say­ing ‘the black­out is a lie’ offends peo­ple. I have no idea why that would be.

• The black­out is a lie.

Rather, the black­out is not an ab­solute pre­ven­tion of all ac­cess to data. They de­scribe the workarounds they provide on their about page and ex­plain the pur­pose of the in­con­ve­nience.

EDIT: Re­trac­tion only to pre­vent fur­ther gw­erniza­tion.

• The thing is… why even call it a ‘black­out’?

• The in­tent is clearly to nod in the di­rec­tion of the in­con­ve­nience of a world sud­denly with­out Wikipe­dia, with­out ac­tu­ally mak­ing us suffer such a fate.

• And, of course, if Wikipe­dia ac­tu­ally man­aged to find a way to suc­cess­fully pre­vent peo­ple from read­ing wikipe­dia con­tent for a day they would be mas­sively un­der­min­ing their own po­si­tion. A big part of the ar­gu­ment against SOPA is “it will not work to pre­vent copy­right in­fringe­ment any­way!” An ac­tual suc­cess­ful block on all wikipe­dia con­tent would amount to “OK guys, this is how it is re­ally done!”

Re­trac­tion to pre­vent fur­ther gw­erniza­tion. I LIKE this com­ment.

• Oh. It looks like I was con­fused about what Gödel’s first in­com­plete­ness the­o­rem re­ally says.

What the the­o­rem does not say:

Let PA* be a for­mal sys­tem con­tain­ing the Peano ax­ioms and maybe some other stuff. Let G be a sen­tence prov­ably equiv­a­lent to “G can­not be proved in PA*”. Then if PA* is con­sis­tent, it can’t prove G and it can’t prove Not G ei­ther.

Why doesn’t the the­o­rem say that? Be­cause we can define a sys­tem PA^ con­sist­ing of PA and an ex­tra ax­iom as­sert­ing the in­con­sis­tency of PA. PA^ is con­sis­tent in the sense that you can’t de­rive a con­tra­dic­tion from it (though note that it’s not sound, so don’t trust any re­sult that PA^ “proves”).

But PA^ can prove its ver­sion of Not G. PA^ proves that PA^ can prove any­thing; hence PA^ proves that PA^ can prove G; hence PA^ proves Not G.

So why did I feel (pos­si­bly un­fairly) that this post pro­moted my origi­nal con­fu­sion? It says this:

Peano ar­ith­metic can­not prove G with­out be­ing in­con­sis­tent; but this is pre­cisely what G is saying

G doesn’t say that “PA can­not prove G with­out be­ing in­con­sis­tent”. G says that “PA can­not prove G”. From the point of view of PA, those are not equiv­a­lent state­ments. So the sort of rea­son­ing used in the ar­ti­cle will work for PA but not for PA^ - we need to know some­thing about the sound­ness of the sys­tem we are work­ing in, not merely its con­sis­tency.

• Ex­cel­lent post! It is well-writ­ten and pushes through a pain point. Good hook, also.

You have some weird pe­ri­ods in the para­graph be­gin­ning “The last two are in­ter­est­ing...”

• They fol­low the num­bers from his list, which also have pe­ri­ods af­ter them. I think he was try­ing to show that he was refer­ring to the items from his list, as op­posed to the num­bers them­selves.

I think he should have used paren­the­ses around each num­ber in­stead.

• I think he should have used paren­the­ses around each num­ber in­stead.

I have now.

• I’ve been think­ing… How is it that we can mean­ingfully even think about full se­man­tics sec­ond or­der logic of physics is com­putable?

What I mean is… if we think we’re talk­ing about or think­ing about full se­man­tics? That is, if no ex­plicit rule fol­low­ing com­putable thingy can en­code rules/​etc that pin down full se­man­tics uniquely, what are our brains do­ing when we think we mean some­thing when we mean “ev­ery” sub­set?

I’m wor­ried that it might be one of those things that feels/​seems mean­ingful, but isn’t. That our brains can­not ex­plic­itly “pin down” that model. So… what are we ac­tu­ally think­ing we’re think­ing about when we’re think­ing we’re think­ing about full se­man­tics/​”ev­ery pos­si­ble sub­set”?

(Does what I’m ask­ing make sense to any­one? And if so… any an­swers?)

• “Every set of num­bers has a least el­e­ment” clearly does NOT define the nat­u­ral num­bers. Con­sider N U {-1}.

• “Every set of num­bers has a least el­e­ment”—along with the other, non-in­duc­tive ax­ioms of Peano ar­ith­metic.

• You might want to in­sert “non-empty”, though.

• Done!

• You should say “re­place THEM”, in that case, to re­fer to the in­finite set of ax­ioms, as op­posed to Peano Arith­metic.

• Corrected

• 16 Jan 2012 20:46 UTC
−1 points

This may be the first time I’ve up­voted a math­e­mat­ics-re­lated post on LW.