= x ∀x∀y x + Sy = S(x + y) ∀x x × 0 = 0 ∀x∀y x × Sy = (x × y) + x. IΣn is first order Peano arithmetic with induction restricted to Σn formulas (for n = 0, 1, 2, ...). The theory IΣ0 is often denoted by IΔ0. This is a series of more and more powerful fragments of Peano arithmetic. The case n = 1 has about the same strength as primitive recursive arithmetic (PRA). Exponential function arithmetic (EFA) is IΣ0 with an axiom stating that xy exists for all x and y (with the usual properties). First order Peano arithmetic, PA. The "standard" theory of arithmetic. The axioms are the axioms of Robinson arithmetic above, together with the axiom scheme of induction: for any formula φ in the language of PA. φ may contain free variables other than x. Kurt Gödel's 1931 paper proved that PA is incomplete, and has no consistent recursively enumerable completions. Complete arithmetic (also known as true arithmetic) is the theory of the standard model of arithmetic, the natural numbers N. It is complete but does not have a recursively enumerable set of axioms. For the real numbers, the situation is slightly different: The case that includes just addition and multiplication cannot encode the integers, and hence Gödel's incompleteness theorem does not apply. Complications arise when adding further function symbols (e.g., exponentiation). Second order arithmetic Second-order arithmetic can refer to a first order theory (in spite of the name) with two types of variables, thought of as varying over integers and subsets of the integers. (There is also a theory of arithmetic in second order logic that is called second order arithmetic. It has only one model, unlike the corresponding theory in first order logic, which is incomplete.) The signature will typically be the signature 0, S, +, × of arithmetic, together with a membership relation ∈ between integers and subsets (though there are numerous minor variations). The axioms are those of Robinson arithmetic, together with axiom schemes of induction and comprehension. There are many different subtheories of second order arithmetic that differ in which formulas are allowed in the induction and comprehension schemes. In order of increasing strength, five of the most common systems are , Recursive Comprehension , Weak König's lemma , Arithmetical comprehension , Arithmetical Transfinite Recursion , comprehension These are defined in detail in the