Peano arithmetic

Peano arithmetic

A system for representing natural numbers inductively using only two symbols, "0" (zero) and "S" (successor).

This could be expressed as a recursive data type with the following Haskell definition:

data Peano = Zero | Succ Peano

The number three, usually written "SSS0", would be Succ (Succ (Succ Zero)). Addition of Peano numbers can be expressed as a simple syntactic transformation:

plus Zero n = n plus (Succ m) n = Succ (plus m n)
References in periodicals archive ?
The book Frege's Theorem focuses, obviously, on Frege's Theorem: that second-order logic supplemented with a cardinality principle also called "Hume's Principle" (HP) allows to derive the axioms of Peano Arithmetic.
Those lecture series have been boiled down to four refereed essays on countable models and the theory of Boral equivalence relations, model theory of difference fields, some computability-theoretic aspects of reals and randomness, and weak fragments of Peano arithmetic.
We add Priest's dialetheic semantics to ordinary Peano arithmetic PA, to produce a recursively axiomatized formal system P[A.