# Logic: the science of algorithm evaluating algorithms

“Math­e­mat­i­cal logic is the sci­ence of al­gorithm eval­u­at­ing al­gorithms.”

Do you think that this is an overly gen­er­al­iz­ing, far fetched propo­si­tion or an al­most triv­ial state­ment? Wait, don’t cast your vote be­fore the end of this short es­say!

It is hard to dis­pute that logic is the sci­ence of draw­ing cor­rect con­clu­sions. It stud­ies the­o­ret­i­cally falsifi­able rules the lead to deriva­tions which are ver­ifi­able in a finite amount of me­chan­i­cal steps, even by ma­chines.

Let’s dig a bit deeper by start­ing to fo­cus­ing on the “draw­ing cor­rect con­clu­sions” part, first. It im­plies the logic deals both with ab­stract rules: “draw­ing” and their mean­ing: “con­clu­sions”.

Logic is not just about mind­less fol­low­ing of cer­tain rules (that’s alge­bra :P) its con­clu­sions must have truth val­ues that re­fer to some “model”. Take for ex­am­ple De Mor­gan’s law:

not (a and b) = (not a) or (not b).

It can be checked for each four pos­si­ble sub­sti­tu­tions of boolean val­ues: a = false, b = false; a = false, b = true; …. If we agreed upon the stan­dard mean­ing of the log­i­cal not, or and and op­er­a­tors, then we must con­clude that the De Mor­gan’s rule is perfect. On the other hand: the similar look­ing rule

not (a and b) = (not a) and (not b)

can be eas­ily re­futed by eval­u­at­ing for the coun­terex­am­ple a = false, b = true.

Gen­er­ally: in any use­ful math­e­mat­i­cal sys­tem, log­i­cal con­clu­sions should work in some in­ter­est­ing model.

How­ever, in gen­eral, to­tal ver­ifi­a­bil­ity is way too much to ask. As Karl Pop­per pointed out: of­ten one must be satis­fied with falsifi­a­bil­ity of sci­en­tific state­ments as a crite­rion. For ex­am­ple, the fol­low­ing log­i­cal rule

not (for each x: F(x)) ⇔ ex­ists x : not F(x)

is im­pos­si­ble to check for ev­ery for­mula F. Not di­rectly check­able state­ments in­clude all those where the set of all pos­si­ble sub­sti­tu­tions is (po­ten­tially) in­finite.

This ob­ser­va­tion could be for­mal­ized by say­ing that a map­ping from ab­stract to con­crete is re­quired. This think­ing can be made pre­cise by for­mal­iz­ing fur­ther: lo­gi­ci­ans study the con­nec­tion be­tween ax­iom sys­tems and their mod­els.

But wait a minute: is not there some­thing fishy here? How could the pro­cess of for­mal­iza­tion be for­mal­ized? Is not this so kind of cir­cu­lar rea­son­ing? In fact, it is deeply cir­cu­lar on differ­ent lev­els. The most pop­u­lar way of deal­ing with this Gor­dian knot is sim­ply by cut­ting it us­ing some kind of naive set the­ory in which the top­most level of ar­gu­ments are con­cluded.

This may be good enough for ed­u­ca­tional pur­poses, but if one in the fol­low­ing ques­tions should always be asked: What is the ba­sis of those top level rules? Could there be any mis­take there? Falsifi­a­bil­ity always im­plies an (at least the­o­ret­i­cal) pos­si­bil­ity of our rules be­ing wrong even at the top­most level. Does us­ing a meta-level set the­ory mean that there is some un­ques­tion­able rule we have to ac­cept as God given, at least there?

For­tu­nately, the falsifi­a­bil­ity of ax­ioms has an­other im­pli­ca­tion: it re­quires only a sim­ple dis­crete and finite pro­cess to re­fute them: an ax­iom or rule is ei­ther falsified or not. Check­ing coun­terex­am­ples is like ex­per­i­men­tal physics: any vi­o­la­tion must be ob­serv­able and re­pro­d­u­ca­ble. There are no fuzzy, con­tin­u­ous mea­sure­ments, here. There are only dis­crete ma­nipu­la­tions. If no mis­takes were made and some coun­terex­am­ple is found, then one of the in­volved log­i­cal rules or ax­ioms had to be wrong.

Let’s squint our eyes a bit and look the at whole topic from a differ­ent per­spec­tive: In tra­di­tional view, ax­iom sys­tems are con­sid­ered to be sets of rules that al­low for draw­ing con­clu­sions. This can also be rephrased as: Ax­iom sys­tems can be cast into pro­grams that take chains of ar­gu­ments as pa­ram­e­ter and test them for cor­rect­ness.

