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 )