Peano Arithmetic

We aim to axiomatize the set of naturals
The language consists of and
with arities of being respectively

Peano Arithmetic consists of the following sentences:







for every formula with

Note that by The Upwards Löwenheim-Skolem Theorem there is an uncountable model of PA.
This is because the induction is not strong enough.
The ‘true’ induction is

But we cannot quantify over subsets of a structure.
Since the language of PA is countable,
the induction axiom-scheme only captures countably many subsets of

Definition

A subset is definable in PA if there’s a formula in PA
with one free variable such that

Gödel’s Incompleteness Theorems imply that PA is not a complete theory.
So there is a formula that holds in but (or )