% 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.
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
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 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 - ∎