And My Axiom! Insights from ‘Computability and Logic’

Foreword

Max Teg­mark’s Our Math­e­mat­i­cal Uni­verse briefly touches on a cap­ti­vat­ing, beau­tiful mys­tery:

The ar­rows in­di­cate the close re­la­tions be­tween math­e­mat­i­cal struc­tures, for­mal sys­tems and com­pu­ta­tions. The ques­tion mark sug­gests that these are all as­pects of the same tran­scen­dent struc­ture, whose na­ture we still haven’t fully un­der­stood.

The profound re­sults com­piled by the Com­putabil­ity and Logic text­book may be the first step to­wards the an­swer.

Com­putabil­ity and Logic

If this sen­tence is true, then Santa Claus is real.

As usual, I’ll ex­plain con­fu­sions I had and gen­er­ally share ob­ser­va­tions. This book is on the MIRI read­ing list.

1 Enumerability

Com­ing back to this book, I’m amazed by some of my mar­gin scrib­bles – ex­pres­sions of won­der­ment and awe at what now strike me as lit­tle more than ob­vi­ous facts (“re­la­tions are sets of or­dered pairs!”).

2 Diagonalization

Ex­er­cise 2.13 (Richard’s para­dox) What (if any­thing) is wrong with fol­low­ing ar­gu­ment?

The set of all finite strings of sym­bols from the alpha­bet, in­clud­ing the space, cap­i­tal let­ters, and punc­tu­a­tion marks, is enu­mer­able; and for definite­ness let us use the spe­cific enu­mer­a­tion of finite strings based on prime de­com­po­si­tion. Some strings amount to defi­ni­tions in English of sets of pos­i­tive in­te­gers and oth­ers do not; strike out the ones that do not, and we are left with an enu­mer­a­tion of all defi­ni­tions in English of sets of pos­i­tive in­te­gers, or, re­plac­ing each defi­ni­tion by the set it defines, and enu­mer­a­tion of all sets of pos­i­tive in­te­gers that have defi­ni­tions in English. Since some sets have more than one defi­ni­tion, there will be re­dun­dan­cies. Strike them out to ob­tain an ir­re­dun­dant enu­mer­a­tion of all sets of pos­i­tive in­te­gers that have defi­ni­tions in English. Now con­sider the set of pos­i­tive in­te­gers defined by the con­di­tion that a pos­i­tive in­te­ger be­longs to the set if and only if does not be­long to the th set in the ir­re­dun­dant enu­mer­a­tion just de­scribed.
This set does not ap­pear in that enu­mer­a­tion, so it can­not have a defi­ni­tion in English. Yet it does, and in fact we have just given such a defi­ni­tion.

My first time read­ing this ex­er­cise, I had plenty of ob­jec­tions. “Is not abu­sive to use English in place of a for­mal sys­tem? How do we even quan­tify the ex­pres­sive­ness of English, is that a thing?”, and so on. Yet, re­turn­ing with more con­text and ex­pe­rience, a few min­utes thought re­vealed to me the crux: in­for­ma­tion and enu­mer­abil­ity aren’t just defined by what is pre­sent, but by what’s not.

Let’s take a lit­tle de­tour. Con­sider the reg­u­lar ex­pres­sion ; its lan­guage is in­finite, and cer­tainly com­putable. We don’t even need a Tur­ing ma­chine to rec­og­nize it; a strictly less-ex­pres­sive finite state au­toma­ton would do just fine. And yet there are in­finite sub­sets of this lan­guage which are not at all com­putable.

Con­sider some rea­son­able en­cod­ing of a Tur­ing ma­chine and in­put . As we see later, we can enu­mer­ate all pos­si­ble Tur­ing ma­chines and in­puts (given that we first fix the alpha­bet, etc.). This means that we can num­ber the en­cod­ings. Con­sider the halt­ing set; that is, . Ex­pressed in unary, the num­bers of the en­cod­ings be­long­ing to this set is a strict sub­set of the reg­u­lar lan­guage , and yet is not com­putable (be­cause the halt­ing set is not nega­tively re­cur­sively semi-de­cid­able; i.e., we can’t say a com­pu­ta­tion won’t halt. Thus, its com­ple­ment is not enu­mer­able).

Do you see the prob­lem now?

