{\huge The Graph of Math}
The last part of our interview with Gödel two years ago
\vspace{.2in}
\includegraphics[width=2in]{GodelBlackboard.png}
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, which sounds more definite. But they are complementary: a statement is capable of being true somewhere precisely when its negation cannot be proved. The question is, where is that somewhere? And when?
Two years ago by our reckoning, Dick and I put that question to Gödel, at the close of our interview whose first and second parts we posted at this time the past two years.
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, and 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 sent its streams to mines in 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, while I monitored the transmission and the neutrino receiver.
Interview, Part III
{\sf 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?
{\sf Gödel:} Nicht nur bauen, sondern ständig zu bauen... {\sf Better in English: when you have building as a standing condition.}
GLL: Building what?
{\sf 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.
{\sf Gödel:} Ja{\sf ---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.
{\sf Gödel:} Gut dann{\sf ---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?
{\sf 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.
{\sf 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.
{\sf Gödel: Yes, the rule is categorical in that sense.}
GLL: But obviously the path obeys the rule. So I can build the graph.
{\sf Gödel: Indeed you can build it so 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.''
{\sf 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.
{\sf Gödel: But you can imagine it being placed.}
GLL: Of course, no problem. We just imagine it's like the numbers $latex {0, 1/2, 2/3, 3/4, 4/5,...}&fg=000000$ and then there's $latex {1}&fg=000000$.
\includegraphics[width=1.25in]{PathGraph.png}
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:
{\sf 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?
{\sf 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.
{\sf Gödel: Here is the rule:}
$latex {\infty}&fg=000000$: There is a node $latex {t}&fg=000000$ which has an arrow from the source node $latex {s}&fg=000000$, such that whenever $latex {x}&fg=000000$ has an arrow into $latex {t}&fg=000000$, there is another node $latex {y}&fg=000000$ that has arrows into it from $latex {x}&fg=000000$ and every node that has an arrow into $latex {x}&fg=000000$, and $latex {t}&fg=000000$ has an arrow from $latex {y}&fg=000000$.
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 $latex {x}&fg=000000$ on the path up from $latex {s}&fg=000000$, now we put $latex {y}&fg=000000$ up and to the side and connect it from $latex {x}&fg=000000$ and $latex {s}&fg=000000$, and we will have to connect both $latex {x}&fg=000000$ and $latex {y}&fg=000000$ to $latex {t}&fg=000000$, now move on the next node $latex {x'}&fg=000000$ up on the path from $latex {x}&fg=000000$ and---we'll also have to do this to $latex {y}&fg=000000$ 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 $latex {y}&fg=000000$ to be different from $latex {x'}&fg=000000$. It can be $latex {x'}&fg=000000$, but we connect it from $latex {s}&fg=000000$ too---so it has two arrows coming in. It's just like the path plus $latex {t}&fg=000000$ before, except now each node has an in-arrow from every node before it. It's just a fat path.
{\sf Gödel: Jawohl. Your fat path is called N.}
He drew a blackboard-bold $latex {\mathbb{N}}&fg=000000$, and I realized what he meant: $latex {0 = \emptyset}&fg=000000$, $latex {1 = \{\emptyset\}}&fg=000000$, $latex {2 = \{\emptyset, \{\emptyset\}\}}&fg=000000$, and in general $latex {x+1 = x \cup \{x\}}&fg=000000$. But Dick kept on about rules.
\includegraphics[width=1.5in]{FatPathGraph.png}
GLL: That was the hardest rule? That was easy...
{\sf 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?
{\sf 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 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.
{\sf 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 $latex {s}&fg=000000$ and $latex {t}&fg=000000$ were left. Then he moved his hand into the area I wondered about above $latex {t}&fg=000000$ and drew an open circle, not a dot. He labeled it $latex {V}&fg=000000$.
\includegraphics[width=3.5in]{GodelSetup.png}
{\sf Gödel: There is one extra concept. The graph has sinks as well as the one source $latex {s}&fg=000000$. 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 $latex {t}&fg=000000$ you imagine $latex {V}&fg=000000$ and the arrows are placed at the very end, last, well after all non-sinks. Note $latex {t}&fg=000000$ is not a sink---$latex {V}&fg=000000$ will have an arrow from $latex {t}&fg=000000$.}
GLL: Why $latex {V}&fg=000000$?
{\sf Gödel: Johnny and some others called it $latex {V}&fg=000000$ 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?
{\sf Gödel: No.}
He did not laugh at my joke; instead he got serious.
{\sf Gödel: The empty set $latex {s}&fg=000000$ is the first, and $latex {V}&fg=000000$ 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''?
{\sf 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?
{\sf 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.
{\sf Gödel: Ziemlich gut! So the rule really says:}
1. For every $latex {x}&fg=000000$ and distinct $latex {y}&fg=000000$, there must exist $latex {z}&fg=000000$ such that $latex {z}&fg=000000$ is connected to $latex {x}&fg=000000$ and not to $latex {y}&fg=000000$ 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?
{\sf Gödel: The standard answer is that the first-order concept of $latex {=}&fg=000000$ 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 $latex {x}&fg=000000$, and $latex {y}&fg=000000$ refers to nodes which are there at the time.}
GLL: And a third answer is that if you ever had two nodes with the name in-neighbors, you could just combine them.
{\sf 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 $latex {V}&fg=000000$ is unique. And $latex {s}&fg=000000$ 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?
{\sf 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?
{\sf 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 $latex {x}&fg=000000$, there must be some $latex {y}&fg=000000$ giving an in-arrow to $latex {x}&fg=000000$, such that no $latex {z}&fg=000000$ is connected to both $latex {x}&fg=000000$ and $latex {y}&fg=000000$.
GLL: I see---if $latex {x}&fg=000000$ just has an arrow to itself then with $latex {y = x}&fg=000000$ you would have a violation with $latex {z = y = x}&fg=000000$. I notice too it's important not to limit the statement to ``already-existing'' $latex {y}&fg=000000$.
{\sf 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 $latex {y}&fg=000000$ is a different node with an in-arrow to $latex {x}&fg=000000$. Then $latex {x}&fg=000000$ going to $latex {x}&fg=000000$ could be OK.
{\sf Gödel: Well the contradiction actually comes because we will have a rule that for all non-virgin $latex {x}&fg=000000$ you must place $latex {x'}&fg=000000$ having an in-arrow only from $latex {x}&fg=000000$. Then for $latex {x'}&fg=000000$ you must choose $latex {y = x}&fg=000000$ and you get the violation with $latex {z = y = x}&fg=000000$.}
GLL: Oh. What about cycles?
{\sf Gödel: Here is where the idea that all arrows into $latex {x}&fg=000000$ come at time of placement helps.}
GLL: I see---you can't place a cycle in order, not even an infinite cycle.
{\sf 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 two rules:}
\includegraphics[width=3.5in]{GodelMidway.png}
3. When you place a node $latex {x}&fg=000000$ you must place a node $latex {u}&fg=000000$ such that for all $latex {y}&fg=000000$ with in-arrows to $latex {x}&fg=000000$, and all $latex {z}&fg=000000$ with in-arrows to $latex {y}&fg=000000$, $latex {u}&fg=000000$ has an in-arrow from $latex {z}&fg=000000$.
4. When you place a non-virgin node $latex {x}&fg=000000$, for every non-virgin node $latex {y}&fg=000000$, you must place a non-virgin node $latex {z}&fg=000000$ with in-arrows from $latex {x}&fg=000000$ and $latex {y}&fg=000000$ and no other node. This allows $latex {x = y}&fg=000000$, 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 $latex {u}&fg=000000$, but it eventually ``bottoms out.'' The latter, however, forces an infinite amount of work, because not only do you have to loop over all $latex {y}&fg=000000$, but then you repeat the whole process with $latex {z}&fg=000000$. 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?
{\sf Gödel: Maybe I am bothered too, but in mathematics $latex {z}&fg=000000$ is simply the pair $latex {\{x,y\}}&fg=000000$. Or with $latex {y = x}&fg=000000$, $latex {z}&fg=000000$ is the singleton set $latex {x' = \{x\}}&fg=000000$ which I gave above. Anyway, here is how these rules forbid cycles in general. Suppose we had a 3-cycle, $latex {p \rightarrow q \rightarrow r \rightarrow p}&fg=000000$.
\includegraphics[width=3.5in]{GodelCycle.png}
{\sf 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.
{\sf 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?
{\sf 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 $latex {V}&fg=000000$. And the node for the set of nodes that are connected to themselves exists without paradox. It is $latex {s}&fg=000000$.}
GLL: Oh my. You don't need a whole type hierarchy to avoid the paradox, just the concept of ``virgin.''
{\sf Gödel: The larger purpose is to make the world safe for formulas as definitions. Thus there is no problem now with the formulas $latex {X \in X}&fg=000000$ and $latex {X \notin X}&fg=000000$. 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.
{\sf Gödel: Don't forget the rule $latex {\infty}&fg=000000$ which I mentioned first, but prefer to number last as 8. Now:}
5. For every non-virtual node $latex {x}&fg=000000$, there is a node $latex {p}&fg=000000$ such that for all nodes $latex {y}&fg=000000$, $latex {y}&fg=000000$ has an arrow to $latex {p}&fg=000000$ if and only if all nodes $latex {z}&fg=000000$ with an arrow to $latex {y}&fg=000000$ also have an arrow to $latex {x}&fg=000000$.
We recognized the last part as the subset relation, and Gödel wrote it that way as $latex {Uyx}&fg=000000$ using the German word Untermenge for subset. We realized he had not written or uttered anything else like ``set'' or $latex {\in}&fg=000000$ for ``member.'' Dick wanted to know whether this could cause a snag like with the cycle.
GLL: Ooh, I have to place $latex {p}&fg=000000$ when I place $latex {x}&fg=000000$, but $latex {p}&fg=000000$ has to come after all the $latex {y}&fg=000000$. So I have to place all the $latex {y}&fg=000000$ first. But that's OK: I only have to worry about all the possibilities for nodes $latex {z}&fg=000000$ that I am connecting to $latex {x}&fg=000000$. For every two or three of them, I will have to build $latex {y}&fg=000000$ 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 $latex {y}&fg=000000$'s are infinite I have to worry...ah, that will be an issue after your rule 8 or $latex {\infty}&fg=000000$ produces $latex {t}&fg=000000$. I see why you call that rule hard.
{\sf 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 which I can expand into eight more simple rules.}
6. For every first-order formula $latex {\phi(X)}&fg=000000$ with one free variable $latex {X}&fg=000000$, there is a node $latex {D_{\phi}}&fg=000000$ with arrows from exactly those nodes $latex {x}&fg=000000$ such that $latex {\phi(x)}&fg=000000$ is true.
{\sf Gödel: The one catch is that $latex {D_{\phi}}&fg=000000$ can be virtual, though the bound variables in $latex {\phi}&fg=000000$ range only over non-virgins. But $latex {D_{\phi}}&fg=000000$ 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 eight simpler ones---then you can define and use any first-order property of sets.}
GLL: Any first-order property?
{\sf 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.}
He drew diagrams above the cycle picture, saying these were the ordered pairs $latex {(x,x)}&fg=000000$ and $latex {(x,y)}&fg=000000$ for $latex {y \neq x}&fg=000000$:
\includegraphics[width=3.5in]{GodelThruPairs.png}
{\sf 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 $latex {V}&fg=000000$. This literally makes Russell's paradox into a virtue.}
7. A node is virtual exactly when there is a bijection between it and $latex {V}&fg=000000$.
Gödel registered our shock---this wasn't like a building rule. He added helpfully, drawing a surjection arrow to symbolize rule 7:
{\sf Gödel: Well it doesn't have to be a bijection---it is enough to have a function that is onto $latex {V}&fg=000000$.}
GLL: How can we tell?
{\sf 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 $latex {V}&fg=000000$ to $latex {V}&fg=000000$ 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.}
\includegraphics[width=3.5in]{GodelAllRules.png}
Dick and I exchanged glances. We were expecting the interview to end now, but Kurt was revved up and prancing around like a madman. But 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:
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?
{\sf 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 $latex {V}&fg=000000$ 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.}
GLL: Oh.
{\sf Gödel: Main thing to notice is that the $latex {x}&fg=000000$ 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 Johnny's rule.
GLL: Can you tell us the other schema?
{\sf 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 in my system where it isn't needed.}
GLL: The schema for Johnny's rule...
{\sf 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.
{\sf Gödel: The schema has one rule for every $latex {E}&fg=000000$ that you define that is a function. It is called ``Replacement,'' though you can also use it for placement.}
If $latex {E}&fg=000000$ is a function then for any non-virtual $latex {z}&fg=000000$, if $latex {Y}&fg=000000$ is such that for all $latex {x \rightarrow z}&fg=000000$, there is $latex {y \rightarrow Y}&fg=000000$ such that $latex {(x,y) \rightarrow E}&fg=000000$, then $latex {Y}&fg=000000$ can be colored black. Or you can place such a $latex {Y}&fg=000000$.
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 $latex {E}&fg=000000$ that was expressly defined. Dick wanted to clarify that point.
GLL: $latex {E}&fg=000000$ itself can be virtual?
{\sf Gödel: Yes. Of course, if you make $latex {E}&fg=000000$ the range of another function with non-virtual domain, then you can color $latex {E}&fg=000000$ black too. A midwife doesn't have to be a virgin. The basis is that you start with $latex {E}&fg=000000$ that are simple like $latex {D}&fg=000000$ and $latex {M}&fg=000000$ and combinations of them as above.}
I cut in.
GLL: Since we can define what it means to be a function, why don't we just quantify over $latex {E}&fg=000000$ in the rule, so we have just one rule not a schema? We can also define ``$latex {x}&fg=000000$ is non-virtual'' by saying $latex {(\exists y) x \rightarrow y}&fg=000000$.
{\sf Gödel: Letting $latex {E}&fg=000000$ 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.
One Choice
Kurt strolled over to his greenboard and solemnly drew a white circle between $latex {V}&fg=000000$ and $latex {t}&fg=000000$. He labeled it $latex {F}&fg=000000$. Then with a flourish he drew bang in the middle a sketch with an arcing dashed arrow he called the action of $latex {F}&fg=000000$.
{\sf Gödel: You need only an existential quantifier for this virtual object:}
There is a virtual node $latex {F}&fg=000000$ such that for all non-virtual nodes $latex {x}&fg=000000$ other than $latex {s}&fg=000000$, there is a unique $latex {y}&fg=000000$ such that $latex {(x,y)}&fg=000000$ has an arrow to $latex {F}&fg=000000$, and that $latex {y}&fg=000000$ has an arrow to $latex {x}&fg=000000$.
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:
{\sf Gödel: Of course $latex {F}&fg=000000$ is a function, and it is global, so this is called the Axiom of Global Choice. $latex {F}&fg=000000$ is last like $latex {V}&fg=000000$, but always there with you from your first placement after $latex {s}&fg=000000$. Of course you see why its presence does not interfere with building.}
\includegraphics[width=3.5in]{GodelComplete.png}
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 $latex {x}&fg=000000$ above the $latex {p,q,r}&fg=000000$ cycle, because you're not placing anything else. You either believe $latex {F}&fg=000000$ exists, or you don't.
{\sf Gödel: If you believe $latex {V}&fg=000000$ exists, then you should believe $latex {F}&fg=000000$ exists.}
I was still going to play Doubting Thomas.
GLL: Can't you get into trouble, when placing $latex {x}&fg=000000$, with what $latex {y}&fg=000000$ you choose? What if you commit to a bad $latex {y}&fg=000000$? Could that screw up the pairs in $latex {F}&fg=000000$, so that you have a problem with in-neighbors to a pair?
I realized that was silly before I finished---all the pairs in $latex {F}&fg=000000$ are already present, and rule 2 trivially holds for $latex {F}&fg=000000$ itself. Gödel read my facial retraction, and simply put his palms up.
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 $latex {F}&fg=000000$? What if I make my choices of $latex {y}&fg=000000$ a super-complex function, vastly uncomputable. Is $latex {F}&fg=000000$ going to catch that? What I really mean is, what if the only $latex {F}&fg=000000$ 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 $latex {F}&fg=000000$?
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.
{\sf Gödel: Wovon kommt diese Frage? Aber... But I tell you, after we sorted out this trouble with Max Zorn and Kazimierz Kuratowski, we realized $latex {F}&fg=000000$ can always be simple.}
Dick reacted and led the rest of the interview.
GLL: If you believe in $latex {F}&fg=000000$, then it is simple?
{\sf Gödel: Ja, equivalently. For one thing $latex {F}&fg=000000$ is equivalent to there being a well-ordering of $latex {V}&fg=000000$, from which you get $latex {F}&fg=000000$ by taking $latex {y}&fg=000000$ 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 $latex {x}&fg=000000$, there is always some in-neighbor $latex {y}&fg=000000$ such that previously when $latex {y}&fg=000000$ was placed, none of the other in-neighbors of $latex {x}&fg=000000$ were there yet. This is the $latex {y}&fg=000000$ you choose.
GLL: You cannot have two such $latex {y}&fg=000000$, because just between any $latex {y}&fg=000000$ and $latex {y'}&fg=000000$, one of them must have been placed earlier and been there for the other. Having no such $latex {y}&fg=000000$ is similarly unthinkable. But you said you wouldn't put the ordinal idea into the rules.
{\sf 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.
{\sf Gödel: Any trouble you have building with choice, you have already with the other rules on the board.}
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?
{\sf 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...
{\sf Gödel Ja, genau But outside the body, people complain the virtual nodes complicate Paul Cohen's forcing idea. I think it is better to think of the body as something you can maybe 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.
{\sf 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?
{\sf 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.
{\sf Gödel: Pretty much. But also you must start with Rule 8...}
GLL: So that is it. All of math in one graph.
{\sf Gödel: Math in a graph, yes, Johnny one step ahead again this time.}
GLL: Thank you very much, Herr Professor.
{\sf Gödel: Bitte schön.}
GLL: Can we see you again sometime?
{\sf 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.
Open Problems
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''?