The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

Here is a proof that your three axioms are inconsistent:

Require Import Arith.
Import Nat.

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

Lemma nope : False.
assert (A := c_gt0).
assert (B := c_non_standard).
destruct c as [|c'].
- now apply lt_irrefl in A.
- specialize (B c' (lt_succ_diag_r c')).
  now apply lt_irrefl in B.
Qed.


On Wed, 2021-06-02 at 21:53 +0200, Vincent Semeria 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.