The classical and the <i>ω</i>-complete arithmetic

TLDR

The paper studies two second‑order functional calculi for natural numbers that share the same primitives and axioms but differ only in their inference rules. The authors define number formulas and propositional formulas inductively as the minimal classes of expressions built from the primitive symbols, with 0, 1, and number variables as the basic number formulas.

Abstract

We consider two formal systems for the theory of (natural) numbers, both of which are applied second-order functional calculi with equality and the description operator. The two systems have the same primitive symbols, rules of formation, and axioms, differing only in the rules of inference. The primitive logical symbols of the systems are the improper symbols (,), the prepositional connectives ∨, &amp;, ⊃, ≡, ~, the quantifiers ( ), (E), the equality symbol =, the description operator ι,-infinitely many distinct individual (or number) variables, and for each positive integer k infinitely many distinct k -place function variables. Our systems have in addition the following four primitive nonlogical (or arithmetical) constants:0, 1, +, ×. The classes of “number formulas” (nfs) and “propositional formulas” (pfs) are defined inductively as the least classes of formal expressions (i.e. of concatenations of primitive symbols) satisfying the following conditions: (1) 0, 1, and the number variables are nfs.