Peano arithmetic in Coq

5
votes

Coq's standard library says that this inductive type gives the Peano natural numbers :

  Inductive nat :=
  | O : nat
  | S : nat -> nat.

It sounds right, because we can prove in Coq all Peano's axioms on nat, including the induction principle, which is given by Coq as nat_ind.

But this repo claims it has a proof in Coq of Goodstein's theorem. And we know that this theorem is not provable with Peano's axioms only. So it seems that Coq's nat is stronger than Peano's axioms, it would rather be a model of them, in which Goodstein's theorem is true. Is this correct ?

Can Coq prove the same arithmetical theorems on nat as the ZFC set-theory does on standard natural numbers ? Same question if we add the classical logic in Coq :

Axiom excluded_middle : forall P : Prop, P \/ ~P.

The underlying question behind this is the truth of Coq proofs. What guarantee do they give ? I am a developer so I am particularly interested in the proofs of programs, hence the specific question on arithmetic.

1
coq
I think when most people say "Peano naturals" they're talking about the particular presentation of the natural numbers as being generated from zero and successor, as opposed to say, binary naturals, which would be the presentation of them as finite binary strings. It doesn't really have anything to do with any particular theory which one would call "Peano arithmetic". – tlon

1 Answers

2
votes

You are right. Any result that can be proved in Peano arithmetic can also be proved in Coq (at least, if we allow ourselves to use the excluded middle); however, there are sentences of Peano arithmetic that cannot be proved in that system but can be proved in Coq.

Benjamin Werner showed that Coq and ZFC are pretty much equivalent in terms of expressive power: you can interpret Coq in ZFC if you assume sufficiently large cardinals, and you can interpret ZFC in Coq by assuming a few non-constructive axioms. (Of course, the status of a computer-checked Coq proof is more complicated, given that the theory implemented in Coq is slightly different from the one considered in that paper, and that there could be bugs in the Coq implementation or in the computer running it.)