Here, we should be care­ful with how we in­ter­pret “in­for­ma­tion”. After all, coNP-com­plete prob­lems are triv­ially Cook re­ducible to their NP-com­plete coun­ter­parts (e.g., query the or­a­cle and then negate the out­put), but many be­lieve that there isn’t a cor­re­spond­ing Karp re­duc­tion (where we do a polyno­mial amount of com­pu­ta­tion be­fore query­ing the or­a­cle and re­turn­ing its an­swer). Since we aren’t con­sid­er­ing com­plex­ity but in­stead whether it’s com­putable at all, com­ple­men­ta­tion is fine.

3 Tur­ing Computability

Tur­ing’s the­sis is that any effec­tively com­putable func­tion is Tur­ing com­putable, so that com­pu­ta­tion in the pre­cise tech­ni­cal sense we have been de­vel­op­ing co­in­cides with effec­tive com­putabil­ity in the in­tu­itive sense.

On sev­eral oc­ca­sions, the au­thors em­pha­size how the in­tu­itive na­ture of “effec­tive com­putabil­ity” ren­ders fu­tile any at­tempt to for­mal­ize the the­sis. How­ever, I’m rather in­ter­ested in for­mal­iz­ing in­tu­itive con­cepts and there­fore won­dered why this hasn’t been at­tempted. In­deed, it seems that a re­cent the­sis by Vino­gradova con­ducts a cat­e­gory-the­o­retic for­mal­iza­tion of the no­tion of ab­stract com­putabil­ity (al­though since I don’t yet know cat­e­gory the­ory, I can’t tell how re­lated it is).

4 Uncomputability

5 Aba­cus Computability

6 Re­cur­sive Functions

The part where you say “FLooPs” and give up on Tur­ing-com­plete prim­i­tive re­cur­sion when the the­o­rems don’t sup­port it.
Pre­face, The Sequents

Nate wrote:

-Zero: The func­tion that always re­turns 0.
-Suc­ces­sor: The func­tion that, given , re­turns .
-Iden­tity: Func­tions that re­turn some­thing they are given.
-Com­po­si­tion: The func­tion that performs func­tion com­po­si­tion.
Th­ese four func­tions are called the “prim­i­tive re­cur­sive” func­tions, and some time is spent ex­plor­ing what they can do. If we al­low use of a fifth func­tion:
-Min­i­miza­tion: Given , finds the ar­gu­ments for which re­turns 0.
we get the “re­cur­sive” func­tions.

How­ever, the book defines min­i­miza­tion like so:

This con­fused me for days, and I didn’t truly un­der­stand it un­til I came back sev­eral months later (i.e., now). How in the world is it effec­tively com­putable if it isn’t even defined on all in­puts?

Sup­pose I challenge you to give me a func­tion that, given a num­ber , re­turns a larger num­ber. The catch is that you aren’t al­lowed to di­rectly mod­ify – you can only use it to check whether your can­di­date solu­tion is big­ger. If you just use the bounded search pro­vided by prim­i­tive re­cur­sion, for some valid in­puts your func­tion will be wrong. If you have to start from scratch, there’s no finite num­ber of ex­po­nen­ti­a­tions or tetra­tions or su­per-duper-tetra­tions that you can in­clude which will work for all in­puts. You have to be able to do un­bounded search – for ex­am­ple, tak­ing the suc­ces­sor un­til you get a larger num­ber.

Depend­ing on the do­main, this isn’t always to­tal, ei­ther. If we’re work­ing with and I give you , you’ll in­cre­ment for­ever. Similarly, your func­tion won’t be defined on in­put . The im­por­tant part is that we’ve given an effec­tive pro­ce­dure for find­ing the solu­tion when­ever it ex­ists and for valid in­puts.

7 Re­cur­sive Sets and Relations

8 Equiv­a­lent Defi­ni­tions of Computability

Com­ing to ap­pre­ci­ate this bridge be­tween math and com­puter sci­ence was one of my most profound ex­pe­riences last year. My mind’s eye be­gan view­ing the world differ­ently. Go­ings-on came to be char­ac­ter­ized not just as in­ter­ac­tions of atomic “ob­jects”, but as the out­growth of the evolu­tion of some math­e­mat­i­cal struc­ture. As a vast and com­plex play of sorts, dis­torted by my mind and ap­prox­i­mated in spe­cific ways – some leg­ible, oth­ers not.

Most of all, a tug­ging in the back of my mind in­ten­sified, con­tinu­ally re­mind­ing me just how ig­no­rant I am about the na­ture of our world.

9 A Pré­cis of First-Order Logic: Syntax

