# Proof verification in GEB

% Remco Bloemen % 2010-01-03, last updated 2014-03-04

In Hofstadter's book Gödel, Escher, Bach he discusses a few formal systems. In this post I have translated the two simplest of them to my simple proof verification system which, as suggested by Sander’s comment, is extended with a command to define a constant.

## The MIU-System

```
C M
C I
C U
T 'Sole axiom'
⊨ M I
∎
T 'Rule I'
∧ x I
⊨ x I U
∎
T 'Rule II'
∧ M x
⊨ M x x
∎
T 'Rule III'
∧ x I I I y
⊨ x U y
∎
T 'Rule IV'
∧ x U U y
⊨ x y
∎
```

With the system defined, I can now enter the derivation of `MUIIU`

:

```
T 'Derivation of M U I I U'
∵ 'Sole axiom'
∵ 'Rule II'
x ⊧ I
∵ 'Rule II'
x ⊧ I I
∵ 'Rule II'
x ⊧ I I
∵ 'Rule I'
x ⊧ M I I I I
∵ 'Rule III'
x ⊧ M
y ⊧ I U
∵ 'Rule III'
x ⊧ M
y ⊧ I U
∵ 'Rule II'
x ⊧ U I U
∵ 'Rule IV'
x ⊧ M U I
y ⊧ I U
∴ M U I I U
∎
```

## The pq-System

The pq-system is not that formal in the book, it contains expressions such as "whenever x is composed of hyphens only" that are not further specified. Luckily, it is easy to formalise these statements in my proof language:

```
C p
C q
C -
C ComposedOfHyphens
T 'ComposedOfHyphens -'
⊨ ComposedOfHyphens -
∎
T 'ComposedOfHyphens a b'
∧ ComposedOfHyphens a
∧ ComposedOfHyphens b
⊨ ComposedOfHyphens a b
∎
T 'The Axiom'
∧ ComposedOfHyphens x
⊨ x p - q x -
∎
T 'The Rule'
∧ ComposedOfHyphens x
∧ ComposedOfHyphens y
∧ ComposedOfHyphens z
∧ x p y q z
⊨ x p y - z -
∎
```