The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

These terms are indeed consistent (if Coq is 1-consistent), though I'm not sure how to add such an axiom schema without some ocaml hacking.

BTW, your proof is (slightly) incorrect, at least without normalizing the proof first, there may be terms which do not actually occur in the proof, but do appear in the normal form.

Best,

Cody

On Wed, Jun 2, 2021 at 3:53 PM Vincent Semeria <vincent.semeria AT gmail.com> wrote:

Dear Coq club,

Is it possible to axiomatize a term c : nat, such as c is greater than all standard natural numbers ? The first 2 lines are easy,

Axiom c : nat.
Axiom c_gt0 : 0 < c.

But then, could we consistently add this axiom ?

Axiom c_non_standard : forall n:nat, n < c -> S n < c.

If the last axiom is not consistent, we could modify Coq's type checker to interpret all names of the form c_gtSSSS...S0 as closed terms of the corresponding types SSSS...S0 < c. I am pretty sure that these terms are consistent, because if they introduced a proof of False, that proof would be a finite lambda-term with only a finite number of these c_gt terms. Then c could be replaced by the greatest of these terms, and we would obtain a proof of False in basic Coq.