Infinite Rules in Finite Systems

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 ∨, &, ⊃, ≡, ~, 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.