Injectivity of successor of natural numbers in Coq

Question

I am a little confused whether the injectivity of the successor function defined on natural numbers in Coq is an axiom? According to Wikipedia/Peano axioms, it is an axiom (7). When I look at Coq.Init.Peano manual page I see the following:

Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H.

Hint Immediate eq_add_S: core.

and it looks like an axiom (?) but what confused me was that in the top of that page it said:

It states various lemmas and theorems about natural numbers, including Peano's axioms of arithmetic (in Coq, these are provable)

This sentence is a bit ambiguous no?

Answer 1

The command you saw is actually a proof of the injectivity of the S constructor. More precisely, it says that the successor function is injective because it has an inverse: the predecessor function (pred). (In Coq, axioms are generally introduced with the keyword Axiom.)

You seem to be confused by what I think are two related senses of the word "axiom." The broader sense in logic is that of a "starting point of reasoning" (Wikipedia). The narrower sense is that of an assertion that is taken for granted in a deductive system without further proof. In Peano arithmetic, Peano's axioms are axioms in both senses of the word, since they primitive. In Coq, ZFC set theory, and other systems, they can be proved from more elementary facts.