This seems good enough for the the for­mal rules, but what about the se­man­tics (their mean­ing)?

In or­der to define the se­man­tics, there need to be map to some­thing else for­mally check­able, ruled by sym­bol­ics, which is just in­for­ma­tion pro­cess­ing, again. Fol­low­ing that path, we end up with with the an­swer: A log­i­cal sys­tem is a pro­gram that checks that cer­tain log­i­cal state­ments hold for the be­hav­ior of an­other pro­gram (model).

This is just the first sim­plifi­ca­tion and we will see how the no­tions of “check”, “log­i­cal state­ment”, and “holds” can also be dropped and re­placed by some­thing more generic and nat­u­ral, but first let’s get con­crete and let us look at the two most ba­sic ex­am­ples:

1. Log­i­cal For­mu­las: The model is the set of all log­i­cal for­mu­las given in terms of bi­nary and, or and the not func­tion. The ax­iom sys­tem con­sists of a few log­i­cal rules like the com­mu­ta­tivity, as­so­ci­a­tivity and dis­tribu­tivity of and and or, the De Mor­gan laws as well as not rule not (not a)=a. (The ex­act choice of the ax­iom sys­tem is some­what ar­bi­trary and is not re­ally im­por­tant here.) This tra­di­tional de­scrip­tion can be turned into: The model is a pro­gram that takes a boolean for­mu­las as in­put and eval­u­ates them on given (in­put) sub­sti­tu­tions. The ax­iom sys­tem can be turned as a pro­gram that given a chain of deriva­tions of equal­ity of boolean for­mu­las checks that each step some rewrit­ten in terms of one of the pre­de­ter­mined ax­ioms, “prov­ing” the equal­ity of the for­mu­las at the be­gin­ning and end of the con­clu­sion chain. Note that given two sup­pos­edly equal boolean for­mu­las (“equal­ity proven us­ing the ax­ioms”), a straight­for­ward loop around the model could check that those for­mu­las are re­ally equiv­a­lent and there­fore our an­ti­ci­pated se­man­tic re­la­tion­ship be­tween the ax­iom sys­tem and its model is clearly falsifi­able.

2. Nat­u­ral num­bers: Our model is the set of all ar­ith­metic ex­pres­sions us­ing +, *, - on nat­u­ral num­bers, pred­i­cates us­ing < and = on ar­ith­metic ex­pres­sions and any log­i­cal com­bi­na­tion of pred­i­cates. For the ax­iom sys­tem, we can choose the set of Peano ax­ioms. Again: We can turn the model into a pro­gram by eval­u­at­ing any valid for­mula in the model. The ax­iom sys­tem can again be turned into a pro­gram that checks the cor­rect­ness of logic chains of deriva­tions. Although we can not check ver­ify the cor­rect­ness of ev­ery Peano for­mula in the model by sub­sti­tut­ing each pos­si­ble value, we still can have an in­finite loop where we could ar­rive at ev­ery sub­sti­tu­tion within a finite amount of steps. That is: falsifi­a­bil­ity still holds.

The above two ex­am­ples can be eas­ily gen­er­al­ized to say­ing that: “A log­i­cal sys­tem is a pro­gram that checks that cer­tain kinds of log­i­cal state­ments can be de­rived for the be­hav­ior of an­other pro­gram (model).”

Let us sim­plify this a bit fur­ther. We can eas­ily re­place the check­ing part al­to­gether by notic­ing that given a state­ment, the ax­iom sys­tem checker pro­gram can loop over all pos­si­ble chains of deriva­tions for the state­ment and its nega­tion. If that pro­gram stops then the log­i­cal cor­rect­ness of the state­ment (or its nega­tion) was es­tab­lished, oth­er­wise it is can nei­ther be proven nor re­futed by those ax­ioms. (That is: it was in­de­pen­dent of those ax­ioms.)

There­fore, we end up just say­ing: “A log­i­cal sys­tem is pro­gram that cor­rectly eval­u­ates whether a cer­tain log­i­cal state­ment holds for the be­hav­ior of an­other pro­gram, (when­ever the eval­u­a­tor pro­gram halts.)”

Un­for­tu­nately, we still have the rel­a­tively fuzzy “log­i­cal state­ment” term in our de­scrip­tion. Is this nec­es­sary?

