Re: [Haskell-cafe] Peano axioms

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