section_path: History/Formal construction
section_name: Formal construction
paragraph_text: Formal construction
  
  In 19th century Europe, there was mathematical and philosophical discussion about the exact nature of the natural numbers. Henri Poincaré stated that axioms can only be demonstrated in their finite application, and concluded that it is "the power of the mind" which allows conceiving of the indefinite repetition of the same act. Leopold Kronecker summarized his belief as "God made the integers, all else is the work of man".
  
  The constructivists saw a need to improve upon the logical rigor in the foundations of mathematics. In the 1860s, Hermann Grassmann suggested a recursive definition for natural numbers, thus stating they were not really natural—but a consequence of definitions. Later, two classes of such formal definitions were constructed; later still, they were shown to be equivalent in most practical applications.
  
  Set-theoretical definitions of natural numbers were initiated by Frege. He initially defined a natural number as the class of all sets that are in one-to-one correspondence with a particular set. However, this definition turned out to lead to paradoxes, including Russell's paradox. To avoid such paradoxes, the formalism was modified so that a natural number is defined as a particular set, and any set that can be put into one-to-one correspondence with that set is said to have that number of elements.
  
  In 1881, Charles Sanders Peirce provided the first axiomatization of natural-number arithmetic within this second class of definitions. In 1888, Richard Dedekind proposed another axiomatization of natural-number arithmetic, and in 1889, Peano published a simplified version of Dedekind's axioms in his book The principles of arithmetic presented by a new method (Latin: Arithmetices principia, nova methodo exposita). This approach is now called Peano arithmetic. It is based on an axiomatization of the properties of ordinal numbers: each natural number has a successor and every non-zero natural number has a unique predecessor. Peano arithmetic is equiconsistent with several weak systems of set theory. One such system is ZFC with the axiom of infinity replaced by its negation. Theorems that can be proved in ZFC but cannot be proved using the Peano Axioms include Goodstein's theorem.