In an earlier section, we discussed how paths in a multiway graph can represent proofs of “equivalence” between expressions (or the “entailment” of one expression by another). For example, with the rule (or “axiom”)
this shows a path that “proves” that “BA entails AAB”:
But once we know this, we can imagine adding this result (as what we can think of as a “lemma”) to our original rule:
And now (the “theorem”) “BA entails AAB” takes just one step to prove—and all sorts of other proofs are also shortened:
It’s perfectly possible to imagine evolving a multiway system with a kind of “caching-based” speed-up mechanism where every new entailment discovered is added to the list of underlying rules. And, by the way, it’s also possible to use two-way rules throughout the multiway system:
But accumulative systems provide a much more principled way to progressively “add what’s discovered”. So what do proofs look like in such systems?
Consider the rule:
Running it for 2 steps we get the token-event graph:
Now let’s say we want to prove that the original “axiom” ABB implies (or “entails”) the “theorem” AAABAB. Here’s the subgraph that demonstrates the result:
And here it is as a separate “proof graph”
where each event takes two inputs—the “rule to be applied” and the “rule to apply to”—and the output is the derived (i.e. entailed or implied) new rule or rules.
If we run the accumulative system for another step, we get:
Now there are additional “theorems” that have been generated. An example is:
And now we can find a proof of this theorem:
This proof exists as a subgraph of the token-event graph:
The proof just given has the fewest events—or “proof steps”—that can be used. But altogether there are 50 possible proofs, other examples being:
These correspond to the subgraphs:
How much has the accumulative character of these token-event graphs contributed to the structure of these proofs? It’s perfectly possible to find proofs that never use “intermediate lemmas” but always “go back to the original axiom” at every step. In this case examples are
which all in effect require at least one more “sequential event” than our shortest proof using intermediate lemmas.
A slightly more dramatic example occurs for the theorem
where now without intermediate lemmas the shortest proof is
but with intermediate lemmas it becomes:
What we’ve done so far here is to generate a complete token-event graph for a certain number of steps, and then to see if we can find a proof in it for some particular statement. The proof is a subgraph of the “relevant part” of the full token-event graph. Often—in analogy to the simpler case of finding proofs of equivalences between expressions in a multiway graph—we’ll call this subgraph a “proof path”.
But in addition to just “finding a proof” in a fully constructed token-event graph, we can ask whether, given a statement, we can directly construct a proof for it. As discussed in the context of proofs in ordinary multiway graphs, computational irreducibility implies that in general there’s no “shortcut” way to find a proof. In addition, for any statement, there may be no upper bound on the length of proof that will be required (or on the size or number of intermediate “lemmas” that will have to be used). And this, again, is the shadow of undecidability in our systems: that there can be statements whose provability may be arbitrarily difficult to determine.