The Coq mailing list

[Slavomir Kaslev <slavomir.kaslev AT gmail.com>]

It's possible to give a constructive description a such a term c of type non-increasing binary sequences and then prove c_gt0 and c_non_standard (sorry of using Lean on the list):

def ℕ' := Σ' a : ℕ → fin 2, Π n : ℕ, a (n + 1) ≤ a n

def lt (a b : ℕ') : Prop := ∃ n : ℕ, a.1 n < b.1 n
instance : has_lt ℕ' := ⟨lt⟩

def zero : ℕ' := ⟨λ n, 0, λ n, by rw fin.le_def⟩
instance : has_zero ℕ' := ⟨zero⟩

def adjoin {A} (x₀ : A) (f : ℕ → A) : ℕ → A
| 0 := x₀
| (n+1) := f n

def fin2_le_1 (x : fin 2) : x ≤ 1 := nat.le_of_lt_succ x.2

def succ (a : ℕ') : ℕ' := ⟨adjoin 1 a.1, λ n, begin
induction n,
{ apply fin2_le_1 },
{ apply a.2 }
end⟩

def c : ℕ' := ⟨λ n, 1, λ n, by rw fin.le_def⟩

def c_gt0 : 0 < c := Exists.intro 0 nat.zero_lt_one

def c_non_standard (a : ℕ') (h : a < c) : succ a < c :=
begin
induction h with n h,
existsi n + 1,
exact h
end

(live in browser version)

On Wed, Jun 2, 2021 at 10:54 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.



--
Slavomir Kaslev