10 A Pré­cis of First-Order Logic: Semantics

In fact, if you take Eu­clid’s first four pos­tu­lates, there are many pos­si­ble in­ter­pre­ta­tions in which “straight line” takes on a mul­ti­tude of mean­ings. This abil­ity to dis­con­nect the in­tended in­ter­pre­ta­tion from the available in­ter­pre­ta­tions is the bedrock of model the­ory. Model the­ory is the study of all in­ter­pre­ta­tions of a the­ory, not just the ones that the origi­nal au­thor in­tended.
Of course, model the­ory isn’t re­ally about find­ing sur­pris­ing new in­ter­pre­ta­tions — it’s much more gen­eral than that. It’s about ex­plor­ing the breadth of in­ter­pre­ta­tions that a given the­ory makes available. It’s about dis­cern­ing prop­er­ties that hold in all pos­si­ble in­ter­pre­ta­tions of a the­ory. It’s about dis­cov­er­ing how well (or poorly) a given the­ory con­strains its in­ter­pre­ta­tions. It’s a toolset used to dis­cuss in­ter­pre­ta­tions in gen­eral.
At its core, model the­ory is the study of what a math­e­mat­i­cal the­ory ac­tu­ally says, when you strip the in­tent from the sym­bols.

I can’t em­pha­size enough how helpful Nate’s Men­tal Con­text for Model The­ory was; the men­tal mo­tions be­hind model the­ory are a ma­jor fac­tor in my ex­cite­ment for study­ing more logic.

11 The Un­de­cid­abil­ity of First-Order Logic

12 Models

Com­ing out of lin­ear alge­bra with a “iso­mor­phism ?= bi­jec­tion” con­fu­sion, the treat­ment in this chap­ter laid the con­cep­tual foun­da­tion for my later un­der­stand­ing ho­mo­mor­phisms. That is, a key part of the “mean­ing” of math­e­mat­i­cal ob­jects lies not just in their num­ber, but in how they re­late to one an­other.

This chap­ter is also great for dis­as­so­ci­at­ing bag­gage we might naïvely as­sign to words on the page, un­der­lin­ing the role of syn­tax as poin­t­ers to math­e­mat­i­cal ob­jects.

13 The Ex­is­tence of Models

14 Proofs and Completeness

15 Arithmetization

16 Rep­re­sentabil­ity of Re­cur­sive Functions

I con­fess that upon wad­ing back into the thicket of log­i­cal no­ta­tion and ter­minol­ogy, I found my­self lost. I was frus­trated at how quickly I’d ap­par­ently for­got­ten ev­ery­thing I’d worked so hard for. After sim­mer­ing down, I went back through a cou­ple chap­ters, and found my­self rather bored by how easy it was. I hadn’t for­got­ten much at all – not be­yond the de­tails, any­ways. I don’t know whether that counts as “truly a part of me”, but I don’t think it’s rea­son­able to ex­pect my­self to mem­o­rize ev­ery­thing, es­pe­cially on the first go.

17 In­defin­abil­ity, Un­de­cid­abil­ity, Incompleteness

Per­haps the most im­por­tant im­pli­ca­tion of the [first] in­com­plete­ness the­o­rem is what it says about the no­tions of truth (in the stan­dard in­ter­pre­ta­tion) and prov­abil­ity (in a for­mal sys­tem): that they are in no sense the same.

In­deed, the no­tion of prov­abil­ity can be sub­tly differ­ent from our men­tal pro­cesses for judg­ing the truth of a propo­si­tion; within the con­fines of a for­mal sys­tem, prov­abil­ity doesn’t just tell us about the propo­si­tion in ques­tion, but also about the char­ac­ter­is­tics of that sys­tem. This must be kept in mind.

When Godel’s the­o­rem first ap­peared, with its more gen­eral con­clu­sion that a math­e­mat­i­cal sys­tem may con­tain cer­tain propo­si­tions that are un­de­cid­able within that sys­tem, it seems to have been a great psy­cholog­i­cal blow to lo­gi­ci­ans, who saw it at first as a dev­as­tat­ing ob­sta­cle to what they were try­ing to achieve. Yet a mo­ment’s thought shows us that many quite sim­ple ques­tions are un­de­cid­able by de­duc­tive logic. There are situ­a­tions in which one can prove that a cer­tain prop­erty must ex­ist in a finite set, even though it is im­pos­si­ble to ex­hibit any mem­ber of the set that has that prop­erty. For ex­am­ple, two per­sons are the sole wit­nesses to an event; they give op­po­site tes­ti­mony about it and then both die. Then we know that one of them was ly­ing, but it is im­pos­si­ble to de­ter­mine which one.

