Systems the Peano axioms can be derived in

Question

I know that the Peano axioms can be got from ZF set theory, and lambda calculus. What other systems can they be derived (I'm not sure if that is quite the right word here) in, and which the simplest system?

Answer 1

It seems you're interested in formal system capable of interpreting(encode) arithmetics and prove Peano Axioms. That is formal system in which you can define (via first order formulas) what are a natural numbers and arithmetic operations, and then you can prove PA axioms inside this system.

This can clearly be done in any sufficiently strong system, for instance every set theory rich enough to be a foundational theory: this include set theories like ZFC, but also NBG and TG, but also formal systems like lambda calculus and type theories.

Of course the simpler system in which you can encode Peano Arithmetic is Peano itself.

But if you are looking for a non trivial example you can consider ZF without the axiom of infinity. Such theory you can encode natural numbers as finite ordinals (as done in ZFC) and arithmetic operations as some predicates of this theory. Then every axiom of (first order) Peano Arithmetic can be proved by the axioms of this set theory. This is intuitively the theory of finite set and is the weakest system that can encode (first order) Peano Arithmetic: that's because it can be proved that ZF without the axiom of infinity can be encoded in Peano Arithmetic and so it's equivalent to it.

Answer 2

Let $X$ be any Dedekind-infinite set, i.e. there exists a function $f:X\to X$ such that $f$ is injective, but not surjective. $f$ not being surjective, there exists $x_0\in X$ such that for all $y\in X$, we have $f(y)\neq x_0.$

It can be shown using ordinary logic and set theory that there exists $N\subset X$ on which the Peano axioms are satisfied with $f$ being the successor function and $x_0$ being the "first" number in $N$.

In other words, there exits at least one "copy" of the natural numbers in every Dedekind-infinite set.