# 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 -
∎


Remco Bloemen
Math & Engineering
https://2π.com