A Discovery about Basic Logic
Logic is a foundation for many things. But what are the foundations of logic itself?
In symbolic logic, one introduces symbols like p and q
to stand for statements (or “propositions”) like “this is an
interesting essay”. Then one has certain “rules of logic”, like that,
for any p and any q, NOT (p AND q) is the same as (NOT p) OR (NOT q).
But where do these “rules of logic” come from? Well,
logic is a formal system. And, like Euclid’s geometry, it can be built
on axioms. But what are the axioms? We might start with things like p AND q = q AND p, or NOT NOT p = p. But how many axioms does one need? And how simple can they be?
It was a nagging question for a long time. But at
8:31pm on Saturday, January 29, 2000, out on my computer screen popped a
single axiom. I had already shown there couldn’t be anything simpler,
but I soon established that this one little axiom was enough to generate
all of logic:
✕
((p·q)·r)·(p·((p·r)·p))==r
|
But how did I know it was correct? Well, because I had a computer prove it. And here’s the proof, as I printed it in 4-point type in A New Kind of Science (and it’s now available in the Wolfram Data Repository):
With the latest version of the Wolfram Language, anyone can now generate this proof in under a minute. And given this proof, it’s straightforward to verify each step. But why is the result true? What’s the explanation?
That’s the same kind of question that’s increasingly
being asked about all sorts of computational systems, and all sorts of
applications of machine learning and AI. Yes, we can see what happens.
But can we understand it?
I think this is ultimately a deep question—that’s
actually critical to the future of science and technology, and in fact
to the future of our whole intellectual development.
But before we talk more about this, let’s talk about logic, and about the axiom I found for it.
The History
Logic as a formal discipline basically originated with Aristotle
in the 4th century BC. As part of his lifelong effort to catalog
things (animals, causes, etc.), Aristotle cataloged valid forms of
arguments, and created symbolic templates for them which basically
provided the main content of logic for two thousand years.
By the 1400s, however, algebra had been invented, and
with it came cleaner symbolic representations of things. But it was not
until 1847 that George Boole finally formulated logic in the same kind of way as algebra, with logical operations like AND and OR being thought of as operating according to algebra-like rules.
Within a few years, people were explicitly writing down axiom systems for logic. A typical example was:
✕
and[p,q]==and[q,p],or[p,q]==or[q,p],and[p,or[q,not[q]]]==p,or[p,and[q,not[q]]]==p,and[p,or[q,r]]==or[and[p,q],and[p,r]],or[p,and[q,r]]==and[or[p,q],or[p,r]]}
|
But does logic really need AND and OR and NOT? After the first decade of the 1900s several people had discovered that actually the single operation that we now call NAND is enough, with for example p OR q being computed as (p NAND p) NAND (q NAND q). (The “functional completeness” of NAND
could have remained forever a curiosity but for the development of
semiconductor technology—which implements all the billions of logic
operations in a modern microprocessor with combinations of transistors that perform none other than NAND or the related function NOR.)
But, OK, so what do the axioms of logic (or “Boolean algebra”) look like in terms of NAND? Here’s the first known version of them, from Henry Sheffer in 1913 (here dot · stands for NAND):
✕
{(p\[CenterDot]p)\[CenterDot](p\[CenterDot]p)==p,p\[CenterDot](q\[CenterDot](q\[CenterDot]q))==p\[CenterDot]p,(p\[CenterDot](q\[CenterDot]r))\[CenterDot](p\[CenterDot](q\[CenterDot]r))==((q\[CenterDot]q)\[CenterDot]p)\[CenterDot]((r\[CenterDot]r)\[CenterDot]p)}
|
Back in 1910 Whitehead and Russell’s Principia Mathematica
had popularized the idea that perhaps all of mathematics could be
derived from logic. And particularly with this in mind, there was
significant interest in seeing just how simple the axioms for logic
could be. Some of the most notable work on this was done in Lviv and
Warsaw (then both part of Poland), particularly by Jan Łukasiewicz (who, as a side effect of his work, invented in 1920 parenthesis-free Łukasiewicz or “Polish” notation). In 1944, at the age of 66, Łukasiewicz fled from the approaching Soviets—and in 1947 ended up in Ireland.
Meanwhile, the Irish-born Carew Meredith,
who had been educated at Winchester and Cambridge, and had become a
mathematics coach in Cambridge, had been forced by his pacifism to go
back to Ireland in 1939. And in 1947, Meredith went to lectures by
Łukasiewicz in Dublin, which inspired him to begin a search for simple
axioms, which would occupy most of the rest of his life.
Already by 1949, Meredith found the two-axiom system:
✕
{(p\[CenterDot](q\[CenterDot]r))\[CenterDot](p\[CenterDot](q\[CenterDot]r))==((r\[CenterDot]p)\[CenterDot]p)\[CenterDot]((q\[CenterDot]p)\[CenterDot]p),(p\[CenterDot]p)\[CenterDot](q\[CenterDot]p)==p}
|
After nearly 20 years of work, he had succeeded by 1967 in simplifying this to:
✕
{p\[CenterDot](q\[CenterDot](p\[CenterDot]r))==((r\[CenterDot]q)\[CenterDot]q)\[CenterDot]p,(p\[CenterDot]p)\[CenterDot](q\[CenterDot]p)==p}
|
But could it get any simpler? Meredith had been picking away for years trying to see how a NAND could be removed here or there. But after 1967 he apparently didn’t get any further (he died in 1976), though in 1969 he did find the three-axiom system:
✕
{p\[CenterDot](q\[CenterDot](p\[CenterDot]r))==p\[CenterDot](q\[CenterDot](q\[CenterDot]r)),(p\[CenterDot]p)\[CenterDot](q\[CenterDot]p)==p,p\[CenterDot]q==q\[CenterDot]p}
|
I actually didn’t know about Meredith’s work when I
started exploring axiom systems for logic. I’d gotten into the subject
as part of trying to understand what kinds of behavior simple rules
could produce. Back in the early 1980s I’d made the surprising discovery that even cellular automata with some of the simplest possible rules—like my favorite rule 30—could generate behavior of great complexity.
And having spent the 1990s basically trying to figure
out just how general this phenomenon was, I eventually wanted to see how
it might apply to mathematics. It’s an immediate observation that in
mathematics one’s basically starting from axioms (say for arithmetic, or geometry, or logic), and then trying to prove a whole collection of sophisticated theorems from them.
But just how simple can the axioms be? Well, that was
what I wanted to discover in 1999. And as my first example, I decided
to look at logic (or, equivalently, Boolean algebra). Contrary to what I
would ever have expected beforehand, my experience with cellular automata, Turing machines, and many other kinds of systems—including even partial differential equations—was
that one could just start enumerating the simplest possible cases, and
after not too long one would start seeing interesting things.
But could one “discover logic” this way? Well, there
was only one way to tell. And in late 1999 I set things up to start
exploring what amounts to the space of all possible axiom
systems—starting with the simplest ones.
In a sense any axiom system provides a set of constraints, say on p · q. It doesn’t say what p · q “is”; it just gives properties that p · q must satisfy (like, for example, it could say that p · q = q · p). Then the question is whether from these properties one can derive all the theorems of logic that hold when p · q is Nand[p, q]: no more and no less.
There’s a direct way to test some of this. Just take the axiom system, and see what explicit forms of p · q satisfy the axioms if p and q can, say, be True or False. If the axiom system were just p · q = q · p then, yes, p · q could be Nand[p, q]—but it doesn’t have to be. It could also be And[p, q] or Equal[p, q]—or lots of other things which won’t satisfy the same theorems as the NAND function in logic. But by the time one gets to the axiom system {((p · p) · q) · (q · p) = q} one’s reached the point where Nand[p, q] (and the basically equivalent Nor[p, q]) are the only “models” of p · q that work—at least assuming p and q have only two possible values.
So is this then an axiom system for logic? Well, no. Because it implies, for example, that there’s a possible form for p · q with 3 values for p and q,
whereas there’s no such thing for logic. But, OK, the fact that this
axiom system with just one axiom even gets close suggests it might be
worth looking for a single axiom that reproduces logic. And that’s what
I did back in January 2000 (it’s gotten a bit easier these days, thanks
notably to the handy, fairly new Wolfram Language function Groupings).
It was easy to see that no axioms with 3 or fewer “NANDs” (or, really, 3 or fewer “dot operators”) could work. And by 5am on Saturday, January 29 (yes, I was a night owl then), I’d found that none with 4 NANDs could work either. By the time I stopped working on it a little after 6am, I’d gotten 14 possible candidates with 5 NANDs. But when I started work again on Saturday evening and did more tests, every one of these candidates failed.
So, needless to say, the next step was to try cases with 6 NANDs.
There were 288,684 of these in all. But my code was efficient, and it
didn’t take long before out popped on my screen (yes, from Mathematica Version 4):
At first I didn’t know what I had. All I knew was that these were the 25 inequivalent 6-NAND axioms that got further than any of the 5-NAND
ones. But were any of them really an axiom system for logic? I had a
(rather computation-intensive) empirical method that could rule axioms
out. But the only way to know for sure whether any axiom was actually
correct was to prove that it could successfully reproduce, say, the
Sheffer axioms for logic.
It took a little software wrangling, but before many
days had gone by, I’d discovered that most of the 25 couldn’t work. And
in the end, just two survived:
✕
{((p\[CenterDot]q)\[CenterDot]r)\[CenterDot](p\[CenterDot]((p\[CenterDot]r)\[CenterDot]p))==r}
|
✕
{(p\[CenterDot]((r\[CenterDot]p)\[CenterDot]p))\[CenterDot](r\[CenterDot](q\[CenterDot]p))==r}
|
And to my great excitement, I was successfully able to
have my computer prove that both are axioms for logic. The procedure
I’d used ensured that there could be no simpler axioms for logic. So I
knew I’d come to the end of the road: after a century (or maybe even a
couple of millennia), we could finally say that the simplest possible
axiom for logic was known.
Not long after, I found two 2-axiom systems, also with 6 NANDs in total, that I proved could reproduce logic:
✕
{(p\[CenterDot]q)\[CenterDot](p\[CenterDot](q\[CenterDot]r))==p,p\[CenterDot]q==q\[CenterDot]p}
|
|
✕
{(p\[CenterDot]r)\[CenterDot](p\[CenterDot](q\[CenterDot]r))==p,p\[CenterDot]q==q\[CenterDot]p}
|
|
And if one chooses to take commutativity p · q = q · p for granted, then these show that all it takes to get logic is one tiny 4-NAND axiom.
Why It Matters
OK, so it’s neat to be able to say that one’s “finished
what Aristotle started” (or at least what Boole started) and found the
very simplest possible axiom system for logic. But is it just a
curiosity, or is there real significance to it?
Before the whole framework I developed in A New Kind of Science,
I think one would have been hard-pressed to view it as much more than a
curiosity. But now one can see that it’s actually tied into all sorts
of foundational questions, like whether one should consider mathematics
to be invented or discovered.
Mathematics as humans practice it is based on a handful of particular axiom systems—each
in effect defining a certain field of mathematics (say logic, or group
theory, or geometry, or set theory). But in the abstract, there are an
infinite number of possible axiom systems out there—in effect each defining a field of mathematics that could in principle be studied, even if we humans haven’t ever done it.
Before A New Kind of Science
I think I implicitly assumed that pretty much anything that’s just “out
there” in the computational universe must somehow be “less interesting”
than things we humans have explicitly built and studied. But my discoveries about simple programs
made it clear that at the very least there’s often lots of richness in
systems that are just “out there” than in ones that we carefully select.
So what about axiom systems for mathematics? Well, to
compare what’s just “out there” with what we humans have studied, we
have to know where the axiom systems for existing areas of mathematics
that we’ve studied—like logic—actually lie. And based on traditional
human-constructed axiom systems we’d conclude that they have to be far,
far out there—in effect only findable if one already knows where they
are.
But my axiom-system discovery basically answered the
question, “How far out is logic?” For something like cellular automata,
it’s particularly easy to assign a number (as I did in the early 1980s)
to each possible cellular automaton. It’s slightly harder to do this
with axiom systems, though not much. And in one approach, my axiom can
be labeled as 411;3;7;118—constructed in the Wolfram Language as:
✕
Groupings[{p, q, r}[[1 + IntegerDigits[411, 3, 7]]], CenterDot -> 2][[118]] == r
|
And at least in the space of possible functional forms
(not accounting for variable labeling), here’s a visual indication of
where the axiom lies:
Given how fundamental logic is to so many formal systems
we humans study, we might have thought that in any reasonable
representation, logic corresponds to one of the very simplest
conceivable axiom systems. But at least with the (NAND-based)
representation we’re using, that’s not true. There’s still by most
measures a very simple axiom system for it, but it’s perhaps the hundred
thousandth possible axiom system one would encounter if one just
started enumerating axiom systems starting from the simplest one.
So given this, the obvious next question is, what about
all the other axiom systems? What’s the story with those? Well, that’s
exactly the kind of investigation that A New Kind of Science
is all about. And indeed in the book I argue that things like the
systems we see in nature are often best captured precisely by those
“other rules” that we can find by enumerating possibilities.
In the case of axiom systems, I made a picture
that represents what happens in “fields of mathematics” corresponding
to different possible axiom systems. Each row shows the consequences of
a particular axiom system, with the boxes across the page indicating
whether a particular theorem is true in that axiom system. (Yes, at
some point Gödel’s Theorem
bites one, and it becomes irreducibly difficult to prove or disprove a
given theorem in a given axiom system; in practice, with my methods that
happened just a little further to the right than the picture shows…)
Is there something fundamentally special about “human-investigated” fields of mathematics?
From this picture, and other things I’ve studied, there doesn’t seem
to be anything obvious. And I suspect actually that the only thing
that’s really special about these fields of mathematics is the
historical fact that they are what have been studied. (One might make
claims like that they arise because they “describe the real world”, or
because they’re “related to how our brains work”, but the results in A New Kind of Science argue against these.)
Alright, well then what’s the significance of my axiom
system for logic? The size of it gives a sense of the ultimate
information content of logic as an axiomatic system. And it makes it
look like—at least for now—we should view logic as much more having been
“invented as a human construct” than having been “discovered” because
it was somehow “naturally exposed”.
If history had been different, and we’d routinely looked (in the manner of A New Kind of Science)
at lots of possible simple axiom systems, then perhaps we would have
“discovered” the axiom system for logic as one with particular
properties we happened to find interesting. But given that we have
explored so few of the possible simple axiom systems, I think we can
only reasonably view logic as something “invented”—by being constructed
in an essentially “discretionary” way.
In a sense this is how logic looked, say, back in the
Middle Ages—when the possible syllogisms (or valid forms of argument)
were represented by (Latin) mnemonics like bArbArA and cElErAnt. And to
mirror this, it’s fun to find mnemonics for what we now know is the
simplest possible axiom system for logic.
Starting with ((p · q) · r) · (p · ((p · r) · p)) = r, we can represent each p · q in prefix or Polish form (the reverse of the “reverse Polish” of an HP calculator) as Dpq—so the whole axiom can be written =DDDpqrDpDDprpr. Then (as Ed Pegg found for me) there’s an English mnemonic for this: FIGure OuT Queue, where p, q, r are u, r, e. Or, looking at first letters of words (with operator B, and p, q, r being a, p, c): “Bit by bit, a program computed Boolean algebra’s best binary axiom covering all cases”.
The Mechanics of Proof
OK, so how does one actually prove that my axiom system
is correct? Well, the most immediate thing to do is just to show that
from it one can derive a known axiom system for logic—like Sheffer’s
axiom system:
✕
{(p\[CenterDot]p)\[CenterDot](p\[CenterDot]p)==p,p\[CenterDot](q\[CenterDot](q\[CenterDot]q))==p\[CenterDot]p,(p\[CenterDot](q\[CenterDot]r))\[CenterDot](p\[CenterDot](q\[CenterDot]r))==((q\[CenterDot]q)\[CenterDot]p)\[CenterDot]((r\[CenterDot]r)\[CenterDot]p)}
|
There are three axioms here, and we’ve got to derive each of them. Well, with the latest version of the Wolfram Language, here’s what we do to derive, say, the second axiom:
✕
pf = FindEquationalProof[
p\[CenterDot](q\[CenterDot](q\[CenterDot]q)) ==
p\[CenterDot]p, \!\(
\*SubscriptBox[\(\[ForAll]\), \({p, q,
r}\)]\(\((\((p\[CenterDot]q)\)\[CenterDot]r)\)\[CenterDot]\((p\
\[CenterDot]\((\((p\[CenterDot]r)\)\[CenterDot]p)\))\) == r\)\)]
|
It’s pretty remarkable that it’s now possible to just do this. The “proof object”
records that 125 steps were used in the proof. And from this proof
object we can generate a notebook that describes each of those steps:
In outline, what happens is that a whole sequence of
intermediate lemmas are proved, which eventually allow the final result
to be derived. There’s a whole network of interdependencies between
lemmas, as this visualization shows:
✕
pf["ProofGraphWeighted"]
|
Here are the networks involved in deriving all three of
the axioms in the Sheffer axiom system—with the last one involving a
somewhat whopping 504 steps:
And, yes, it’s clear these are pretty complicated. But
before we discuss what that complexity means, let’s talk about what
actually goes on in the individual steps of these proofs.
The basic idea is straightforward. Let’s imagine we had an axiom that just said p · q = q · p. (Mathematically, this corresponds to the statement that · is commutative.) More precisely, what the axiom says is that for any expressions p and q, p · q is equivalent to q · p.
OK, so let’s say we wanted to derive from this axiom that (a · b) · (c · d) = (d · c) · (b · a). We could do this by using the axiom to transform d · c to c · d, b · a to a · b, and then finally (c · d) · (a · b) to (a · b) · (c · d).
FindEquationalProof
does essentially the same thing, though it chooses to do the steps in a
slightly different order, and modifies the left-hand side as well as
the right-hand side:
✕
pf = FindEquationalProof[(a\[CenterDot]b)\[CenterDot](c\[CenterDot]d) \
== (d\[CenterDot]c)\[CenterDot](b\[CenterDot]a), \!\(
\*SubscriptBox[\(\[ForAll]\), \({p, q}\)]\(p\[CenterDot]q ==
q\[CenterDot]p\)\)]["ProofNotebook"]
|
Once one’s got a proof like this, it’s straightforward
to just run through each of its steps, and check that they produce the
result that’s claimed. But how does one find the proof? There are lots
of different possible sequences of substitutions and transformations that one could do. So how does one find a sequence that successfully gets to the final result?
One might think: why not just try all possible
sequences, and if there is any sequence that works, one will eventually
find it? Well, the problem is that one quickly ends up with an
astronomical number of possible sequences to check. And indeed the main
art of automated theorem proving consists of finding ways to prune the number of sequences one has to check.
This quickly gets pretty technical, but the most
important idea is easy to talk about if one knows basic algebra. Let’s
say you’re trying to prove an algebraic result like:
✕
(-1 + x^2) (1 - x + x^2) (1 + x + x^2) == (-1 + x) (1 + x + x^2) (1 + x^3)
|
Well, there’s a guaranteed way to do this: just apply
the rules of algebra to expand out each side—and immediately one can see
they’re the same:
✕
{Expand[(-1 + x^2) (1 - x + x^2) (1 + x + x^2)],
Expand[(-1 + x) (1 + x + x^2) (1 + x^3)]}
|
Why does this work? Well, it’s because there’s a way of
taking algebraic expressions like this, and always systematically
reducing them so that eventually they get to a standard form. OK, but
so can one do the same thing for proofs with arbitrary axiom systems?
The answer is: not immediately. It works in algebra
because algebra has a special property that guarantees one can always
“make progress” in reducing expressions. But what was discovered
independently several times in the 1970s (under names like the Knuth–Bendix and the Gröbner Basis algorithm) is that even if an axiom system doesn’t intrinsically have the appropriate property, one can potentially find “completions” of it that do.
And that’s what’s going on in typical proofs produced by FindEquationalProof (which is based on the Waldmeister (“master of trees”) system).
There are so-called “critical pair lemmas” that don’t directly “make
progress” themselves, but make it possible to set up paths that do. And
the reason things get complicated is that even if the final expression
one’s trying to get to is fairly short, one may have to go through all
sorts of much longer intermediate expressions to get there. And so, for
example, for the proof of the first Sheffer axiom above, here are the
intermediate steps:
In this case, the largest intermediate form is about 4 times the size of the original axiom. Here it is:
✕
(p\[CenterDot]q)\[CenterDot](((p\[CenterDot]q)\[CenterDot](q\
\[CenterDot]((q\[CenterDot]q)\[CenterDot]q)))\[CenterDot](p\
\[CenterDot]q)) == (((q\[CenterDot](q\[CenterDot]((q\[CenterDot]q)\
\[CenterDot]q)))\[CenterDot]r)\[CenterDot]((p\[CenterDot]q)\
\[CenterDot](((p\[CenterDot]q)\[CenterDot](q\[CenterDot]((q\
\[CenterDot]q)\[CenterDot]q)))\[CenterDot](p\[CenterDot]q))))\
\[CenterDot](q\[CenterDot]((q\[CenterDot]q)\[CenterDot]q))
|
One can represent expressions like this as a tree. Here’s this one, compared to the original axiom:
And here’s how the sizes of intermediate steps evolve through the proofs found for each of the Sheffer axioms:
Why Is It So Hard?
Is it surprising that these proofs are so complicated?
In some ways, not really. Because, after all, we know perfectly well
that math can be hard. In principle it might have been that anything
that’s true in math would be easy to prove. But one of the side effects
of Gödel’s Theorem from 1931 was to establish that even things we can eventually prove can have proofs that are arbitrarily long.
And actually this is a symptom of the much more general phenomenon I call computational irreducibility. Consider a system governed, say, by the simple rule of a cellular automaton (and of course, every essay of mine must have a cellular automaton somewhere!). Now just run the system:
✕
ArrayPlot[CellularAutomaton[{2007,{3,1}},RandomInteger[2,3000],1500],Frame->False,ColorRules->{0->White,1->Hue[0.09, 1., 1.],2->Hue[0.03, 1., 0.76]}]
|
One might have thought that given that there’s a simple
rule that underlies the system, there’d always be a quick way to figure
out what the system will do. But that’s not the case. Because
according to my Principle of Computational Equivalence
the operation of the system will often correspond to a computation
that’s just as sophisticated as any computation that we could set up to
figure out the behavior of the system. And this means that the actual
behavior of the system in effect corresponds to an irreducible amount of
computational work that we can’t in general shortcut in any way.
In the picture above, let’s say we want to know whether
the pattern eventually dies out. Well, we could just keep running it,
and if we’re lucky it’ll eventually resolve to something whose outcome
is obvious. But in general there’s no upper bound to how far we’ll have
to go to, in effect, prove what happens.
When we do things like the logic proofs above, it’s a slightly different setup.
Instead of just running something according to definite rules, we’re
asking whether there exists a way to get to a particular result by
taking some series of steps that each follow a particular rule. And,
yes, as a practical computational problem, this is immediately more
difficult. But the core of the difficulty is still the same phenomenon
of computational irreducibility—and that this phenomenon implies that
there isn’t any general way to shortcut the process of working out what a
system will do.
Needless to say, there are plenty of things in the
world—especially in technology and scientific modeling, as well as in
areas where there are various forms of regulation—that have
traditionally been set up to implicitly avoid computational
irreducibility, and to operate in ways whose outcome can readily be
foreseen without an irreducible amount of computation.
But one of the implications of my Principle of Computational Equivalence
is that this is a rather singular and contrived situation—because it
says that computational irreducibility is in fact ubiquitous across
systems in the computational universe.
OK, but what about mathematics? Maybe somehow the rules
of mathematics are specially chosen to show computational reducibility.
And there are indeed some cases where that’s true (and in some sense
it even happens in logic). But for the most part it appears that the
axiom systems of mathematics are not untypical of the space of all
possible axiom systems—where computational irreducibility is inevitably
rampant.
What’s the Point of a Proof?
At some level, the point of a proof is to know that something is true. Of course, particularly in modern times, proof has very much taken a back seat
to pure computation. Because in practice it’s much more common to want
to generate things by explicit computation than it is to want to “go
back” and construct a proof that something is true.
In pure mathematics, though, it’s fairly common to deal with things that at least nominally involve an infinite number of cases
(“true for all primes”, etc.), for which at least direct computation
can’t work. And when it comes to questions of verification (“can this
program ever crash?” or “can this cryptocurrency ever get spent twice?”)
it’s often more reasonable to attempt a proof than to do something like
run all possible cases.
But in the actual practice of mathematics, there’s more
to proof than just establishing if things are true. Back when Euclid
first wrote his Elements, he just
gave results, and proofs were “left to the reader”. But for better or
worse, particularly over the past century, proof has become something
that doesn’t just happen behind the scenes, but is instead actually the
primary medium through which things are supposed to be communicated.
At some level I think it’s a quirk of history that
proofs are typically today presented for humans to understand, while
programs are usually just thought of as things for computers to run.
Why has this happened? Well, at least in the past, proofs could really
only be represented in essentially textual form—so if they were going to
be used, it would have to be by humans. But programs have essentially
always been written in some form of computer language. And for the
longest time, that language tended to be set up to map fairly directly
onto the low-level operations of the computer—which meant that it was
readily “understandable” by the computer, but not necessarily by humans.
But as it happens, one of the main goals of my own
efforts over the past several decades has been to change this—and to
develop in the Wolfram Language a true “computational communication language” in which computational ideas can be communicated in a way that is readily understandable to both computers and humans.
There are many consequences of having such a language.
But one of them is that it changes the role of proof. Let’s say one’s
looking at some mathematical result. Well, in the past the only
plausible way to communicate how one should understand it was to give a
proof that people could read. But now something different is possible:
one can give a Wolfram Language
program that computes the result. And in many ways this is a much more
powerful way to communicate why the result is true. Because every
piece of the program is something precise and unambiguous—that if one
wants to, one can actually run. There’s no issue of trying to divine
what some piece of text means, perhaps filling in some implicit
assumptions. Instead, everything is right there, in absolutely explicit
form.
OK, so what about proof? Are there in fact unambiguous
and precise ways to write proofs? Well, potentially yes, though it’s
not particularly easy. And even though the main Wolfram Language has
now existed for 30 years, it’s taken until pretty much now to figure out
a reasonable way to represent in it even such structurally
comparatively straightforward proofs as the one for my axiom system
above.
One can imagine authoring proofs in the Wolfram Language
much like one authors programs—and indeed we’re working on seeing how
to provide high-level versions of this kind of “proof assistant”
functionality. But the proof of my axiom system that I showed above is
not something anyone authored; it’s something that was found by the
computer. And as such, it’s more like the output of running a program
than like a program itself. (Like a program, though, the proof can in
some sense be “run” to verify the result.)
Generating Understandability
Most of the time when people use the Wolfram Language—or Wolfram|Alpha—they
just want to compute things. They’re interested in getting results,
not in understanding why they get the results they do. But in
Wolfram|Alpha, particularly in areas like math and chemistry, a popular
feature for students is “step-by-step solutions”:
When Wolfram|Alpha
does something like computing an integral, it’s using all sorts of
powerful systematic algorithmic techniques optimized for getting
answers. But when it’s asked to show steps it needs to do something
different: it needs instead to explain step by step why it gets the
result it does.
It wouldn’t be useful for it to explain how it actually
got the result; it’s a very non-human process. Instead, it basically
has to figure out how the kinds of operations humans learn can be used
to get the result. Often it’ll figure out some trick that can be used.
Yes, there’ll be a systematic way to do it that’ll always work. But it
involves too many “mechanical” steps. The “trick” (“trig
substitution”, “integration by parts”, whatever) won’t work in general,
but in this particular case it’ll provide a faster way to get to the
answer.
OK, but what about getting understandable versions of
other things? Like the operation of programs in general. Or like the
proof of my axiom system.
Let’s start by talking about programs. Let’s say one’s
written a program, and one wants to explain how it works. One
traditional approach is just to “include comments” in the code. Well,
if one’s writing in a traditional low-level language, that may be the
best one can do. But the whole point of the Wolfram Language
being a computational communication language is that the language
itself is supposed to allow you to communicate ideas, without needing
extra pieces of English text.
It takes effort to make a Wolfram Language
program be a good piece of exposition, just like it takes effort to
make English text a good piece of exposition. But one can end up with a
piece of Wolfram Language code that really explains very clearly how it
works just through the code itself.
Of course, it’s very common for the actual execution of
the code to do things that can’t readily be foreseen just from the
program. I’ll talk about extreme cases like cellular automata soon.
But for now let’s imagine that one’s constructed a program where there’s
some ability to foresee the broad outlines of what it does.
And in such a case, I’ve found that computational essays (presented as Wolfram Notebooks) are a great tool in explaining what’s going on. It’s crucial that the Wolfram Language
is symbolic, so it’s possible to run even the tiniest fragments of any
program on their own (with appropriate symbolic expressions as input or
output). And when one does this, one can present a succession of steps
in the program as a succession of elements in the dialog that forms the
core of a computational notebook.
In practice, it’s often critical to create
visualizations of inputs or outputs. Yes, everything can be represented
as an explicit symbolic expression. But we humans often have a much
easier time understanding things when they’re presented visually, rather
than as some kind of one-dimensional language-like string.
Of course, there’s something of an art to creating good visualizations. But in the Wolfram Language
we’ve managed to go a long way towards automating this art—often using
pretty sophisticated machine learning and other algorithms to do things
like lay out networks or graphics elements.
What about just starting from the raw execution trace
for a program? Well, it’s hard. I’ve done experiments on this for
decades, and never been very satisfied with the results. Yes, you can
zoom in to see lots of details of what’s going on. But when it comes to
knowing the “big picture” I’ve never found any particularly good
techniques for automatically producing things that are terribly useful.
At some level it’s similar to the general problem of
reverse engineering. You are shown some final machine code, chip
design, or whatever. But now you want to go backwards to reconstruct
the higher-level description that some human started from, that was
somehow “compiled” to what you see.
In the traditional approach to engineering, where one
builds things up incrementally, always somehow being able to foresee the
consequences of what one’s building, this approach can in principle
work. But if one does engineering by just searching the computational universe
to find an optimal program (much like I searched possible axiom systems
to find one for logic), then there’s no guarantee that there’s any
“human story” or explanation behind this program.
It’s a similar problem in natural science. You see some elaborate set of things happening in some biological system.
Can one “reverse engineer” these to find an “explanation” for them?
Sometimes one might be able to say, for example, that evolution by
natural selection would be likely to lead to something. Or that it’s
just common in the computational universe and so is likely to occur.
But there’s no guarantee that the natural world is set up in any way
that necessarily allows human explanation.
Needless to say, when one makes models for things,
one inevitably considers only the particular aspects that one’s
interested in, and idealizes everything else away. And particularly in
areas like medicine, it’s not uncommon to end up with some approximate
model that’s a fairly shallow decision tree that’s easy to explain, at
least as far as it goes.
The Nature of Explainability
What does it mean to say that something is explainable? Basically it’s that humans can understand it.
So what does it take for humans to understand something?
Well, somehow we have to be able to “wrap our brains around it”.
Let’s take a typical cellular automaton with complex behavior. A
computer has no problem following each step in the evolution. And with
immense effort a human could laboriously reproduce what a computer does.
But one wouldn’t say that means the human “understands”
what the cellular automaton is doing. To get to that point, the human
would have to be readily able to reason about how the cellular automaton
behaves, at some high level. Or put another way, the human would have
to be able to “tell a story” that other humans could readily understand,
about how the cellular automaton behaves.
Is there a general way to do this? Well, no, because of computational irreducibility.
But it can still be the case that certain features that humans choose
to care about can be explained in some reduced, higher-level way.
How does this work? Well, in a sense it requires that
some higher-level language be constructed that can describe the features
one’s interested in. Looking at a typical cellular automaton pattern,
one might try to talk not in terms of colors of huge numbers of
individual cells, but instead in terms of the higher-level structures
one can pick out. And the key point is that it’s possible to make at
least a partial catalog of these structures: even though there are lots
of details that don’t quite fit, there are still particular structures
that occur often.
And if we were going to start “explaining” the behavior of the cellular automaton,
we’d typically begin by giving the structures names, and then we’d
start talking about what’s going on in terms of these named things.
The case of a cellular automaton has an interesting
simplifying feature: because it operates according to simple
deterministic rules, there are structures that just repeat identically.
If we’re dealing with things in the natural world, for example, we
typically won’t see this kind of identical repetition. Instead, it’ll
just be that this tiger, say, is extremely similar to this other one, so
we can call them both “tigers”, even though their atoms are not
identical in their arrangement.
What’s the bigger picture of what’s going on? Well,
it’s basically that we’re using the idea of symbolic representation.
We’re saying that we can assign something—often a word—that we can use
to symbolically describe a whole class of things, without always having
to talk about all the detailed parts of each thing.
In effect it’s a kind of information compression: we’re
using symbolic constructs to find a shorter way to describe what we’re
interested in.
Let’s imagine we’ve generated a giant structure, say a mathematical one:
✕
Solve[a x^4 + b x^3 + c x^2 + d x + e == 0, x]
|
Well, a first step is to generate a kind of internal
higher-level representation. For example, we might find substructures
that appear repeatedly. And we might then assign names to them. And
then display a “skeleton” of the whole structure in terms of these
names:
And, yes, this kind of “dictionary compression”–like scheme is useful in bringing a first level of explainability.
But let’s go back to the proof of my axiom system. The
lemmas that were generated in this proof are precisely set up to be
elements that are used repeatedly (a bit like shared common
subexpressions). But even having in effect factored them out, we’re
still left with a proof that is not something that we humans can readily
understand.
So how can we go further? Well, basically we have to come up with some yet-higher-level description. But what might this be?
The Concept of Concepts
If you’re trying to explain something to somebody, it’s a
lot easier when there’s something similar that they’ve already
understood. Imagine trying to explain a modern drone
to someone from the Stone Age. It’d probably be pretty difficult. But
explaining it to someone from 50 years ago, who’d already seen
helicopters and model airplanes etc., would be a lot easier.
And ultimately the point is that when we explain
something, we do it in some language that both we and whoever we’re
explaining it to know. And the richer this language is, the fewer new
elements we have to introduce in order to communicate whatever it is
that we’re trying to explain.
There’s a pattern that’s been repeated throughout
intellectual history. Some particular collection of things gets seen a
bunch of times. And gradually it’s understood that these things are all
somehow abstractly similar. And they can all be described in terms of
some particular new concept, often referred to by some new word or
phrase.
Let’s say one had seen things like water and blood and
oil. Well, at some point one realizes that there’s a general concept of
“liquid”, and all of these can be described as liquids. And once one
has this concept, one can start reasoning in terms of it, and
identifying more concepts—like, say, viscosity—that build on it.
When does it makes sense to group things into a concept?
Well, that’s a difficult question, which can’t ultimately be answered
without foreseeing everything that might be done with that concept.
And in practice, in the evolution of human language and human ideas
there’s some kind of process of progressive approximation that goes on.
There’s a much more rapid recapitulation that happens in a modern machine learning system. Imagine taking all sorts of objects that one’s seen in the world, and just feeding them to FeatureSpacePlot
and seeing what comes out. Well, if one gets definite clusters in
feature space, then one might reasonably think that each of these
clusters should be identified as corresponding to a “concept”, that we
could for example label with a word.
Now, to be fair, what’s happening with FeatureSpacePlot—like in human intellectual development—is in some ways incremental. Because to lay the objects out in feature space, FeatureSpacePlot is using features that it’s learned how to extract from previous categorizations it knows about.
But, OK, given the world as it is, what are the best
categories—or best concepts—one can use to describe things? Well, it’s
an evolving story. And in fact breakthroughs—whether in science,
technology or elsewhere—are very often precisely associated with the
realization that some new category or concept can usefully be
identified.
But in the actual evolution of our civilization, there’s
a kind of spiral at work. First some particular concept is
identified—say the idea of a program. And once some concept has been
identified, people start using it, and thinking in terms of it. And
pretty soon all sorts of new things have been constructed on the basis
of that concept. But then another level of abstraction is identified,
and new concepts get constructed, building on top of the previous one.
It’s pretty much the same story for the technology stack
of modern civilization, and its “intellectual stack”. Both involve
towers of concepts, and successive levels of abstraction.
The Problem of Education
In order for people to be able to communicate using some
concept, they have to have learned about it. And, yes, there are some
concepts (like object permanence) that humans automatically learn by
themselves just by observing the natural world. But looking for example
at a list of common words
in modern English, it’s pretty clear that most of the concepts that we
now use in modern civilization aren’t ones that people can just learn
for themselves from the natural world.
Instead—much like a modern machine learning system—at
the very least they need some “specially curated” experience of the
world, organized to highlight particular concepts. And for more
abstract areas (like mathematics) they probably need explicit exposure
to the concepts themselves in their raw abstract forms.
But, OK, as the “intellectual stack” of civilization
advances, will we always have to learn progressively more? We might
worry that at some point our brains just won’t be able to keep up, and
we’d have to add some kind of augmentation. But perhaps fortunately, I
think it’s one of those cases where the problem can instead most likely
be “solved in software”.
The issue is this: At any given point in history,
there’s a certain set of concepts that are important in being able to
operate in the world as it is at that time. And, yes, as civilization
progresses new things are discovered, and new concepts are introduced.
But there’s another process at work as well: new concepts bring new
levels of abstraction, which typically subsume large numbers of earlier
concepts.
We often see this in technology. There was a time when
to operate a computer you needed to know all sorts of low-level details.
But over time those got abstracted away, so all you need to know is
some general concept. You click an icon and things start to happen—and
you don’t have to understand operating systems, or interrupt handlers or
schedulers, or any of those details.
Needless to say, the Wolfram Language provides a great example of all this. Because it goes to tremendous trouble to “automate out”
lots of low-level details (for example about what specific algorithm to
use) and let human users just think about things in terms of
higher-level concepts.
Yes, there still need to be some people who understand
the details “underneath” the abstraction (though I’m not sure how many
flint knappers modern society needs). But mostly education can
concentrate on teaching at a higher level.
There’s often an implicit assumption in education that
to reach higher-level concepts one has to somehow recapitulate the
history of how those concepts were historically arrived at. But
usually—and perhaps always—this doesn’t seem to be true. In an extreme
case, one might imagine that to teach about computers, one would have to
recapitulate the history of mathematical logic. But actually we know
that people can go straight to modern concepts of computing, without recapitulating any of the history.
But what is ultimately the understandability network of
concepts? Are there concepts that can only be understood if one already
understands other concepts? Given a particular ambient experience for a
human (or particular background training for a neural network) there is
presumably some ordering.
But I suspect that something analogous to computational
universality probably implies that if one’s just dealing with a “raw
brain” then one could start anywhere. So if some alien were exposed to
category theory and little else from the very beginning, they’d no doubt
build a network of concepts where this is at the root, and maybe what
for us is basic arithmetic would be something only reached in their
analog of math graduate school.
Of course, such an alien might form their technology
stack and their built environment in a quite different way from us—much
as the recent history of our own civilization might have been very
different if computers had successfully been developed in the 1800s rather than in the mid-1900s.
The Progress of Mathematics
I’ve often wondered to what extent the historical
trajectory of human mathematics is an “accident”, and to what extent
it’s somehow inexorable. As I mentioned earlier, at the level of formal
systems there are many possible axiom systems from which one could
construct something that is formally like mathematics.
But the actual history of mathematics did not start with
arbitrary axiom systems. It started—in Babylonian times—with efforts
to use arithmetic for commerce and geometry for land surveying. And
from these very practical origins, successive layers of abstraction have
been added that have led eventually to modern mathematics—with for
example numbers being generalized
from positive integers, to rationals, to roots, to all integers, to
decimals, to complex numbers, to algebraic numbers, to quaternions and
so on.
Is there an inexorability to this progression of
abstraction? I suspect to some extent there is. And probably it’s a
similar story as with other kinds of concept formation. Given some
stage that’s been reached, there are various things that can readily get
studied, and after a while groups of them are seen to be examples of
more general and abstract constructs—which then in turn define another
stage from which new things can be studied.
Are there ways to break out of this cycle? One
possibility would be through doing experiments in mathematics. Yes, one
can systematically prove things about particular mathematical systems.
But one can also just empirically notice mathematical facts—like Ramanujan’s observation that ![Exp[Pi Sqrt[163]]](https://content.wolfram.com/uploads/sites/43/2018/11/img66.png "Exp[Pi Sqrt[163]]")
is numerically close to an integer. And the question is: are things
like this just “random facts of mathematics” or do they somehow fit into
the whole “fabric of mathematics”?
One can ask the same kind of thing about questions in mathematics. Is the question of whether odd perfect numbers exist
(which has been unanswered since Pythagoras) a core question in
mathematics, or is it, in a sense, a random question that doesn’t
connect into the fabric of mathematics?
Just like one can enumerate things like axiom systems,
so also one can imagine enumerating possible questions in mathematics.
But if one does this, I suspect there’s immediately an issue. Gödel’s Theorem
establishes that in axiom systems like the one for arithmetic there are
“formally undecidable” propositions, that can’t be proved or disproved
from within the axiom system.
But the particular examples that Gödel constructed
seemed far from anything that would arise naturally in doing
mathematics. And for a long time it was assumed that somehow the
phenomenon of undecidability was something that, while in principle
present, wasn’t going to be relevant in “real mathematics”.
However, with my Principle of Computational Equivalence and my experience in the computational universe, I’ve come to the strong conclusion that this isn’t correct—and that instead undecidability is actually close at hand
even in typical mathematics as it’s been practiced. Indeed, I won’t be
surprised if a fair fraction of the current famous unsolved problems of
mathematics (Riemann Hypothesis, P=NP, etc.) actually turn out to be in effect undecidable.
But if there’s undecidability all around, how come
there’s so much mathematics that’s successfully been done? Well, I
think it’s because the things that have been done have implicitly been
chosen to avoid undecidability, basically just by virtue of the way
mathematics has been built up. Because if what one’s doing is basically
to form progressive levels of abstraction based on things one has shown
are true, one’s basically setting up a path that’s going to be able to
move forward without being forced into undecidability.
Of course, doing experimental mathematics
or asking “random questions” may immediately land one in some area
that’s full of undecidability. But at least so far in its history, this
hasn’t been the way the mainstream discipline of mathematics has
evolved.
So what about those “random facts of mathematics”?
Well, it’s pretty much like in other areas of intellectual endeavor.
“Random facts” don’t really get integrated into a line of intellectual
development until some structure—and typically some abstract
concepts—are built around them.
My own favorite discoveries about the origins of complexity in systems like the rule 30 cellular automaton are a good example. Yes, similar phenomena had been seen—even millennia earlier (think: randomness in the sequence of primes). But without a broader conceptual framework nobody really paid attention to them.
Nested patterns are another example. There are isolated examples of these in mosaics from the 1200s, but nobody really paid attention to them until the whole framework around nesting and fractals emerged in the 1980s.
It’s the same story over and over again: until abstract
concepts around them have been identified, it’s hard to really think
about new things, even when one encounters phenomena that exhibit them.
And so, I suspect, it is with mathematics: there’s a
certain inevitable layering of abstract concept on top of abstract
concept that defines the trajectory of mathematics. Is it a unique
path? Undoubtedly not. In the vast space of possible mathematical
facts, there are particular directions that get picked, and built along.
But others could have been picked instead.
So does this mean that the subject matter of mathematics
is inevitably dominated by historical accidents? Not as much as one
might think. Because—as mathematics has discovered over and over again,
starting with things like algebra and geometry—there’s a remarkable
tendency for different directions and different approaches to wind up
having equivalences or correspondences in the end.
And probably at some level this is a consequence of the Principle of Computational Equivalence,
and the phenomenon of computational universality: even though the
underlying rules (or underlying “language”) used in different areas of
mathematics are different, there ends up being some way to translate
between them—so that at the next level of abstraction the path that was
taken no longer critically matters.
The Logic Proof and the Automation of Abstraction
OK, so let’s go back to the logic proof. How does it
connect to typical mathematics? Well, right now, it basically doesn’t.
Yes, the proof has the same nominal form as a standard mathematical
proof. But it isn’t “human-mathematician friendly”. It’s all just
mechanical details. It doesn’t connect to higher-level abstract
concepts that a human mathematician can readily understand.
It would help a lot if we discovered that nontrivial lemmas in the proof already appeared in the mathematics literature.
(I don’t think any of them do, but our theorem-searching capabilities
haven’t gotten to the point where one can be sure.) But if they did
appear, then this would likely give us a way to connect these lemmas to
other things in mathematics, and in effect to identify a circle of
abstract concepts around them.
But without that, how can the proof become explainable?
Well, maybe there’s just a different way to do the proof
that’s fundamentally more connected to existing mathematics. But even
given the proof as we have it now, one could imagine “building out” new
concepts that would define a higher level of abstraction and put the
proof in a more general context.
I’m not sure how to do either of these things. I’ve considered sponsoring a prize (analogous to my 2007 Turing machine prize)
for “making the proof explainable”. But it’s not at all clear how one
could objectively judge “explainability”. (Maybe one could ask for a
1-hour video that would successfully explain the proof to a typical
mathematician—but this is definitely rather subjective.)
But just like we can automate things like finding aesthetic layouts for networks,
perhaps we can automate the process of making a proof explainable. The
proof as it is right now basically just says (without explanation),
“Consider these few hundred lemmas”. But let’s say we could identify a
modest number of “interesting” lemmas. Maybe we could somehow add these
to our canon of known mathematics and then be able to use them to
understand the proof.
There’s an analogy here with language design. In building up the Wolfram Language
what I’ve basically done is to try to identify “lumps of computational
work” that people will often want. Then we make these into built-in functions in the language, with particular names that people can use to refer to them.
A similar process goes on—though in a much less
organized way—in the evolution of human natural languages. “Lumps of
meaning” that turn out to be useful eventually get represented by words
in the language. Sometimes they start as phrases constructed out of a
few existing words. But the most impactful ones are typically
sufficiently far away from anything that has come before that they just
arrive as new words with potentially quite-hard-to-give definitions.
In the design of the Wolfram Language—with functions named with English words—I leverage
the “ambient understanding” that comes from the English words (and
sometimes from their meanings in common applications of computation).
One would want to do something similar in identifying
lemmas to add to our canon of mathematics. Not only would one want to
make sure that each lemma was somehow “intrinsically interesting”, but
one would also want when possible to select lemmas that are “easy to
reach” from existing known mathematical results and concepts.
But what does it mean for a lemma to be “intrinsically interesting”? I have to say that before I worked on A New Kind of Science,
I assumed that there was great arbitrariness and historical accident in
the choice of lemmas (or theorems) in any particular areas of
mathematics that get called out and given names in typical textbooks.
But when I looked in detail at theorems in basic logic, I was surprised to find something different. Let’s say one arranges all the true theorems of basic logic in order of their sizes (e.g. p = p might come first; p AND p = p
a bit later, and so on). When one goes through this list there’s lots
of redundancy. Indeed, most of the theorems end up being trivial
extensions of theorems that have already appeared in the list.
But just sometimes one gets to a theorem that
essentially gives new information—and that can’t be proved from the
theorems that have already appeared in the list. And here’s the
remarkable fact: there are 14 such theorems, and they essentially correspond exactly with the theorems that are typically given names in textbooks of logic. (Here AND is ∧, OR is ∨, and NOT is ¬.)
In other words, at least in this case, the named or
“interesting” theorems are the ones that give minimal statements of new
information. (Yes, after a while, by this definition there will be no
new information, because one will have encountered all the axioms needed
to prove anything that can be proved—though one can go a bit further
with this approach by starting to discuss limiting the complexity of
proofs that are allowed.)
What about with NAND theorems, like the ones in the proof? Once again, one can arrange all true NAND theorems in order—and then find which of them can’t be proved from any earlier in the list:
✕
{{a\[CenterDot]b==b\[CenterDot]a,a==(a\[CenterDot]a)\[CenterDot](a\[CenterDot]a),a==(a\[CenterDot]a)\[CenterDot](a\[CenterDot]b),(a\[CenterDot]a)\[CenterDot]a==(b\[CenterDot]b)\[CenterDot]b,(a\[CenterDot]a)\[CenterDot]b==(a\[CenterDot]b)\[CenterDot]b,a\[CenterDot]((a\[CenterDot]b)\[CenterDot]c)==a\[CenterDot]((b\[CenterDot]b)\[CenterDot]c)},{a\[CenterDot]b==b\[CenterDot]a,a==(a\[CenterDot]a)\[CenterDot](a\[CenterDot]a),a==(a\[CenterDot]a)\[CenterDot](a\[CenterDot]b),a==(a\[CenterDot]a)\[CenterDot](b\[CenterDot]a),a==(a\[CenterDot]b)\[CenterDot](a\[CenterDot]a),a==(b\[CenterDot]a)\[CenterDot](a\[CenterDot]a),(a\[CenterDot]a)\[CenterDot]a==a\[CenterDot](a\[CenterDot]a),(a\[CenterDot]a)\[CenterDot]a==(b\[CenterDot]b)\[CenterDot]b,a\[CenterDot](a\[CenterDot]a)==(b\[CenterDot]b)\[CenterDot]b,(a\[CenterDot]a)\[CenterDot]a==b\[CenterDot](b\[CenterDot]b),a\[CenterDot](a\[CenterDot]a)==b\[CenterDot](b\[CenterDot]b),a\[CenterDot](a\[CenterDot]b)==(a\[CenterDot]b)\[CenterDot]a,a\[CenterDot](a\[CenterDot]b)==a\[CenterDot](b\[CenterDot]a),(a\[CenterDot]a)\[CenterDot]b==(a\[CenterDot]b)\[CenterDot]b,a\[CenterDot](a\[CenterDot]b)==a\[CenterDot](b\[CenterDot]b),a\[CenterDot](a\[CenterDot]b)==(b\[CenterDot]a)\[CenterDot]a,(a\[CenterDot]a)\[CenterDot]b==b\[CenterDot](a\[CenterDot]a),(a\[CenterDot]a)\[CenterDot]b==(b\[CenterDot]a)\[CenterDot]b,(a\[CenterDot]a)\[CenterDot]b==b\[CenterDot](a\[CenterDot]b),a\[CenterDot](a\[CenterDot]b)==(b\[CenterDot]b)\[CenterDot]a,(a\[CenterDot]a)\[CenterDot]b==b\[CenterDot](b\[CenterDot]a),(a\[CenterDot]b)\[CenterDot]a==a\[CenterDot](b\[CenterDot]a),(a\[CenterDot]b)\[CenterDot]a==a\[CenterDot](b\[CenterDot]b),a\[CenterDot](b\[CenterDot]a)==a\[CenterDot](b\[CenterDot]b),(a\[CenterDot]b)\[CenterDot]a==(b\[CenterDot]a)\[CenterDot]a,a\[CenterDot](b\[CenterDot]a)==(b\[CenterDot]a)\[CenterDot]a,(a\[CenterDot]b)\[CenterDot]a==(b\[CenterDot]b)\[CenterDot]a,a\[CenterDot](b\[CenterDot]a)==(b\[CenterDot]b)\[CenterDot]a,a\[CenterDot](b\[CenterDot]b)==(b\[CenterDot]a)\[CenterDot]a,(a\[CenterDot]b)\[CenterDot]b==b\[CenterDot](a\[CenterDot]a),(a\[CenterDot]b)\[CenterDot]b==(b\[CenterDot]a)\[CenterDot]b,(a\[CenterDot]b)\[CenterDot]b==b\[CenterDot](a\[CenterDot]b),a\[CenterDot](b\[CenterDot]b)==(b\[CenterDot]b)\[CenterDot]a,(a\[CenterDot]b)\[CenterDot]b==b\[CenterDot](b\[CenterDot]a),a\[CenterDot](b\[CenterDot]c)==a\[CenterDot](c\[CenterDot]b),(a\[CenterDot]b)\[CenterDot]c==(b\[CenterDot]a)\[CenterDot]c,a\[CenterDot](b\[CenterDot]c)==(b\[CenterDot]c)\[CenterDot]a,(a\[CenterDot]b)\[CenterDot]c==c\[CenterDot](a\[CenterDot]b),a\[CenterDot](b\[CenterDot]c)==(c\[CenterDot]b)\[CenterDot]a,(a\[CenterDot]b)\[CenterDot]c==c\[CenterDot](b\[CenterDot]a),(a\[CenterDot]a)\[CenterDot](a\[CenterDot]a)==(a\[CenterDot]a)\[CenterDot](a\[CenterDot]b),(a\[CenterDot]a)\[CenterDot](a\[CenterDot]a)==(a\[CenterDot]a)\[CenterDot](b\[CenterDot]a),(a\[CenterDot]a)\[CenterDot](a\[CenterDot]a)==(a\[CenterDot]b)\[CenterDot](a\[CenterDot]a),(a\[CenterDot]a)\[CenterDot](a\[CenterDot]a)==(b\[CenterDot]a)\[CenterDot](a\[CenterDot]a),(a\[CenterDot]a)\[CenterDot](a\[CenterDot]b)==(a\[CenterDot]a)\[CenterDot](a\[CenterDot]c),(a\[CenterDot]a)\[CenterDot](a\[CenterDot]b)==(a\[CenterDot]a)\[CenterDot](b\[CenterDot]a),(a\[CenterDot]a)\[CenterDot](a\[CenterDot]b)==(a\[CenterDot]a)\[CenterDot](c\[CenterDot]a),(a\[CenterDot]a)\[CenterDot](a\[CenterDot]b)==(a\[CenterDot]b)\[CenterDot](a\[CenterDot]a)},{a\[CenterDot]((a\[CenterDot]b)\[CenterDot]b)==(c\[CenterDot](a\[CenterDot]a))\[CenterDot]a,a\[CenterDot]((a\[CenterDot]b)\[CenterDot]b)==((c\[CenterDot]a)\[CenterDot]c)\[CenterDot]a,a\[CenterDot]((a\[CenterDot]b)\[CenterDot]b)==(c\[CenterDot](a\[CenterDot]c))\[CenterDot]a,(a\[CenterDot](a\[CenterDot]b))\[CenterDot]b==(c\[CenterDot](b\[CenterDot]b))\[CenterDot]b,(a\[CenterDot](a\[CenterDot]b))\[CenterDot]b==((c\[CenterDot]b)\[CenterDot]c)\[CenterDot]b,(a\[CenterDot](a\[CenterDot]b))\[CenterDot]b==(c\[CenterDot](b\[CenterDot]c))\[CenterDot]b,a\[CenterDot]((a\[CenterDot]b)\[CenterDot]b)==(c\[CenterDot](c\[CenterDot]a))\[CenterDot]a,(a\[CenterDot](a\[CenterDot]b))\[CenterDot]b==(c\[CenterDot](c\[CenterDot]b))\[CenterDot]b,a\[CenterDot]((a\[CenterDot]b)\[CenterDot]b)==((c\[CenterDot]c)\[CenterDot]c)\[CenterDot]a,a\[CenterDot]((a\[CenterDot]b)\[CenterDot]b)==(c\[CenterDot](c\[CenterDot]c))\[CenterDot]a,(a\[CenterDot](a\[CenterDot]b))\[CenterDot]b==((c\[CenterDot]c)\[CenterDot]c)\[CenterDot]b,(a\[CenterDot](a\[CenterDot]b))\[CenterDot]b==(c\[CenterDot](c\[CenterDot]c))\[CenterDot]b,a\[CenterDot](a\[CenterDot](b\[CenterDot]c))==a\[CenterDot](a\[CenterDot](c\[CenterDot]b)),(a\[CenterDot](a\[CenterDot]b))\[CenterDot]c==((a\[CenterDot]b)\[CenterDot]a)\[CenterDot]c,(a\[CenterDot](a\[CenterDot]b))\[CenterDot]c==(a\[CenterDot](b\[CenterDot]a))\[CenterDot]c,a\[CenterDot]((a\[CenterDot]b)\[CenterDot]c)==a\[CenterDot]((b\[CenterDot]a)\[CenterDot]c),((a\[CenterDot]a)\[CenterDot]b)\[CenterDot]c==((a\[CenterDot]b)\[CenterDot]b)\[CenterDot]c,(a\[CenterDot](a\[CenterDot]b))\[CenterDot]c==(a\[CenterDot](b\[CenterDot]b))\[CenterDot]c,a\[CenterDot]((a\[CenterDot]b)\[CenterDot]c)==a\[CenterDot]((b\[CenterDot]b)\[CenterDot]c),a\[CenterDot]((a\[CenterDot]b)\[CenterDot]c)==((a\[CenterDot]b)\[CenterDot]c)\[CenterDot]a,a\[CenterDot](a\[CenterDot](b\[CenterDot]c))==(a\[CenterDot](b\[CenterDot]c))\[CenterDot]a,a\[CenterDot](a\[CenterDot](b\[CenterDot]c))==a\[CenterDot]((b\[CenterDot]c)\[CenterDot]a),a\[CenterDot](a\[CenterDot](b\[CenterDot]c))==((a\[CenterDot]b)\[CenterDot]c)\[CenterDot]c,(a\[CenterDot](a\[CenterDot]b))\[CenterDot]c==(a\[CenterDot](b\[CenterDot]c))\[CenterDot]c,a\[CenterDot]((a\[CenterDot]b)\[CenterDot]c)==a\[CenterDot]((b\[CenterDot]c)\[CenterDot]c),a\[CenterDot]((a\[CenterDot]b)\[CenterDot]c)==a\[CenterDot](c\[CenterDot](a\[CenterDot]b)),a\[CenterDot](a\[CenterDot](b\[CenterDot]c))==(a\[CenterDot](c\[CenterDot]b))\[CenterDot]a,a\[CenterDot](a\[CenterDot](b\[CenterDot]c))==a\[CenterDot]((c\[CenterDot]b)\[CenterDot]a),a\[CenterDot]((a\[CenterDot]b)\[CenterDot]c)==a\[CenterDot](c\[CenterDot](b\[CenterDot]a)),a\[CenterDot](a\[CenterDot](b\[CenterDot]c))==((a\[CenterDot]c)\[CenterDot]b)\[CenterDot]b,a\[CenterDot]((a\[CenterDot]b)\[CenterDot]c)==a\[CenterDot](c\[CenterDot](b\[CenterDot]b)),((a\[CenterDot]a)\[CenterDot]b)\[CenterDot]c==((a\[CenterDot]c)\[CenterDot]b)\[CenterDot]c,(a\[CenterDot](a\[CenterDot]b))\[CenterDot]c==(a\[CenterDot](c\[CenterDot]b))\[CenterDot]c,a\[CenterDot]((a\[CenterDot]b)\[CenterDot]c)==a\[CenterDot]((c\[CenterDot]b)\[CenterDot]c),a\[CenterDot]((a\[CenterDot]b)\[CenterDot]c)==a\[CenterDot](c\[CenterDot](b\[CenterDot]c)),a\[CenterDot]((a\[CenterDot]b)\[CenterDot]c)==a\[CenterDot](c\[CenterDot](c\[CenterDot]b))}}
|
NAND doesn’t have the same kind of historical tradition as AND, OR and NOT. (And there doesn’t seem to be any human language that, for example, has a single ordinary word for NAND.) But in the list of NAND theorems, the first highlighted one is easy to recognize as commutativity of NAND. After that, one really has to do a bit of translation to name the theorems: a = (a · a) · (a · a) is like the law of double negation, a = (a · a) · (a · b) is like the absorption law, (a · a) · b = (a · b) · b is like “weakening”, and so on.
But, OK, so if one’s going to learn just a few “key theorems” of NAND logic, which should they be? Perhaps they should be theorems that appear as “popular lemmas” in proofs.
Of course, there are many possible proofs of any given theorem. But let’s say we just use the particular proofs that FindEquationalProof generates. Then it turns out that in the proofs of the first thousand NAND theorems the single most popular lemma is a · a = a · ((a · a) · a), followed by such lemmas as (a · ((a · a) · a)) · (a · (a · ((a · a) · a))) = a.
What are these? Well, for the particular methods that FindEquationalProof uses, they’re useful. But for us humans they don’t seem terribly helpful.
But what about popular lemmas that happen to be short? a · b = b · a is definitely not the most popular lemma, but it is the shortest. (a · a) · (a · a) = a is more popular, but longer. And then there are lemmas like (a · a) · (b · a) = a.
But how useful are these lemmas? Here’s a way to test. Look at the first thousand NAND theorems, and see how much adding the lemmas shortens the proofs of these theorems (at least as found by FindEquationalProof):
a · b = b · a is very successful, often cutting down the proof by nearly 100 steps. (a · a) · (a · a) = a is much less successful; in fact, it actually sometimes seems to “confuse” FindEquationalProof, causing it to take more rather than fewer steps (visible as negative values in the plot). (a · a) · (b · a) = a is OK at shortening, but not as good as a · b = b · a. Though if one combines it with a · b = b · a, the result is more consistent shortening.
One could go on with this analysis, say including a
comparison of how much shortening is produced by a given lemma,
relative to how long its own proof was. But the problem is that if one
adds several “useful lemmas”, like a · b = b · a and (a · a) · (b · a) = a, there are still plenty of long proofs—and thus a lot left to “understand”:
What Can One Understand?
There are different ways to create models of things.
For a few hundred years, exact science was dominated by the idea of
finding mathematical equations that could be solved to say how things
should behave. But in pretty much the time since A New Kind of Science appeared, there’s been a strong shift to instead set up programs that can be run to say how things should behave.
Sometimes those programs are explicitly constructed for a
particular purpose; sometimes they’re exhaustively searched for. And
in modern times, at least one class of such programs is deduced using
machine learning, essentially by going backwards from examples of how
the system is known to behave.
OK, so with these different forms of modeling, how easy
is it to “understand what’s going on”? With mathematical equations,
it’s a big plus when it’s possible to find an “exact solution”—in which
the behavior of the system can be represented by something like an
explicit mathematical formula. And even when this doesn’t happen, it’s
fairly common to be able to make at least some mathematical statements
that are abstract enough to connect to other systems and other
behaviors.
As I discussed above, with a program—like a cellular
automaton—it can be a different story. Because it’s common to be thrust
immediately into computational irreducibility, which ultimately limits
how much one can ever hope to shortcut or “explain” what’s going on.
But what about with machine learning, and, say, with neural nets? At
some level, the training of a neural net is like recapitulating
inductive discovery in natural science. One’s trying to start from
examples and deduce a model for how a system behaves. But then can one
understand the model?
Again there are issues of computational irreducibility.
But let’s talk about a case where we can at least imagine what it would
look like to understand what’s going on.
Instead of using a neural net to model how some system behaves, let’s consider making a neural net that classifies some aspect of the world: say, takes images and classifies them
according to what they’re images of (“boat”, “giraffe”, etc.). When we
train the neural net, it’s learning to give correct final outputs.
But potentially one can think of the way it does this as being to
internally make a sequence of distinctions (a bit like playing a game of
Twenty Questions) that eventually determines the correct output.
But what are those distinctions? Sometimes we can recognize
some of them. “Is there a lot of blue in the image?”, for example. But
most of the time they’re essentially features of the world that we
humans don’t notice. Maybe there’s an alternative history of natural
science where some of them would have shown up. But they’re not things
that are part of our current canon of perception or analysis.
If we wanted to add them, we’d probably end up inventing
words for them. But the situation is very similar to the one with the
logic proof. An automated system has created things that it’s
effectively using as “waypoints” in generating a result. But they’re
not waypoints we recognize or relate to.
Once again, if we found that particular distinctions
were very common for neural nets, we might decide that those are
distinctions that are worth us humans learning, and adding to our
standard canon of ways to describe the world.
Can we expect that a modest number of such distinctions
would go a long way? It’s analogous to asking whether a modest number
of theorems would go a long way in understanding something like the
logic proof.
My guess is that the answer is fuzzy. If one looks, for example, at a large corpus of math papers, one can ask how common different theorems are. It turns out that the frequency of theorems follows an almost perfect Zipf law (with the Central Limit Theorem, the Implicit Function Theorem and Fubini’s Theorem
as the top three). And it’s probably the same with distinctions that
are “worth knowing”, or new theorems that are “worth knowing”.
Knowing a few will get one a certain distance, but there’ll be an infinite power-law tail, and one will never get to the end.
The Future of Knowledge
Whether one looks at mathematics, science or technology,
one sees the same basic qualitative progression of building a stack of
increasing abstraction. It would be nice to be able to quantify this
process. Perhaps one could look at how certain terms or descriptions
that are common at one time later get subsumed into higher levels of
abstraction, which then in turn have new terms or descriptions
associated with them.
Maybe one could create an idealized model of this process using some formal model of computation, like Turing machines.
Imagine that at the lowest level one has a basic Turing machine, with
no abstraction. Now imagine selecting programs for this Turing machine
according to some defined random process. Then run these programs and
analyze them to see what “higher-level” model of computation can
successfully reproduce the aggregate behavior of these programs without
having to run each step in each program.
One might have thought that computational irreducibility
would imply that this higher-level model of computation would
inevitably be more complicated in its construction. But the key point
is that we’re only trying to reproduce the aggregate behavior of the
programs, not their individual behavior.
OK, but so then what happens if you iterate this
process—essentially recapitulating idealized human intellectual history
and building a progressive tower of abstraction?
Conceivably there’s some analogy to critical phenomena in physics, and to the renormalization group.
And if so, one might imagine being able to identify a definite
trajectory in the space of what amount to concept representation
frameworks. What will the trajectory do?
Maybe it’ll have some kind of fixed-point behavior,
representing the guess that at any point in history there are about the
same number of abstract concepts that are worth learning—with new ones
slowly being invented, and old ones being subsumed.
What might any of this mean for mathematics? One guess
might be that any “random fact of mathematics”, say discovered
empirically, would eventually be covered when some level of abstraction
is reached. It’s not obvious how this process would work. After all,
at any given level of abstraction, there are always new empirical facts
to be “jumped to”. And it might very well be that the “rising tide of
abstraction” would move only slowly compared to the rate at which such
jumps could be made.
The Future of Understanding
OK, so what does all this mean for the future of understanding?
In the past, when humans looked, say, at the natural world, they had few pretensions to understand it. Sometimes they would personify
certain aspects of it in terms of spirits or deities. But they saw it
as just acting as it did, without any possibility for humans to
understand in detail why.
But with the rise of modern science—and especially as
more of our everyday existence came to be in built environments
dominated by technology (or regulatory structures) that we had
designed—these expectations changed. And as we look at computation or
AI today, it seems unsettling that we might not be able to understand
it.
But ultimately there’s always going to be a competition
between what the systems in our world do, and what our brains are
capable of computing about them. If we choose to interact only with
systems that are computationally much simpler than our brains, then,
yes, we can expect to use our brains to systematically understand what
the systems are doing.
But if we actually want to make full use of the
computational capabilities that our universe makes possible, then it’s
inevitable that the systems we’re dealing with will be equivalent in
their computational capabilities to our brains. And this means that—as
computational irreducibility implies—we’ll never be able to
systematically “outthink” or “understand” those systems.
But then how can we use them? Well, pretty much like
people have always used systems from the natural world. Yes, we don’t
know everything about how they work or what they might do. But at some
level of abstraction we know enough to be able to see how to get
purposes we care about achieved with them.
What about in an area like mathematics? In mathematics
we’re used to building our stack of knowledge so that each step is
something we can understand. But experimental mathematics—as well as
things like automated theorem proving—make it clear that there are
places to go that won’t have this feature.
Will we call this “mathematics”? I think we should.
But it’s a different tradition from what we’ve mostly used for the past
millennium. It’s one where we can still build abstractions, and we can
still construct new levels of understanding.
But somewhere underneath there will be all sorts of
computational irreducibility that we’ll never really be able to bring
into the realm of human understanding. And that’s basically what’s
going on in the proof of my little axiom for logic. It’s an early
example of what I think will be the dominant experience in
mathematics—and a lot else—in the future.
![](https://blogger.googleusercontent.com/img/proxy/AVvXsEgiYV_qJof_iG3Vfme-VO0SYYPzs1aybB5LTgE0xw-lYZ-B80MJMw9p2cefwChHUmES3FgIa_Zr3uk3tonjksLNddOSOTJjWre5kw84WPYA-nR_9fs3ldFzFiBAO2-0-cl-lRVmFBj5YJIlCoKkZqRMjyU7g00NqvKpPg=s0-d-e1-ft"")
