Related posts

• Reading Notes on GEB: Gödel, Escher, Bach: an Eternal Golden Braid (Preface)

WJU formal system

Good, we begin discussing formal systems; this will be the first step toward Gödel's incompleteness theorem.

This is a formal system of strings made of the three characters WJU. Initially the system has WJ as an axiom; strings obtained from the axiom by finitely many applications of Rules I through IV are called theorems:

• Rule I: If a string you own ends with J, you may append a U to it.
• Rule II: If you have Wx, then you also own Wxx.
• Rule III: If JJJ appears in a string in your stock, you may replace that JJJ with a U to get a new string.
• Rule IV: If UU appears in one of your strings, you may delete it.

Most people's approach to solving the WU puzzle is: first rather blindly derive some theorems and see what turns up. Soon they begin to notice certain properties of the theorems they generate; human intelligence operates at that point.

I feel this is roughly a medium problem on LeetCode. I tried a bit of old-school programming this time; after debugging a few bugs I finally wrote an enumerator for the WJU formal system, of course using the mechanical, clumsy method the author describes. I used breadth-first search to traverse the proof tree:

from collections import deque
import tqdm
import itertools
import sys

axiom = "WJ"

def generate_strings(axiom):
    q = deque([axiom])

    while True:
        theorem = q.popleft()

        if theorem[-1] == 'J':
            q.append(theorem + "U")
        q.append(theorem + theorem[1:])

        start_k = 0
        while True:
            i = theorem.find("JJJ", start_k)
            if i == -1:
                break
            q.append(theorem[:i] + "U" + theorem[i+3:])
            start_k = i + 1
        
        start_k = 0
        while True:
            i = theorem.find("UU", start_k)
            if i == -1:
                break
            q.append(theorem[:i] + theorem[i+2:])
            start_k = i + 1
        
        yield theorem

gen = generate_strings(axiom)
print(next(itertools.dropwhile(lambda x: x[1] != sys.argv[1], tqdm.tqdm(enumerate(gen)))))

We did fairly well proving WJ, WJU, WJJJJJ, and WJUUUUUU; although because I maintained a queue, memory quickly became a bit strained, at least it completed normally. But when trying to prove WU, the author tricked us — it seems this really can't be proved (I killed the process before the swap ran out).

This story tells us that being a hands-off manager is definitely wrong; as the author says, this is the time to "step outside the system", to reflect on the proof, that is, to find the theorem's "decision procedure".

I think the AI's understanding is more accurate than mine. My initial mistake was to invoke human ability to find a path in that proof tree for a class of theorems. Machines can only enumerate, while humans, by their spirit, can proactively find that path. The original author, however, is more concerned with stepping outside the system (for example using modular arithmetic and other dimensionality-reducing methods), not being fixated on finding that path, which clearly fits the context here better.

Two-Part Invention

After Achilles had overtaken the tortoise, he complacently sat down on its back. "So then, you have already reached the end of our race, have you?" said the tortoise. "Although the course is made up of an infinite number of stretches, you still ran to the end? I remember someone clever once proved that it is impossible to do so."

This story is mainly about syllogism. Setting aside whether we accept the major premise and minor premise, suppose we do not accept the step from premises to conclusion — what would happen?

This may seem absurd, but if we go back to the WJU formal system: syllogism itself is like a rule that operates on strings; it belongs to the system's "inference rules", not something beyond the system. Just as we can decide whether Rules I-IV exist in the WJU system, we can also choose whether to accept syllogism as a rule. In other words, any formal system depends on the axioms and derivation rules we accept in advance; it is not automatically "reasonable".

We adopt it because, under the usual semantic interpretations, it reliably preserves truth from true premises to true conclusions, and thus is suitable to characterize human rational inference.

In the next chapter, I look forward to more exploration and deeper understanding of such formal systems.