Exploring the Peano Axioms Through Algebraic Data Types

Re:Exploring the Peano Axioms Through Algebraic Data Types by intuitionist on Tuesday January 15, 2019 @01:10AM (#18909142)

Strictly speaking, aren’t these the axioms of Robinson arithmetic (a much weaker system)? For Peano arithmetic you need the axiom schema of induction as well.

[ Parent | on HN ]

Re:Exploring the Peano Axioms Through Algebraic Data Types by choeger on Tuesday January 15, 2019 @02:34AM (#18909411)

I think structural induction over S will do just fine.

[ Parent | on HN ]

Re:Exploring the Peano Axioms Through Algebraic Data Types by traderjane on Tuesday January 15, 2019 @02:55AM (#18909464)

I thought that the recursively enumerable structure was given by the Axiom of Induction.

[ Parent | on HN ]