Arithmetic on formulas

• Use Peano arithmetic to encode formula manipulation:
• Subst(N, M):
• Subst returns a number Z
• N is interpreted as the Godel number of formula Fx with a free variable x
• Substitute M for all instances of ‘x’ in Fx
• Z is the Godel number of the resulting formula