In fact, quan­tifiers in log­i­cal state­ments can be eas­ily re­placed by loops around the eval­u­at­ing pro­gram that check for the cor­re­spond­ing sub­sti­tu­tions. Func­tions and re­la­tions can be re­solved similarly. So we can ex­tend the model pro­gram from a sim­ply sub­sti­tu­tion method to one search­ing for some solu­tion by adding suit­able loops around it. The main prob­lem is that those loops may be in­finite. Still, they always loop over a countable set. When­ever there is a match­ing sub­sti­tu­tion, the search pro­gram will find it. We have at least falsifi­a­bil­ity, again. For ex­am­ple, the state­ment of Fer­mat’s Last The­o­rem is equiv­a­lent to the state­ment that pro­gram the searches for its solu­tion never stops.

In short: the state­ment “log­i­cal state­ment S holds for a pro­gram P” can always be re­placed by ei­ther “pro­gram P’ stops” or “pro­gram P’ does not stop” (where P’ is a suit­able pro­gram us­ing P as sub­rou­tine, de­pend­ing on the log­i­cal state­ment). That is we fi­nally ar­rive at our origi­nal state­ment:

“Math­e­mat­i­cal logic is the sci­ence of al­gorithm eval­u­at­ing al­gorithms [with the pur­pose mak­ing pre­dic­tions on their (stop­ping) be­hav­ior.]”

Sim­ple enough, isn’t it? But can this be ar­gued back­ward? Can the stop­ping prob­lem always be re-cast as a model the­o­retic prob­lem on some model? In fact, it can. Logic is pow­er­ful and the se­man­tics of the the work­ing of a pro­grams is eas­ily ax­io­m­a­tized. There re­ally is a rel­a­tively straight­for­ward one-to-one cor­re­spon­dence be­tween model the­ory and al­gorithms tak­ing the pro­grams as ar­gu­ments to pre­dict their (stop­ping) be­hav­ior.

Still, what can be gained any­thing by hav­ing such an al­gorith­mic view?

First of all: it has a re­mark­able sym­me­try not ex­plic­itly ap­par­ent by the tra­di­tional view point: It is much less im­por­tant which pro­gram is the model and which is the “pre­dic­tor”. Pre­dic­tion goes both ways: the roles of the pro­grams are mostly in­ter­change­able. The dis­tinc­tion be­tween con­crete and ab­stract van­ishes.

Another point is the con­cep­tual sim­plic­ity: the need for a as­sum­ing a meta-sys­tem van­ishes. We treat the al­gorith­mic be­hav­ior as the sin­gle source of ev­ery­thing and look for sym­met­ric cor­re­la­tions be­tween the be­hav­ior of pro­grams in­stead of pos­tu­lat­ing higher and higher lev­els of meta-the­o­ries.

Also, the al­gorith­mic view has quite a bit of sim­plify­ing power due to its gen­er­al­ity:

Tur­ing’s halt­ing the­o­rem is con­cep­tu­ally very sim­ple. (Seems al­most too sim­ple to be in­ter­est­ing.) Goedel’s the­o­rem, on the other hand, looks more tech­ni­cal and in­volved. Still, by the above cor­re­spon­dence, Tur­ing’s halt­ing the­o­rem is ba­si­cally just a more gen­eral ver­sion Goedel’s the­o­rem. By the cor­re­spon­dence be­tween the al­gorith­mic and log­i­cal view, Tur­ing’s the­o­rem can be trans­lated to: ev­ery generic enough ax­iom sys­tem (cor­re­spond­ing to a Tur­ing com­plete lan­guage) has at least one un­de­cid­able state­ment (in­put pro­gram, for which the check­ing pro­gram does not stop.) The only tech­ni­cally in­volved part of Goedel’s the­o­rem is to check that its cor­re­spond­ing pro­gram is Tur­ing com­plete. How­ever, hav­ing the right goal in mind, it is not hard to check at all.

• You are look­ing for essences at ev­ery turn, ask what cer­tain things “re­ally are”, but the world doesn’t work like that. There are of­ten mul­ti­ple ex­pla­na­tions (in­ter­pre­ta­tions), none of them “more real” than the other. And in math that is more ap­par­ent than el­se­where, so mor­phisms of ev­ery kind be­tween all kinds of struc­tures get in­tro­duced to de­scribe par­tic­u­lar ex­pla­na­tions, re­la­tions be­tween differ­ent things that show in what way do prop­er­ties of one thing tell some­thing about the other.

