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

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

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

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

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

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

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

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

For­mal­iz­ing the in­tu­itive no­tion of effec­tive com­putabil­ity was ex­actly what Tur­ing was try­ing to do when he in­tro­duced Tur­ing ma­chines, and Tur­ing’s the­sis claims that his at­tempt was suc­cess­ful. If you come up with a new for­mal­iza­tion of effec­tive com­putabil­ity and prove it equiv­a­lent to Tur­ing com­putabil­ity, then in or­der to use this as a proof of Tur­ing’s the­sis, you would need to ar­gue that your new for­mal­iza­tion is cor­rect. But such an ar­gu­ment would in­evitably be in­for­mal, since it links a for­mal con­cept to an in­for­mal con­cept, and there already have been in­for­mal ar­gu­ments for Tur­ing’s the­sis, so I don’t think there is any­thing re­ally fun­da­men­tal to be gained from this.

• Another way of putting it: you can’t pos­si­bly know that there isn’t some de­vice out in the uni­verse that lets you do more pow­er­ful things than your model (eg. a de­vice that can tell you whether an ar­bi­trary Tur­ing ma­chine halts), so it can never be proven that your model cap­tures real-world com­putabil­ity.

• Be care­ful stat­ing what physics can’t prove.

• Fwiw, I dis­agree with the frame of that post as well.

I’m happy to agree that you can prove that your model cap­tures real-world com­putabil­ity un­der a par­tic­u­lar for­mal­iza­tion of physics.

• Con­sider the halt­ing set; … is not enu­mer­able /​ com­putable.

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 enu­mer­able at all, com­ple­men­ta­tion is fine.

You’re us­ing the word “enu­mer­able” in a non­stan­dard way here, which might in­di­cate that you’ve missed some­thing (and if not, then per­haps at least this will be use­ful for some­one else read­ing this). “Enu­mer­able” is not usu­ally used as a syn­onym for com­putable. A set is com­putable if there is a pro­gram that de­ter­mines whether or not its in­put is in the set. But a set is enu­mer­able if there is a pro­gram that halts if its in­put is in the set, and does not halt oth­er­wise. Every com­putable set is enu­mer­able (since you can just use the out­put of the com­pu­ta­tion to de­cide whether or not to halt). But the halt­ing set is an ex­am­ple of a set that is enu­mer­able but not com­putable (it is enu­mer­able be­cause you can just run the pro­gram coded by your in­put, and halt if/​when it halts). Enu­mer­able sets are not closed un­der com­ple­men­ta­tion; in fact, an enu­mer­able set whose com­ple­ment is enu­mer­able is com­putable (be­cause you can run the pro­grams for the set and its com­ple­ment in par­allel on the same in­put; even­tu­ally one of them will halt, which will tell you whether or not the in­put is in the set).

The dis­tinc­tion be­tween Cook and Karp re­duc­tions re­mains mean­ingful when “polyno­mial-time” is re­placed by “Tur­ing com­putable” in the defi­ni­tions. Any set that an enu­mer­able set is Tur­ing-Karp re­ducible to is also enu­mer­able, but an enu­mer­able set is Tur­ing-Cook re­ducible to its com­ple­ment.

The rea­son “enu­mer­able” is used for this con­cept is that a set is enu­mer­able iff there is a pro­gram com­put­ing a se­quence that enu­mer­ates ev­ery el­e­ment of the set. Given a pro­gram that halts on ex­actly the el­e­ments of a given set, you can con­struct an enu­mer­a­tion of the set by run­ning your pro­gram on ev­ery in­put in par­allel, and adding an el­e­ment to the end of your se­quence when­ever the pro­gram halts on that in­put. Con­versely, given an enu­mer­a­tion of a set, you can con­struct a pro­gram that halts on el­e­ments of the set by go­ing through the se­quence and halt­ing when­ever you find your in­put.

• Thanks, my ter­minol­ogy was a lit­tle loose. What I was try­ing to hint at is that some of the para­dox’s cul­ling op­er­a­tions re­quire un­com­putable tests of English sen­tences, and that the reg­u­lar­ity of the origi­nal lan­guage doesn’t de­ter­mine the sta­tus of its sub­sets.

• But that’s not what the puz­zle is about. There is noth­ing about com­putabil­ity in it. It is sup­posed to be a para­dox along Rus­sell’s set of all sets that don’t con­tain them­selves.

The re­sponse about for­mal­iz­ing ex­actly what counts as a set defined by an English sen­tence is ex­actly cor­rect.

• But there are more ob­jec­tions; even if “com­putabil­ity” isn’t ex­plic­itly men­tioned in the prob­lem, it’s still pre­sent. Are the sets “the sin­gle­ton set con­tain­ing 1 if and only if ma­chine halts on in­put ” and “the sin­gle­ton set con­tain­ing 1” the same? Even if we grant a pro­ce­dure for figur­ing out what counts as a set, we can’t even com­pute which sen­tences are du­pli­cates.

• That still doesn’t make com­putabil­ity rele­vant un­til one in­tro­duces it de­liber­ately. Com­pare to weaker no­tions than com­putabil­ity, like com­putabil­ity in polyno­mial time. Com­putabil­ity the­ory also com­plains the same once we have ex­plic­itly made defin­abil­ity sub­jec­tive, and should have no more log­i­cal prob­lems.

• I don’t think I un­der­stand this line of ob­jec­tion; would you be will­ing to ex­pand?

• Say­ing that the prob­lem is about com­putabil­ity be­cause there is no com­putable solu­tion proves too much: I could re­ply that it is about com­plex­ity the­ory be­cause there is no polyno­mial-time solu­tion. (In fact, there is no solu­tion.)

We can build some­thing like a solu­tion by spec­i­fy­ing that de­scrip­tions must be writ­ten in some for­mal lan­guage that can­not de­scribe its own set of de­scrib­ables, then use a more pow­er­ful for­mal lan­guage to talk about that pre­vi­ous lan­guage’s set. For pow­er­ful enough lan­guages, that’s still not com­putable, though, so com­putabil­ity the­ory wouldn’t no­tice such a solu­tion, which speaks against look­ing at this through the lens of com­putabil­ity the­ory.

• Sure, but how do we get the fi­nal set, then? The para­dox ad­dresses the reader in the im­per­a­tive, im­ply­ing one can fol­low along with some effec­tive pro­ce­dure to trim down the set. Yet if Tur­ing’s the­sis is to be be­lieved, there is no such pro­ce­dure, no fi­nal set, and there­fore no para­dox.

• Com­putabil­ity is just \Delta^0_1 defin­abil­ity. There are plenty of other no­tions of defin­abil­ity you could try to cash out this para­dox in terms of. Why pick \Delta^0_1 defin­abil­ity?

If the ar­gu­ment worked in any par­tic­u­lar defin­abil­ity no­tion (e.g. ar­ith­metic defin­abil­ity) it would be a prob­lem. Thus, the solu­tion needs to ex­plain why the ar­gu­ment shouldn’t con­vince you that with re­spect to any con­crete no­tion of defin­able set the ar­gu­ment doesn’t go through.

• Tur­ing’s the­sis ap­plies only to this no­tion of defin­abil­ity, right?

• Yah, enu­mer­able means some­thing differ­ent than com­putably enu­mer­able.

• It seems “Com­putabil­ity and Logic” doesn’t in­clude Kleene’s re­cur­sion the­o­rem and Rice’s the­o­rem. What sources would you recom­mend for learn­ing those the­o­rems, their proofs, and their corol­laries? Also, which chap­ters of “Com­putabil­ity and Logic” are re­quired to un­der­stand them?