 where n is the formal term which denotes the natural number n. (In P, this is S(S(…S(0)…), where n is the number of iterations of the successor function applied to the constant symbol 0.) One of the principal goals is to numeralwise express the predicate