# Goedel, Escher, Bach

(under construction in 2021 ... a blog on teaching an advanced high-school or first year college course on GEB ... not everything we do in the course is reflected in the notes)

I found an online version of the book [here](https://www.physixfan.com/wp-content/files/GEBen.pdf). But it contains typos.

## Introduction

I assume that you have read (or are going to read soon) the Introduction of GEB. I collect some background information that may be helpful.

### (1) The Danger of Contradictions

To understand why paradoxes (self-contradictory sentences) pose a potentially serious problem for logic, mathematics and science, we need to first understand that once one arrived at one contradiction, then anything becomes provable.

We first reviewed some aspects of logical reasoning.

- We are interested in reasoning about propositions that can be true or false. Numbers such as $0,1,2,\ldots$ are not propositions but the equation $0=1$ is a proposition (a false one).
- Propositions can be combined with operations such as *not*, *and*, *or*, *implies*. For example, if $A$ and $B$ are propisitions then so are
- $\neg A$ (*not* $A$),
- $A\wedge B$ ($A$ *and* $B$),
- $A\vee B$ ($A$ *or* $B$),
- $A\to B$ ($A$ *implies* $B$, if $A$ then $B$).
- The rules of reasoning only depend on the form, not on the content of the proposition. We wrote down examples of rules such as ...
- We reflected on why the rules for "and" and "or" are not symmetric. The reason is that both rules are formulated in a "meta-logic" that has "and" (but not "or"). [The relationship between "object-language" and "meta-language" will play a major role in GEB.]

This can be shown in many ways. I reproduce the argument from [Wikipedia](https://en.wikipedia.org/wiki/Principle_of_explosion), in symbolic notation.

$$\frac{\frac{\frac{}{\vdash A}}{\vdash A\wedge B} \quad
\frac{}{\vdash\neg A}}{\vdash B}$$

### (2) Excursion to Logic 1

Since we have seen some logic in the last session, I thought it might be worthwhile digressing a bit into logic.

We talked about the many ways one might want to formalise logic.

**Boolean Algebra:** The starting point is the analogy between equations known from algebra such as the first below and laws of logic such as the second one.
\begin{align}
a\cdot (b+c) & =a\cdot b + a\cdot c\\
A\wedge (B \vee C) & = (A\wedge B)\vee(A\wedge C)
\end{align}

These two laws have the same form, even if $a,b,c$ range over numbers and $A,B,C$ range over propositions. (The capitalization (or not) of the letters is traditional and has no signficance.)

One arrives at **Boolean algebra** by collecting all laws of logic satisfied by operations $\neg,\wedge,\vee$.

**Ordered Algebra:** Instead of with equations, we can also work with inequations. Recall that operations such as $+$ and $\cdot$ have inverses (subtraction and division). Unfortunately, $\wedge$ and $\vee$ do not have inverses, due to the fact that
\begin{align}
A\wedge A & = A \\
A\vee A & = A \\
\end{align}

But this can be repaired (partially) if we replace equations by inequations. For example, we talked about
$$S\wedge H \le P \quad \ \Longleftrightarrow \ \quad S\le \neg H \vee P$$

Here we see that $\neg H \vee (-)$ allows us to "bring the $H$ on the other side", an operation that has similar properties to subtraction and division.

**Truthtables:** Yet another way to explain logic is via truth tables. We discussed the truth table of implication. Example: "All squares are rectangles" can be written as $A\to B$ with $A$ for *square* and $B$ for *rectangle*. It also helps to have an example of an implication that is false such as "all squares are triangles".

The truth table for implication is difficult to understand, we spent most of the time on this.

**Other formalism:** There are many other ways to explain logic: Venn Diagrams, semantic tableaux, natural deduction, sequent calculi, deep inference, display calculi, syllogistic logics, categorical logic, etc. They are all equivalent in some sense and different in another.

### (3) Excursion to Logic 2

We discussed how to derive Gentzen's rules of Natural Deduction for $\wedge$, $\vee$, $\to$ from examples.

You can see that [Gentzen's original rules](https://github.com/alexhkurz/programming-languages/blob/main/resources/Gentzen-natural-deduction-rules.png) are the same, just that his notation is slightly different ($\&$ for $\wedge$ and $\supset$ for $\to$). A good modern account, but more advanced than what we covered can be found in [this article](https://leanprover.github.io/logic_and_proof/natural_deduction_for_propositional_logic.html) which is part of a series on the LEAN theorem prover (a software package for implementing and verifying mathematical proofs).

### (4) Excursion to Logic 3

We studied some example proofs in natural deduction to get a feel for what it means to write out mathematical proofs by using the rules of a logical calculus.

We discussed how to prove that, as in algebra, logic supports a rule for factoring and expansion known as the distributive law: $A\wedge (B\vee C)$ is logically equivalent to $(A\wedge B)\vee(A\wedge C)$.

*Homework:* Prove, using the rules of [natural deduction](https://github.com/alexhkurz/programming-languages/blob/main/resources/Gentzen-natural-deduction-rules.png), that $A\vee (B\wedge C)$ is logically equivalent to $(A\vee B)\wedge(A\vee C)$. [^Hint]

### (5) Paradoxes

To recap, we have seen that one contradiction can bring all of mathematics to fall in the sense that from one contradiction everything can be proved.

We followed this up with a brief look at the logical calculus of natural deduction, to get a feel of what it means to conduct formal proofs in such a calculus.

In this session we looked at the actual paradox (contradiction) that the mathematicians and logicians in the early 1900s felt threatened by.

Russell's Paradox: [SEP](https://plato.stanford.edu/entries/russell-paradox), ...

We defined *the set of all sets that do not contain themselves* in set theoretic notation as $y=\{x\mid x\notin x\}$ in order to see more clearly that it follows from this definition that $y\notin y \ \Leftrightarrow y\in y$, a contradiction.

To understand why this paradox was so influential one needs to put it into the context of mathematics of around 1900. Other version of it, such as the Liar's Paradox ([Wikipedia](https://en.wikipedia.org/wiki/Liar_paradox), [SEP](https://plato.stanford.edu/entries/liar-paradox/)) have been known since antiquity.

We also discussed a version that is known as the barbers paradox.

We ended up spending most of the time on the [Berry Paradox](https://en.wikipedia.org/wiki/Berry_paradox). This allowed us to discuss how the meaning of language depends on the context and whether this is crucial for this paradox to work.

## Chapter I

We already studied a little bit a quite complex formal system, namely natural deduction. Chapter I looks at a much simpler style of formal systems, known as Post systems (after [Emil Post](https://en.wikipedia.org/wiki/Emil_Leon_Post) who also has other discoveries to his name) or [string rewriting systems](https://en.wikipedia.org/wiki/Semi-Thue_system).

### (6) The MU Puzzle

We started writing out the 4 rules from Chapter 1 in the following two forms.

\begin{align}
x\bf I & \to x\bf IU \\
\mathbf Mx & \to \mathbf Mxx\\
x{\bf III}y & \to x\mathbf Uy\\
x{\bf UU}y & \to xy
\end{align}

Here, $\bf M, I, U$ are the letters from which we form the word (aka strings, or sequences of symbols). $x,y$ are variables ranging over 'words'. Thus, the rules tell us how to rewrite words.

There is an alternative format used commonly to formalize such rewrite rules. In this second format, a rule can be applied to any *substring* that matches the left-hand side. To make sure that, for example, the first rule only allows to add a $\bf U$ at the end of a word, we introduce a special end-of-word symbol $\#$. (This can be really any symbol as long as it is differnt from $\bf M, I, U$.)

\begin{align}
\mathbf I\# & \to {\bf IU}\# \\
\mathbf Mx\# & \to \mathbf Mxx\#\\
{\bf III} & \to \mathbf U\\
{\bf UU} & \to
\end{align}

**Discussion:** Why do these two sets of rules specify the same rewrite systems?

**Exercise:** Prove that one cannot derive $\bf U$ from $\bf MI$.

**Question:** Can one derive $\bf MU$ starting from $\bf MI$?

**Discussion:** How can one prove that a certain word is *not* derivable?

**Homework:** Finish the proof that $\bf MU$ is not derivable from $\bf MI$ (using a clock of 3 to count the numbers of $\bf I$) discussed during this session.

[^Hint]: Here are the proofs, we have done previously. The homework is similar.


## Chapter 2 (Formal Systems)

### (7) An invariant of the pq-system

We wrote out the $\sf pq$-system as follows.

\begin{align}
& x{\sf p \hyphen q}x{\sf\hyphen} & \rm Axiom\\
& x{\sf p} y\mathsf q z \ \rightarrow \ x{\sf p} y{\sf \hyphen q} z\hyphen & \rm Rule\\
\end{align}

We discovered and proved and invariant of the pq-system.

### (8) Infinitely many primes

After reviewing the last session and talking more about decision procedures, we proved Euclid's theorem on the existence of infinitely many prime numbers.

## Chapter 3 (Figure and Ground)

(Prime numbers as a formal system, figure and ground)

What can be captured by formal systems? What about prime numbers? Can we make a tq-system for multiplication?

### (9) "Less than" as a formal system

We talked about how to design a formal system that recognizes prime numbers. But before we can get there we need quite some infrastructure. For example, we may need a procedure to decide whether one number is smaller than another.

We started with $<$. How can we design axioms and rules such that $x\mathsf Ly$ is a theorem if and only if the string $x$ is shorter than the string $y$?

Hofstadter in Chapter 2 allows infinite sets of axioms as long as there is a decision procedure to check whether a given string is an axiom. This gives us quite some freedom in designing formal systems.

**Activity:** Find rules for the different formal system starting from the following different sets of axioms. Below variables $x,y$ range of strings of hyphens `-`.

|Name| Axioms | Rules |
|:---:|:---:|:---:|
|FS1|$x\mathsf Lx\hyphen$ ||
|FS2|$\hyphen\mathsf L\hyphen\hyphen x$||
|FS3|$x\mathsf Lx\hyphen y$||
|FS4|$\hyphen\mathsf L\hyphen\hyphen$||

The difficulty with FS1-3 is that there are infinitely many axioms, one for each instantiation of the variables. This is not a problem as long as we can use typographical operations[^typographical] to decide whether any given string is an axiom, but the burden is on us and requires an argument outside of the formal system. I therefore prefer FS4, which has more rules, but only one axiom.

### (10) Two-Part Invention

(In the book this comes before Chapter 2.)

We wrote down the rule (A) with variables $x,y,z$ as
$$\frac{x=y\quad\quad y=z}{x=z}.$$

(B) can be written as
$$a=c\quad\quad c=b$$

where $a,b,c$ are constants (denoting specific sides in some triangle).

Now applying rule (A) to data (B), we conclude (Z)
$$ a=b.$$

So what is the problem that Turtoise does (pretend to) have? Why is Turtoise able to trick Achilles into a seemingly infinite sequence of deductions?

I have a tentative answer, but I'd like to hear your take on this ...

### (11) Proving the correctness of the pq-system

Going back to the pq-system, we have seen that the pq-system captures/describes addition of numbers. Can we turn this into a mathematical statement that can be proven mathematically?

One way of doing this is to define two sets, one using addition and the other using the formal system and then proving the two sets to be equal.

The first set, which I call
$$\sf Plus$$ is the set of all strings $x\mathsf py\mathsf qz$ such that $|x|+|y|=|z|$, where the length of a given string $s$ is denoted by $|s|$. [^Plus]

The second, which I call
$$\sf Thms$$ is the set of all strings $x\mathsf py\mathsf qz$ that have a derivation in the pq-system. [^Thms]

Now, if we wnt to show mathematically that the pq-system describes addition, we can prove that
$$\sf Plus = Thms.$$

In general, to show the equality of two sets, we show that one is a subset of the other, and vice versa. Here that means that we need to show
$$\sf Plus \subseteq Thms$$

and
$$\sf Thms \subseteq Plus.$$

Let us sketch the two arguments.

$\sf Plus \subseteq Thms$: To prove $\sf Plus \subseteq Thms$, we need to show that all $x\mathsf py\mathsf qz$ with $|x|+|y|=|z|$ have a derivation. We assume here that we do addition of positive numbers. If $y$ is $\sf\hyphen$ then the derivation consists just of an axiom and needs no rule. If the $y$ has two or more hyphens, we apply the rule
$$x\mathsf p y\mathsf q z \ \longrightarrow \ x\mathsf p y\hyphen\mathsf q z\hyphen$$

$(y-1)$-times and construct the following derivation (rhs abbreviates right-hand-side).
\begin{align}
& x{\sf p\hyphen q\hyphen} x & \rm Axiom\\
& x{\sf p\hyphen\hyphen q\hyphen\hyphen}x & \textrm{rhs of the rule where $y$ is $\hyphen$}\\
& x{\sf p\hyphen\hyphen\hyphen q\hyphen\hyphen\hyphen}x & \textrm{rhs of the rule where $y$ is $\hyphen\hyphen$}\\
& ... & ... \\
& x\mathsf py \mathsf qz & z=yx\\
\end{align}

After applying the rule $(y-1)$-times, the string following the $\sf q$ has $|x|+|y|$ hyphens, thus, by assumption, $|z|$ hyphens, as required. [^boundvariable]

[^boundvariable]: There is a subtlety hidden in the proof. When we begin the proof, $x,y,z$ are given strings with an arbitrary but fixed number of hyphens, only subject to the constraint that $|x|+|y|=|z|$. At the same time, the symbols $x,y,z$ also appear as variables in the rule. Note that the meaning of the $y$ changes each time we apply the rule. We say that the $y$ (and the $x$ and the $z$)

$\sf Thms \subseteq Plus$: To prove $\sf Thms \subseteq Plus$, we need to show that whenever there is a derivation of $x\mathsf py\mathsf qz$ then we have $|x|+|y|=|z|$. For this it suffices to show that
- $|x|+|y|=|z|$ holds for all axioms and
- $|x|+|y|=|z|$ holds after the application of a rule, whenever it holds before.

In other words, we show that $|x|+|y|=|z|$ is an **invariant** of the pq-system. The proof technique which establishes an invariant by checking that the invariant holds for axioms (base case) and by verifying that the invariant is preserved by rules (inductive/recursive case) is also known as **induction** or **recursion**.

**Exercise:** The law of addition that is needed to prove the inductive case is known by which name?

### (11b) Isomorphisms

Hofstadter argues that the meaning of the pq-system arises from an isomorphism between strings and numbers. (Hofstadter does not seem to require that isomorphisms have inverses.) This isomorphism is also useful to explain the proofs in the previous section.

The difficulty with the proofs in the previous section is that once one sees that the pq-system captures addition, this becomes so obvious that it is not clear anymore why it needs proof, or, at what level of detail such a proof should be conducted. So let us look at the proof through the lense of the isomorphism.

Proofs about a formal system are usually done outside of the formal system. In our case, the length-function provides a bridge between the pq-system and numbers. In detail, the length-function maps a string $s$ to the number $|s|$ of symbols in $s$. We can consider the length-function as the mathematical substrate of Hofstadter's isomorphism.

We can now say more clearly what properties we are allowed to use in the correctness proof. We are allowed to use
- the rules of logic,
- properties of strings,
- properties of the length function,
- properties of the numbers.

In particular, if the proof is carried through in all detail, one will need
- $|xy| = |x| + |y|$ and $|\hyphen|=1$
- $x+(y+z) = (x+y)+z$

(There may be a few more, let me know if you find them ...)

Note how the properties $|xy| = |x| + |y|$ and $|\hyphen|=1$ correspond to the fact that the length-function does not only map strings to numbers, but does so in a **structure preserving** way.

**Discussion:** What structure is preserved by the length function?

### (12) A formal system for multiplication

We talked about how to design the rules of a formal system that captures multiplication. See the footnote for a solution. [^tq]

### (13) Correctness of the formal system of multiplication

Homework: Can you transfer the correctness proof of the $\sf pq$-system in (11) to a correctness proof of the $\sf tq$-system in (12).

### (14) A formal system for non prime

### (15) A formal system for prime

## Chapter 4

### (16) Correctness and Completeness

Correctness (external consistency) and completeness are relative wrt an interpretation (aka a model).

In (11), we expressed correctness (everything derivable conforms to the laws of arithmetic) as
$$\sf Thms \subseteq Plus$$

and completeness (all sums $k+m=n$ interpret some derivable string) as
$$\sf Plus \subseteq Thms.$$

**Discussion:** Explain the importance of non-Euclidean geometry.

**Discussion:** Can we define internal consistency?

### (17) Is Mathematics the Same in Every Conceivable World?

Escher's paintings, eg Fig 22 and 23 in GEB, illustrate several ideas. The formal system is the two dimensional figure. Only an interpretation turns it into a 3 dimensional world. There are different possible interpretations that can contradict each other.

Mathematicians used to believe that Euclidean geometry is the only geometry, that geometry is the same in every conceivable world. That turned out to be wrong. What about other parts of mathematics. Such as number theory. Even after the other geometries were discovered, there was still a core that all geometries had in common. Could logic be such a common core for all of mathematics?

## Chapter 5 (Recursion)

Little Harmonic Labyrinth:
- Metawishes and Typeless Wishes.
- GOD = GOD Over Djinn
- I wish my wish would not be granted!

### (18) Push, Pop, and Towers of Hanoi

I moved this [here](https://hackmd.io/@alexhkurz/rJQwvpyMY).

[^typographical]: Typographical operations are defined at the beginning of Chapter 3 as follows.

[^Plus]: In a maths book you might find this defined as ${\sf Plus} = \{x\mathsf py\mathsf qz \mid x,y,z\in\{\hyphen\}^\ast \ {\rm and } \ |x|+|y|=|z|\}$ where the of strings over a set $A$ of symbols is denoted by $A^\ast$.

[^Thms]: In a maths book you might find this defined as ${\sf Thms} = \{s \mid {\sf pq}\vdash s\}$ where ${\sf pq}\vdash s$ is an abbreviation for "the string $s$ has a derivation in the $\sf pq$-system".

[^tq]: One possible solution is
\begin{align}
& x{\sf t \hyphen q} x & \rm Axiom\\
& x{\sf t} y\mathsf q z \ \longrightarrow \ x{\sf t} y{\sf \hyphen q} zx & \rm Rule\\
\end{align}