[Haskell-cafe] Peano axioms

[John D. Ramsdell]

I don't understand your goal.  Isn't Peano arithmetic summarized in Haskell as:

data Peano = Zero | Succ Peano deriving Eq

This corresponds to a first-order logic over a signature that has
equality, a constant symbol 0, and a one-place successor function
symbol S.

Function symbols such as < and + can be introduced as defined function
symbols that do not add substantive information to the theory.  The
only axioms you want are the ones for equality.

John