• Ex­actly. There are enough con­nec­tions within math­e­mat­ics that al­most any field can be seen as an ab­struse de­vel­op­ment of al­most any other field, and in­deed, most math­e­mat­i­ci­ans have the be­lief that their field is the most truly fun­da­men­tal one. What we just saw here is a com­puter sci­en­tist look­ing to sub­orn math­e­mat­i­cal logic as a spe­cial case; nat­u­rally, the op­po­site in­ter­pre­ta­tion is just as valid.

• You seem to be limit­ing your­self to countably in­finite mod­els when you say you can (pos­si­bly in­finitely) loop over all the items in check­ing quan­tifi­ca­tions.

I like your theme/​in­tu­ition (aes­thet­i­cally; in terms of it bear­ing fruit, I don’t see it yet), but the meat of this post is rid­dled with un­clear (to me) state­ments. It would help if we could see a more for­mal ver­sion.

• I ex­pected the re­ac­tion with the countably in­finite mod­els, but I did not ex­pect it to be the first. ;)

I wanted to get into that in the write up, but I had to stop at some point. The ar­gu­ment is that in or­der to have sci­en­tific the­o­ries, we need to have falsifi­a­bil­ity, which means that this always nec­es­sar­ily deals with a dis­crete pro­jec­tion of the phys­i­cal world. On the other hand so far ev­ery dis­crete man­i­fes­ta­tion of phys­i­cal sys­tems seemed to be able to be mod­el­led by Tur­ing ma­chines. (This as­sump­tion is called the Church the­sis.) If you add these two, then you ar­rive by the above con­clu­sion.

Another rea­son for it not be­ing a prob­lem is that ev­ery (first or­der) ax­iom sys­tem has a countable model by the the­o­rem of Lowen­heim-Skolem. (Yes, even the the­ory of real num­bers have a countable model, which is also known as the Skolem para­dox.)

Ac­tu­ally, I don’t think that the tech­ni­cal con­tent of the write-up is novel, it is prob­a­bly some­thing that was already clear to Tur­ing, Church, Goedel and von Neu­mann in the 40-50ies. IMO, the take­away is a cer­tain, more prag­matic, way of think­ing about logic in the age in­for­ma­tion pro­cess­ing, in­stead of stick­ing to an out­dated in­tu­ition. Also the ex­plicit recog­ni­tion that the do­mains of math­e­mat­i­cal logic and AI are much more di­rectly con­nected than it would seem naively.

• I know that ma­te­rial, but couldn’t figure out how your in­for­mal de­scrip­tions map to it in ev­ery case. (When fol­low­ing a proof, I like to make sure I un­der­stand ev­ery step, and fix prob­lems be­fore pro­ceed­ing). If this isn’t in­tended as new, then I won’t sweat it.

• The over­all mes­sage is not re­ally new tech­ni­cally, but its philo­soph­i­cal im­pli­ca­tions are some­what sur­pris­ing even for math­e­mat­i­ci­ans. In gen­eral, look­ing at the same thing from differ­ent an­gles to helps to get ac­quire more thor­ough un­der­stand­ing even if it does not nec­es­sar­ily provide a clear short term benefit.

A few years ago, I chat­ted with a few very good math­e­mat­i­ci­ans who were not aware (rel­a­tively straight­for­ward) equiv­alence be­tween the the­o­rems of Tur­ing and Goedel, but could see it within a few min­utes and had no prob­lem grasp­ing the the in­her­ent, nat­u­ral con­nec­tion be­tween log­i­cal sys­tems and pro­gram eval­u­at­ing al­gorithms.

I think, that there is quite a bit of mys­ti­cism and mis­con­cep­tion re­gard­ing math­e­mat­i­cal logic, set the­ory, etc. by the gen­eral pub­lic. I think that it is valuable to put them in a con­text that clar­ifies their real, in­her­ently al­gorith­mic na­ture. It may be also helpful for clean­ing up one’s own world view.

I am sorry if my ac­count was un­clear at points and I am glad to provide clar­ifi­ca­tion to any un­clear points.

• An ad­mirable re­sponse.

Here’s the first place you lost me:

In or­der to define the se­man­tics, there need to be map to some­thing else for­mally check­able, ruled by sym­bol­ics, which is just in­for­ma­tion pro­cess­ing, again. Fol­low­ing that path, we end up with with the an­swer: A log­i­cal sys­tem is a pro­gram that checks that cer­tain log­i­cal state­ments hold for the be­hav­ior of an­other pro­gram (model).

This isn’t pre­cise enough for me to agree that it’s true. Is it a claim? A new defi­ni­tion?

