Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Non standard natural numbers

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Non standard natural numbers


Chronological Thread 
    < Chronological >      < Thread >
  • From: Vincent Semeria <vincent.semeria AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Non standard natural numbers
  • Date: Wed, 2 Jun 2021 21:53:28 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vincent.semeria AT gmail.com; spf=Pass smtp.mailfrom=vincent.semeria AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f51.google.com
  • Ironport-hdrordr: A9a23:J5XgTKtxRznL7YQ4JdQWAPLf7skDe9V00zEX/kB9WHVpm62j5qeTdZEgvyMc5wxhO03I9erhBEDiexLhHPxOkOss1N6ZNWGMhILCFvAG0WKN+UyFJ8Q8zIJgPGVbHpSWxOeeMbGyt6jH3DU=
  • Ironport-phdr: A9a23:A+5yExKUVi4C9vhvWNmcuHtmWUAX0o4c3iYr45Yqw4hDbr6kt8y7ehCGtLM33QCCAtiTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yuS/94fNbwhMhjexbrF/IRWrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIOD43/m/UhMJtkqxUvAmsqAZjz4POeoyZKOZyc6HbcNgHRWRBRMFRVylZD4yzbosPCfYOMvher4nhulAAsAWxBQyyC+P1yz9HnGL90Kok0+QgFwHJwBIvH9QSsHjOt9X6KqISXv6vzKnJ1zrOdPxW2TLn54jJdhAtu+2DXbV1ccfIz0QkCgzKgEmKp4P/IzOVyvoCs3Kd7+d4SO+ihHMqpgJ1rzWuwsohiYbEi58Jx13F6yl03Yk4K9O6RUJnbtOpH5hduiKVOoV5Xs4vQn1ktDonxrAIvZO3Yi4Hw4kkyR7Hc/GLbZSE7xb5WOuSITp0nmxpdK+jixqo8UWs1+vxXdSu3llQtCpKiNzMu2gN1xPN7siHTeNw/kK71jaO0wDf8+ZEIVwpmabCJZ4swqM8moAcsUTEGS/2l0H2g7GMeko4/eio7vzrYrTgppCCK495kh/yPrgql8ClAuk1MhICU3aG9eigzrHu/VD1TK1PjvIsk6nZtJ7aJd4cpq68GwJVzIcj6xCjADi41tQYgWMLLElbdxKCkYfpIVDOL+rjAPewhlSjijZrx/TcMrL9BZXNK2DPkK39crZl905c1A0zwMhD6JJTE7ENOe78WkvstNPDFRI5KAy1w+P/CNpnzI8eWGSPArWYMKzIq1OI6PgvcKGwY9oevy+4IPw47dbvi2U4kBkTZ/qHx5wSPU65GP9rJVnRWnfpj80AGC9eoAs4R+HslBuZXDtefXe7d6057zA/TomhCNGQFciWnLWd0XLjTdVtbWdcBwXUeZ8NX4qBUvYILimVJ505+tTrfbekQo4lkxqpsV2jo1KGBu/d+yldso66kdYovqvckhY98TEyBMOYgTnlcg==
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.

Archive powered by MHonArc 2.6.19+.

Top of Page