 System \(\mathsf{P}\) is obtained from that of Whitehead and Russell’s Principia Mathematica (1910–1913)  by omitting the ramification of types, taking the natural numbers as the lowest type, and adding for them the second-order Peano axioms. It is hence a fixed formal system with finitely many non-logical axioms sufficient for the development of elementary number  theory.[7] Recall also that an arithmetical system is said to be \(\omega\)-consistent if it does not prove both \(\exists x \varphi(x)\) and \(\neg \varphi(\overline{n})\) for each natural number \(n \in \mathbb{N}\) (where \(\overline{n} =_{\mathrm{df}} s(s(\ldots s(0)))\) \(n\)-times) and that \(\omega\)-consistency implies simple consistency (i.e., the non-derivability of a formula and its negation).  