First-order theory with 0, S, +, ·, induction schema. PA incomplete (Gödel), consistent with ε_0 induction (Gentzen 1936).