The Graph of Math
The last part of our interview with Gödel two years ago
Kurt Gödel is said to have been a latecomer to appreciating the power of Model Theory. He was of course the greatest architect of Proof Theory, which stands in contrast to Model Theory. Model Theory concerns itself with what could be true, while Proof Theory deals with what can be proved. The latter sounds more definite, but they are supplementary: a statement is capable of being true somewhere precisely when its negation cannot be proved. The question is, where is that somewhere? And when?
As before, we took advantage of time-reversed communication that was made possible by Gödel’s own solution to Albert Einstein’s equations of general relativity. We needed zillions of rapidly spinning objects to implement a dual form of it. Time-traveling neutrinos fit the bill nicely, until the proof of this technology was found to be flawed. Still, it worked for a time, and the transmitter I managed while Dick led the talking duly sent its streams to mines in Soudan, Minnesota and Gran Sasso, Italy for recovery and transcription.
We must confess we are unable to recover the beginning of this part of the interview. Gödel said something we thought was crazy, just false, a self-contradiction really, and our reaction upset him. What he said was he thought the axioms of set theory were “obviously true” and he was trying to prove them using “large cardinals,” which we took to be part of set theory. We reacted with what we thought was a careful, innocent, reader-friendly question:
Doesn’t using set theory to prove set theory true imply proving it’s consistent, which you proved set theory cannot do?
Well Gödel didn’t like this question. He flew into German so loudly and rapidly that I missed a lot of words. He either said our trifling question was not serious then something about Zermelo’s axioms, or he said it was a niggling question like Ernst Zermelo would ask—since “ernst” means “serious” in German. Then he said that set theory was “not closed in on itself” so “my theorem doesn’t stop it.” Then I made out only a few words: sechszehn (sixteen) … jungfern (virgin) … Körper (bodies) … vermeiden Russell (avoid Russell), amid several references to “classes” and “Johnny.” Bertrand Russell’s escapades were well known, but that couldn’t be what Gödel was talking about, and my total perplexity was read well enough by Dick.
What saved us again was Gödel’s tendency to be contrite on regaining his composure. He said he thought he had convinced everyone that set theory was true (!—he did not say “consistent”) when he proved that the Axiom of Choice could not cause its inconsistency, but now he himself was beginning to doubt the truth (!) of the Continuum Hypothesis even though he had proved it was “equally consistent.” He admitted how people could be concerned that set theory was inconsistent “since it happened before,” and said he would apologize by demonstrating his understanding of their point of view.
Then he launched into something we didn’t know from his writings, and this is what we want to share with you, our readers. As before, Dick asked the questions unless I chimed in.
Interview, Part III
Gödel: Of course mathematics is about truth, not possibility. But possibility in mathematics—which is when falseness is not necessary—can also be about truth, the truth of being able to build…
GLL: To build?
Gödel: Nicht nur bauen, sondern ständig zu bauen… Better in English: when you have building as a standing condition.
GLL: Building what?
Gödel: I should say “building a model,” but in the 1950’s I thought about this again after hearing some of Johnny’s last ideas.
GLL: Johnny of course is John von Neumann.
Gödel: Ja—and he said his work on cellular automata made him study networks, I think now you say “graphs.”
GLL: Yes of course, directed or undirected, finite or infinite graphs. A big area of study.
Gödel: Gut dann—well these questions about the foundations of mathematics are about whether you can build infinite directed graphs according to certain rules.
GLL: What kind of rules?
Gödel: Simple for the most part. Let me try one example. Every node has one arrow in and one arrow out, except one source node has only one arrow out.
GLL: You are tricky—since you said there is one source node I can’t just use the empty graph.
Gödel: Right, but can you use a finite graph?
Dick realized that the source node rule prevents a finite cycle, while the other rule prevents any arrow from going to any old node. So the graph must be infinite.
GLL: We have to build the infinite path.
Gödel: Yes, the rule admits no finite model, as they say today.
GLL: But obviously the path obeys the rule. So I can build the graph.
Gödel: Indeed you can build it observing the condition that whenever you place a node, you determine all arrows that go in to it.
GLL: Yes, no problem. But I place a node infinitely many times—I guess that’s what you meant by “standing condition.”
Gödel: Genau—exactly—now one more point will convey the whole task. Can you place a node that has arrows coming in from every node in your path?
GLL: Yes of course—it just sits at the top above the path…oh I see, I see…, there’s no finite time when you place it, if you need to determine all incoming arrows when you do.
Gödel: But you can imagine it being placed.
GLL: Of course, no problem. We just imagine it’s like the numbers and then there’s .
I squirmed in the background and thought of asking whether we’d have to place nodes at uncountably many infinite delays, but feared another fuss. Gödel seemed to sense my thought anyway, because he said:
Gödel: The rules that matter will be simple, and maybe we care about only one more infinite building step.
GLL: What are some other rules?
Gödel: I will give you the hardest rule—in a sense the only hard one—right away.
Hard is Easy, But What’s Impossible?
Gödel pulled up a green chalkboard on wheels. I’ve often wondered whether they use those or PowerPoint where he is, now I know. He drew one dot at bottom center and one at upper center but not near the top, and I wondered why he left room there.
Gödel: Here is the rule:
: There is a node which has an arrow from the source node , such that whenever has an arrow into , there is another node that has arrows into it from and every node that has an arrow into , and has an arrow from .
Gödel wheeled the blackboard toward Dick, maybe not realizing that across the spacetime expanse Dick couldn’t come forward to use it. But Dick started telling Kurt—OK we never called him Kurt—what he wanted to draw.
GLL: Take your on the path up from , now we put up and to the side and connect it from and , and we will have to connect both and to , now move on the next node up on the path from and—we’ll also have to do this to too…so the graph may get pretty bushy…
Gödel leaned in with a grin and waved his hand out but toward himself, like hinting for a better answer. Dick picked up quick:
GLL: Ah—we don’t need to be different from . It can be , but we connect it from too—so it has two arrows coming in. It’s just like the path plus before, except now each node has an in-arrow from every node before it. It’s just a fat path.
Gödel: Jawohl. Your fat path is called N.
He drew a blackboard-bold , and I realized what he meant: , , , and in general . He wrote the quantifiers he’d stated and then a wavy line to represent the fat path. But Dick kept on about rules.
GLL: That was the hardest rule? That was easy…
Gödel: Well, we’ll see how it interacts with the other rules. I will mention it again later.
GLL: Are any rules impossible? What would be an impossible rule?
Gödel: Each rule is possible—all the rules together is the issue. But here is an impossible rule: You must not allow infinitely many nodes having no arrows between any two, and you must not allow infinitely many nodes with an arrow between every two.
GLL: The fat path has an arrow between every pair, so that’s out, while the thin path…ah, does not have any arrows between even nodes. Or between odd-numbered nodes. So that’s out. But why can’t I build alternating…?
Again we saw the professorial grin and wide—but not smug—eyes behind Kurt’s thick glasses.
GLL: Oh of course. The infinite Ramsey theorem.
I had thought of that too. Kurt waggled his hands approvingly. I was glad he didn’t think we were stupid anymore. Indeed I thought to say the Ramsey rule was maybe unfair because it had second-order quantifiers over infinite sets, but Gödel had the floor.
Gödel: Are you ready now to try the rules—the real rules? There are eight of them, but one is a “schema” that I discovered can be expanded into just nine more rules, so that makes sixteen with no schemas. But if you are happy with the intuition with a schema about formulas, then another rule—Johnny’s rule—can be treated very nicely if you also allow choice.
We were game for anything.
Start of the Rules
Kurt erased the board so only and and the partially-written rule were left. Then he moved his hand into the area I wondered about above and drew an open circle, not a dot. He labeled it .
Gödel: There is one extra concept. The graph has sinks as well as the one source . Many sinks. But one sink is, how do you say in English—the Kitchen Sink, because it has an arrow from every non-sink. Of course like with you imagine and the arrows are placed at the very end, last, well after all non-sinks. Note is not a sink— will have an arrow from .
GLL: Why ?
Gödel: Johnny and some others called it for veritas, truth, while I thought “virtual” in English, but I now think maybe better is “virgin,” because it does not connect to anything. There are other sinks too—other virgins—and they are very useful. Virgins can be born—have arrows coming in but only from non-virgins of course—and importantly they can be “midwives” to non-virgins.
I couldn’t resist cutting in.
GLL: There are no Virgin Births?
He did not laugh at my joke; instead he got serious.
Gödel: The empty set is the first, and is the last, and they are connected. Paul Bernays spoke of them as two separate kinds of object—at least this was better than Johnny making everything a function—but it suits my spirit better if they are one kind but have two different states of being.
Dick took this in but moved forward.
GLL: OK, the white dots are “virgins”?
Gödel: You can call them “classes,” except for me “class” includes “set”—so you can say “proper classes” to distinguish the white ones. If you say “class” for white then I could say Körper—bodies—for both, but anyway the rules about incoming arrows will apply to both the same way, so don’t worry. It’s all one graph—that’s why I consider it the same kind.
GLL: Okay, how do we build the graph?
Gödel: The first rule is really only a “gentleman’s agreement,” since if you ever violated it with a placement, you could just skip it. The rule is:
1. No two nodes may have arrows from the same set of nodes.
GLL: Since you say “set,” and the set could be infinite, aren’t you assuming what you’re formalizing?
I caught my breath momentarily, but Kurt was actually very pleased.
Gödel: Ziemlich gut! So the rule really says:
1. For every and distinct , there must exist such that is connected to and not to or vice-versa.
This made me brave enough to ask a really niggling question:
GLL: But Herr Professor Doktor, when you say “distinct,” is this not already referencing the condition of set-inequality which you are defining here?
Gödel: The standard answer is that the first-order concept of as identity is more primitive than equality of sets, which this rule ensures never comes up. My other answer is that the rule applies in the order of placement for , and refers to nodes which are there at the time.
GLL: And a third answer is that if you ever had two nodes with the same in-neighbors, you could just combine them.
Gödel: Yes, and this applies to all nodes. No white node can ever have the same in-neighbors as a black node, or another white node. So is unique. And is the unique source.
I cut in again.
GLL: If you had other sources that were not placed but were there from the beginning, would that be OK?
Gödel: Yes that would be OK. Such nodes are called Ur-Elemente, original elements. I think of them like Adam and Eve, and Lilith and others… Having them be sources will not cause a problem and is good for discourse, but there is no need—this makes no difference in what you are able to prove.
I also wanted to ask about whether using quantifiers and variables was prematurely assuming things about set theory as a foundation, but I gathered Gödel had a long answer which could go into Principia Mathematica and/or the lambda calculus of Alonzo Church. I guessed that so long as all the rules stuck to first-order logic this would be fine. Dick had a more-pressing question anyway.
Four Rules to Avoid Russell
GLL: Can we make an arrow go back to the same node? Can we have a cycle?
Gödel: First I’ll state the second rule. I’ll use the “ordinal placement” language to state it:
2. When you place a node , there must be some that gives an in-arrow to , such that no is connected to both and .
GLL: I see—if just has an arrow to itself then with you would have a violation with . I notice too it’s important not to limit the statement to “already-existing” .
Gödel: Indeed we must write the rules without referencing the time of placement or ideas of “already” or “before” at all.
GLL: Wait—what if is a different node with an in-arrow to . Then going to could be OK.
Gödel: Well the contradiction actually comes because we will have a rule that for all non-virgin you must place having an in-arrow only from . Then for you must choose and you get the violation with .
GLL: Oh. What about cycles?
Gödel: Here is where the idea that all arrows into come at time of placement helps.
GLL: I see—you can’t place a cycle in order, not even an infinite cycle.
Gödel: The actual way cycles are banished with two more rules is important to see, because it is a “delayed effect” of the kind that makes me wonder whether we can formalize a better intuition. Here are the next two rules:
3. When you place a node you must place a node such that for all with in-arrows to , and all with in-arrows to , has an in-arrow from .
4. When you place a non-virgin node , for every non-virgin node , you must place a non-virgin node with in-arrows from and and no other node. This allows , but of course they cannot be virgins since they have out-arrows.
GLL: The former rule is fine—you must repeat it when you place , but it eventually “bottoms out.” The latter, however, forces an infinite amount of work, because not only do you have to loop over all , but then you repeat the whole process with . Plus I’m a little bothered by the “non-virgin” condition here—when do we tell whether a node is going to be or stay a virgin?
Gödel: Maybe I am bothered too, but in mathematics is simply the pair . Or with , is the singleton set which I gave above. Anyway, here is how these rules forbid cycles in general. Suppose we had a 3-cycle, :
- By rule 4 we have a node with arrows from and .
- By rule 4 again we have a node with arrows from and .
- By rule 3 we have a node with three in-arrows: from , , and .
- But now that placement of violates rule 2. Because: whatever we choose, its predecessor in the cycle is connected to both and .
Gödel: For longer cycles you have to do more pairing and union steps, but even for an infinite cycle, as you build up the infinite union you would fly inexorably to a violation of rule 2 at some infinite time.
GLL: That’s rather scary.
Gödel: But it never comes up, because the rules are first-order, and you never have to fear that you will accidentally build the cycle. The placement intuition tells you this already.
GLL: OK. But what about Russell? Isn’t the idea of a “node connected from all nodes that are not connected from themselves” still a contradiction?
Gödel. No. All virgins are not connected to anything, so not to themselves. If you were going to get a paradox whose statement doesn’t already violate the condition of being virgin, it would be about a node connected from all non-virgin nodes that are not connected to themselves. Above we made sure all non-virgins are not connected to themselves. So that node exists, without paradox. It is . And the node for the set of nodes that are connected to themselves exists without paradox. It is .
GLL: Oh my. You don’t need a whole type hierarchy to avoid the paradox, just the concept of “virgin.”
Gödel: The larger purpose is to make the world safe for formulas as definitions. Thus there is no problem now with the formulas and . You just allow that your answer might turn out to be a virgin—well, virtual. If you are happy with formulas, then the last three rules will not bother you. One of them already is no problem.
The Last Three Rules
Gödel had just enough room at the left to write one more rule, and started writing “5.” just as Dick broke in.
GLL: You said 8 rules, but three more makes only 7.
Gödel: Don’t forget the rule which I mentioned first, but prefer to number last as 8. Now:
5. For every non-virtual node , there is a node such that for all nodes has an arrow to if and only if all nodes with an arrow to also have an arrow to .
We recognized the last part as the subset relation, and Gödel wrote it that way as using the German word Untermenge for subset. We realized he had not otherwise written or spoken anything else like “set” or for “member” in these rules. Dick wanted to know whether this could cause a snag like with the cycle.
GLL: Ooh, I have to place when I place , but has to come after all the . So I have to place all the first. But that’s OK: I only have to worry about all the possibilities for nodes that I am connecting to . For every two or three of them, I will have to build as the pair or triple of them anyway, as you showed above when discussing the 3-cycle. And so on. So it bottoms out OK. OK, I think I can build with this rule…maybe when the ‘s are infinite I have to worry…ah, that will be an issue after your rule 8 or produces . I see why you call that rule hard.
Gödel: But I hope that since we are putting it eighth and last, you won’t find the other two rules hard. I am going to be informal with the next one, because it is the schema that I can expand into nine more simple rules.
6. For every first-order formula with one free variable , there is a node with arrows from exactly those nodes such that is true.
Gödel: The one catch is that can be virtual, though the bound variables in range only over non-virgins. But need not always be virtual—the seventh rule will tell you when it is. If you accept this rule—like I said it follows from nine simpler ones—then you can define and use any first-order property of sets.
GLL: Any first-order property?
Gödel: Yes, but it is merely what the syntax gives you. We already have pairs, and I should show you now how to make ordered pairs.
Before writing rule 6 on the board, he drew diagrams above the cycle picture, saying these were the ordered pairs and for :
Gödel: We can now have a relation between virtual nodes, because its members are pairs comprised of an element from each and those elements are not virtual. Then we can define when the relation is a function, when it is onto, one-to-one, and a bijection. Well Johnny started with functions, but we have arrived there, and now we can state his rule—note that rule 6 defined . This literally makes Russell’s paradox into a virtue.
7. A node is virtual exactly when there is a bijection between it and .
Gödel registered our shock—this wasn’t like a building rule. He added helpfully, drawing a surjection arrow to symbolize rule 7:
Gödel: Well it doesn’t have to be a bijection—it is enough to have a function that is onto .
GLL: How can we tell?
Gödel: When you are finishing saying how you are building the graph, you just have to tell how all your sinks have bijections. From to it is immediate, of course. But I showed this is equivalent to the schema of replacement, allowng virtual nodes as functions between sets like midwives, plus the Axiom of Choice extended to all nodes. If you accept the former, then since I showed the latter cannot be the obstacle that blocks you, you can build.
Dick and I exchanged glances. We were expecting the interview to end now, but Kurt was revved up and prancing around like a madman. We realized he would oblige any further request, so Dick ventured:
GLL: Can you tell us the nine simple rules and the other schema?
He was already starting to do so.
The Two Schemas
Gödel did not write anything more on the board he had filled, but rather dictated the following rules:
- represents True and represents False;
- We build for “diagonal,” which has an arrow from every , and represents .
- We build for “member.” This has an arrow from every where , and represents .
- We build with arrows from all nodes not of the form . Similarly we can apply to complement any node. This represents negation.
- For any nodes we ensure there is a node such that . We write , and here too need not be virtual—for instance . This represents Boolean AND.
- For any node we build a node with arrows from for all and all such that , allowing . This represents introducing a variable and forms the Cartesian product .
- For any with arrows only from ordered pairs not in , we build the node with arrows from the “” part of each pair. This forms the range and represents existentially quantifying the “” parts.
For any with arrows only from ordered pairs , we can build with arrows from their reversed pairs , with being OK. And for any composed of triples , we can build with triples and with triples . Finally for with quartuples , we build with quartuples instead. These rules represent enough ways to permute the list of variables in a formula.
Dick frantically took them down on his notepad. He slowed Kurt down only on the last one, which Dick wrote as four separate rules. Upon ending the last one, Gödel went stock-still, but did not look cross, so Dick queried him.
GLL: These are eleven rules?
Gödel: The last is almost one rule, but I call it three for pairs, triples, quartuples. And the first rule is just interpretation, not building, so it isn’t a rule—we have the empty set with infinity and with complements. Hence I count nine. Whatever, this is finite and allows you to build the denotation of any formula in the original schema 6, so it is not a schema.
Gödel: Main thing to notice is that the parts of pairs cannot be virtual. Hence the formulas quantify only over non-virtual nodes, though the denotation itself for the free variable can be virtual. This limitation is completely natural. If you ignore it and allow formulas to quantify over virtual nodes, you cannot make a finite set of rules anymore. You get a stronger set theory, but the only ways I see how to build it are inaccessible…
We were starting to feel stupid and were afraid to ask what “inaccessible” meant. Instead we wanted to know more about Johnny’s rule.
GLL: Can you tell us the other schema?
Gödel: The only schema? If you forget virtuals and choice it is the only schema, and has to be. But it is still good to have it in my system, even though it isn’t needed.
GLL: The schema for Johnny’s rule…
Gödel: Yes. Johnny’s rule tells you when you can say a node is virtual. This rule—it is Abraham Fraenkel’s rule—tells you when you can say it is not virtual. If you have choice for all nodes then the effect is the same.
GLL: Please continue.
Gödel: The schema has one rule for every that you define that is a function. It is called “Replacement,” though you can also use it for placement.
When you have defined an that is a function, you obtain the rule that for any non-virtual , if is such that for all there is such that , then is colored black. Or you can place such a .
This made us happier than von Neumann’s rule, because it was talking about sets rather than “virtual” whatevers, and each individual rule concerned a function that was expressly defined. Dick wanted to clarify that point.
GLL: itself can be virtual?
Gödel: Yes. Of course, if you make the image of another function with non-virtual domain, then you can color black too. A midwife doesn’t have to be a virgin. The basis is that you start with that are simple like and and combinations of them as above.
GLL: Does have to be the whole domain of ?
Gödel: No, but if is definable, then we can define restricted to anyway. Also needs only to be a function on .
I cut in.
GLL: Since we can define what it means to be a function, why don’t we just quantify over in the rule, so we have just one rule not a schema? We can also define “ is non-virtual” by saying
Gödel: Letting be arbitrary would lose the sense of building, and also it would be a universal quantifier over virtual objects inside a rule. This was also my first feeling about Johnny’s rule, until I saw it can be proved from replacement if you have choice.
Dick and I stiffened up. We were about to hear the Axiom of Choice from Gödel himself.
Kurt strolled over to his greenboard and solemnly drew a white circle between and . He labeled it . Then with a flourish he drew bang in the middle a sketch with an arcing dashed arrow he called the action of .
Gödel: You need only an existential quantifier for this virtual object:
There is a virtual node such that for all non-virtual nodes other than , there is a unique such that has an arrow to , and that has an arrow to .
Dick and I totally missed what he said. We thought the axiom of choice always began with the words “for every,” as in “for every collection of nonempty sets…” We were expecting to hear the word “function” again. Dick nicely spared me the embarrassment by taking it on himself.
GLL: I’m totally sorry, I missed what you said.
Gödel repeated it calmly, and then said:
Gödel: Of course is a function, and it is global, so this is called the Axiom of Global Choice. is last like , but always there with you from your first placement after . Of course you see why its presence does not interfere with building.
It took only a few seconds to hit us that Kurt was saying his famous proof of the relative consistency of the axiom of choice—in his stronger version—was something we should see immediately.
GLL: Right—I see—it’s not going to get you into trouble like when you placed above the cycle, because you’re not placing anything else. You either believe exists, or you don’t.
Gödel: If you believe exists, then you should believe exists.
I was still going to play Doubting Thomas.
GLL: Can’t you get into trouble, when placing , with what you choose? What if you commit to a bad ? Could that screw up the pairs in , so that you have a problem with in-neighbors to a pair?
I realized that was silly before I finished—all the pairs in are already present, and rule 2 trivially holds for itself. Gödel read my facial retraction, and simply put his palms out.
But then Dick swiveled around to me and whispered something about finite choice and complexity that he had posted on. I caught Dick’s drift and spoke up again in a firmer tone.
GLL: Herr Professor Doktor, what is the complexity of ? What if I make my choices of a super-complex function, vastly uncomputable. Is going to catch that? What I really mean is, what if the only is super-complex, “inaccessible” like you said? Then we don’t see how to build the choices—and isn’t that what you need to say you can build ?
Gödel flipped the chalk in his hand, and distorted his face as if it were a rubber mask he was about to tear off, but gave a snorting chuckle and sounded recomposed.
Gödel: Woher kommt diese Frage? Aber… But I tell you, after we sorted out this trouble with Max Zorn and Kazimierz Kuratowski, we realized can always be simple.
Dick reacted and led the rest of the interview.
GLL: If you believe in , then it is simple?
Gödel: Ja, equivalently. For one thing is equivalent to there being a well-ordering of , from which you get by taking to be the least element among the possibilities. And the well-ordering itself can also be a simple consequence of how you build:
When you placed , there is always some in-neighbor such that previously when was placed, none of the other in-neighbors of were there yet. This is the you choose.
GLL: You cannot have two such , because just between any and , one of them must have been placed earlier and been there for the other. Having no such is similarly unthinkable. But you said you wouldn’t put the ordinal idea into the rules.
Gödel: I didn’t. Did I say that? The rule is what I said before. This is just the intuition. These last two rules, replacement and choice, are equivalent to rule 7 anyway. Rule 7 gives you a finite axiomatization, but I prefer the other two rules for my thinking. They convince me that Johnny’s rule is good.
GLL: I must admit, the intuition is clear. And we know from our recent discussion of first-order models that the graph itself can always stay countable, even while it is modeling Cantor’s Theorem.
Gödel: Any trouble you have building with choice, you have already with the other rules on the board. Rule 6 already restores the Eden we had with “naive” set theory, provided we acknowledge the original sin from Russell’s paradox. But to make it a kingdom, we should have the action of choice.
Math as a Graph
Dick and I stared at the eight rules. We wondered how they could possibly capture virtually all of mathematics as we know it, all of computer science theory. But they do. Every theorem we know can be systematically encoded in this language and proved with standard first-order logic plus these rules. Even second-order and higher logic can be simulated by quantifying over sets.
Only the “sets” we were looking at were just dots with arrows in graphs. The graphs don’t even have any cycles. Directed acyclic graphs—DAGs—are about the simplest things we work on in algorithms and theory. How can they execute everything?
GLL: So if we can build the graph, then set theory—your set theory—is consistent?
Gödel: ZFC set theory too. They are equally consistent. Any statement that does not mention a virtual node—or involve my notion of coloring a node white or black—can be proved in my system with Johnny and Bernays, if and only if it can be proved in ZFC. Ours is a “conservative extension.”
GLL: So your system has exactly the same power for expressing mathematics, the main body of mathematics…
Gödel Ja, genau. But outside the body, people complain that the virtual nodes complicate Paul Cohen’s forcing idea. I think it is better to think of the body as something you can perhaps extend by a 17th rule, one that can be like the Unified Field Theory which Albert was looking for.
GLL: But the body we have cannot tell whether the graph exists.
Gödel: Right—the 16 rules cannot prove their own consistency.
GLL: Yet all you’re talking about is the existence of a countably infinite directed acyclic graph. One graph. One with constructive rules for building. So we can’t use our whole math curriculum to determine that this graph exists?
Gödel: No. You must only believe it, or look for higher rules—like I am also doing.
GLL: It seems like the only obstacle is what you sketched with the cycle, from Rule 2.
Gödel: Pretty much. But also you must start with Rule 8…
GLL: So that is it. All of math in one graph.
Gödel: Math in a graph, yes, Johnny was one step ahead again this time.
GLL: Thank you very much, Herr Professor.
Gödel: Bitte schön.
GLL: Can we see you again sometime?
Gödel: Should be possible. But you will need new science.
And with that the professor and the chalkboard became enmeshed in a noise of dots and lines on our screen, until it all went white.
Do you see how to build the graph of math? Are you convinced it is entirely there?
As an exercise, can you complete the first-order infinity rule, which Gödel left “non-finito”?
[fixed two counts of the “simpler rules” from “eight” to “nine”; added link to Morse-Kelley’s “stronger set theory”; woher-to-woraus-back to-woher; spot word tweaks]