[Haskell-cafe] Peano axioms

John D. Ramsdell ramsdell0 at gmail.com
Thu Sep 17 17:21:01 EDT 2009

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.


More information about the Haskell-Cafe mailing list