Next:

For the ax­iom sys­tem, we can choose the set of Peano ax­ioms.

I took “ax­iom sys­tem” to mean a set of ax­ioms and rules for de­duc­ing their con­se­quences (I know you prob­a­bly mean the usual first-or­der logic de­duc­tion rules).

Although we can not check ver­ify the cor­rect­ness of ev­ery Peano for­mula in the model by sub­sti­tut­ing each pos­si­ble value, we still can have an in­finite loop where we could ar­rive at ev­ery sub­sti­tu­tion within a finite amount of steps.

What do you mean? Are you talk­ing about some­thing other pro­cess than the proof check­ing pro­gram?

I’ll wait for clar­ifi­ca­tions on those points be­fore pro­ceed­ing.

• In or­der to define the se­man­tics,… This isn’t pre­cise enough for me to agree that it’s true. Is it a claim? A new defi­ni­tion?

First: sorry for the bad gram­mar! Let me start with rephras­ing the first sen­tence a bit more clearly:

“In or­der to define se­man­tics, we need to define a map be­tween the logic to the model ….”

It is cor­rect that this de­scrip­tion con­strains se­man­tics to maps be­tween sym­bol­i­cally check­able sys­tems. Physi­cists may not agree with this view and could say: “For me, se­man­tics is a map­ping from a for­mal sys­tem to a phys­i­cal sys­tem that could be con­tin­u­ous or to which the Church the­sis does not hold.”

Model the­o­ret­i­ci­ans, how­ever, define their no­tion of se­man­tics be­tween log­i­cal sys­tems only. There­fore I think I am in a pretty good agree­ment with their nomen­cla­ture.

The mes­sage is that even if we con­sider a con­tin­u­ous sys­tem math­e­mat­i­cally (for ex­am­ple real num­ber), only those of its as­pects mat­ter which can be ver­ified by cap­tured by dis­crete in­for­ma­tion pro­cess­ing method. What I ar­gue here is that this im­plicit pro­jec­tion to the dis­crete is best made ex­plicit if view it from an al­gorith­mic point of view.

Although we can not check ver­ify the cor­rect­ness … .. What do you mean? Are you talk­ing about some­thing other pro­cess than the proof check­ing pro­gram?

It is more model check­ing: Given a state­ment like “For each x: F(x)”, since your in­put do­main is countable, you can just loop over all sub­sti­tu­tions. Although this pro­gram will not ever stop if the state­ment was true, but you can at least re­fute it in a finite num­ber of steps if the state­ment is false. This is why I con­sider falsifi­a­bil­ity im­por­tant.

I agree that there is also a culprit: this is only true for sim­ple ex­pres­sions if you have only each quan­tifiers. For ex­am­ple, but not for more com­plex log­i­cal ex­pres­sions like the twin primes con­jec­ture, which can be cast as:

fore­ach x: ex­ists y: prime(y) and prime(y+2)

Still this ex­pres­sion can be cast into the form: “T(x) halts for ev­ery in­put x.”, where T is the pro­gram that searches for the next pair of twin primes both big­ger than n.

But what about longer se­quences of quan­tifier, like

f = fore­ach a: ex­ists b: fore­ach c: ex­ists d: …. F(a,b,c,d,...)

Can this still be casted into the form “T(x) halts for ev­ery in­put x”? If it would not then we needed to add an­other layer of logic around the stop­ping of Tur­ing ma­chine which would defeat our origi­nal pur­pose.

In fact, there is a neat trick to avoid that: You can define a pro­gram T’(n) which takes a sin­gle nat­u­ral num­ber and checks the val­idity (not f) for ev­ery sub­sti­tu­tion of to­tal length < n. Then f is equiv­a­lent to the statate­ment: T’(n) does halt for ev­ery nat­u­ral num­ber n.

Which means we man­age to hide the cas­cade of quan­tifiers within al­gorithm T’. Cool, hugh?

• Logic is not just about mind­less fol­low­ing of cer­tain rules (that’s alge­bra :P) its con­clu­sions must have truth val­ues that re­fer to some “model”.

Seems like it would make ex­actly as much sense to say the op­po­site; what use is alge­bra if the quan­tities in your equa­tion don’t re­fer to some model?

Of course, if you’re ex­plor­ing alge­bra for its own ends, you can just leave ev­ery­thing ab­stract… but then again, you can also do that with logic.

• I kept wait­ing for the ra­tio­nal­ity-re­lated punch­line for this post, but it never came.

• The best ar­ti­cle on LW so far.