In this ex­am­ple, the un­de­cid­abil­ity is not an in­her­ent prop­erty of the propo­si­tion or the event; it sig­nifies only the in­com­plete­ness of our own in­for­ma­tion. But this is equally true of ab­stract math­e­mat­i­cal sys­tems; when a propo­si­tion is un­de­cid­able in such a sys­tem, that means only that its ax­ioms do not provide enough in­for­ma­tion to de­cide it. But new ax­ioms… might sup­ply the miss­ing in­for­ma­tion and make the propo­si­tion de­cid­able af­ter all.

In the fu­ture, as sci­ence be­comes more and more ori­ented to think­ing in terms of in­for­ma­tion con­tent, Godel’s re­sults will be seen as more of a plat­i­tude than a para­dox. In­deed, from our view­point “un­de­cid­abil­ity” merely sig­nifies that a prob­lem is one that calls for in­fer­ence rather than de­duc­tion. Prob­a­bil­ity the­ory as ex­tended logic is de­signed speci­fi­cally for such prob­lems.
~ E.T. Jaynes, Prob­a­bil­ity Theory

18 The Un­prov­abil­ity Of Consistency

19 Nor­mal Forms

20-27 [Skipped]

I found these ad­vanced top­ics rather bor­ing; the most im­por­tant was likely prov­abil­ity logic, but I in­tend to study that sep­a­rately in the fu­ture any­ways.

Fi­nal Thoughts

  • Nate Soares already cov­ered this; un­like him, I didn’t quite find it to be a breeze, al­though it cer­tainly isn’t the hard­est ma­te­rial I cov­ered last year.

  • I’m sur­prised the au­thors didn’t in­clude the the­mat­i­cally ap­pro­pri­ate re­cur­sion the­o­rem, which states that a Tur­ing ma­chine can use its source code in its own com­pu­ta­tion with­out any kind of in­finite regress (see: quines). This the­o­rem al­lows par­tic­u­larly el­e­gant proofs of the un­de­cid­abil­ity of the halt­ing prob­lem, and more gen­er­ally, of Rice’s the­o­rem.

I re­ally liked this book. In the chap­ters I com­pleted, I did all of the ex­er­cises – they seemed to be of ap­pro­pri­ate difficulty, and I gen­er­ally didn’t re­quire help.

I’ve already com­pleted Un­der­stand­ing Ma­chine Learn­ing, the first five chap­ters of Prob­a­bil­ity The­ory, and much of two books on con­fronta­tional com­plex­ity. I’m work­ing through a rather hefty ab­stract alge­bra tome and in­tend to go through two calcu­lus books be­fore an or­di­nary differ­en­tial equa­tions text. The lat­ter ma­te­rial is more recre­ational, as I in­tend to start learn­ing physics. This pro­ject will prob­a­bly be much slower, but I’m re­ally look­ing for­ward to it.

Forwards

Good math­e­mat­i­ci­ans see analo­gies be­tween the­o­rems; great math­e­mat­i­ci­ans see analo­gies be­tween analo­gies.
~ Banach

I don’t think I’m a great math­e­mat­i­cian yet by any means, but as my stud­ies con­tinue, I can’t shake a grow­ing sense of struc­ture. I’m try­ing to broaden my toolbox as much as pos­si­ble, study­ing ar­eas of math which had seemed dis­tant and un­re­lated. Yet the more I learn, the more my men­tal buck­ets col­lapse and merge.

And to think that I had once sus­pected the Void of melo­drama.

If for many years you prac­tice the tech­niques and sub­mit your­self to strict con­straints, it may be that you will glimpse the cen­ter. Then you will see how all tech­niques are one tech­nique, and you will move cor­rectly with­out feel­ing con­strained. Musashi wrote: “When you ap­pre­ci­ate the power of na­ture, know­ing the rhythm of any situ­a­tion, you will be able to hit the en­emy nat­u­rally and strike nat­u­rally. All this is the Way of the Void.”

If you are in­ter­ested in work­ing with me or oth­ers to learn MIRI-rele­vant math, if you have a burn­ing de­sire to knock the al­ign­ment prob­lem down a peg—I would be more than happy to work with you. Mes­sage me for an in­vi­ta­tion to the MIRIx Dis­cord server.