That is, if the theory asserts (i.e. proves) "P"("n") separately for each natural number "n" given by its specified name, then it also asserts "P" collectively for all natural numbers at once via the evident finite universally quantified counterpart of the infinitely many antecedents of the rule. For a theory of arithmetic, meaning one with intended domain the natural numbers such as Peano arithmetic, the predicate "N" is redundant and may be omitted from the language, with the consequent of the rule for each "P" simplifying to formula_7.