Here are some links to Logiweb pages:
prop My first attempt at implementing an axiomatic system (for the propositional calculus). It looks a mess, but all the formal stuff on the page is correct.
peano commutativity This is a page proving the commutativity of addition of natural numbers (that is, we have x+y = y+x for all non-negative integers x and y).
Frederik Eriksen, June 29th 2005.