whats 2 + 2?

?

To prove that 2+2=4 we'll need a specification consisting of:

A constant, 0
A unary function, succ

With these two we can represent all positive integers


A binary function, +
Two variables, x, y

Define the semantics of + as:

1) 0 + x = x
2) succ(x) + y = succ(x + y)


Let 2 be an alias for succ(succ(0))
Let 4 be an alias for succ(succ(succ(succ(0))))


succ(succ(0)) + succ(succ(0)) =? succ(succ(succ(succ(0))))

rewrite using rule 2

succ(succ(0) + succ(succ(0))) =? succ(succ(succ(succ(0))))

rewrite using rule 2

succ(succ(0 + succ(succ(0)))) =? succ(succ(succ(succ(0))))

rewrite using rule 1

succ(succ(succ(succ(0)))) =? succ(succ(succ(succ(0))))

we've reached normal form, and the two sides match. zomg hacks!