coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] The violation of type restrictions in a presentation of Goedel's First Incompleteness Theorem

From: Ken Kubota <mail AT kenkubota.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] The violation of type restrictions in a presentation of Goedel's First Incompleteness Theorem
Date: Thu, 7 Jan 2016 12:43:19 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT kenkubota.de; spf=Pass smtp.mailfrom=mail AT kenkubota.de; spf=None smtp.helo=postmaster AT plasma6.jpberlin.de
Ironport-phdr: 9a23:RSr8shCtxBjffN/K+l/+UyQJP3N1i/DPJgcQr6AfoPdwSP74psbcNUDSrc9gkEXOFd2CrakU1ayJ6Ou7ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTpkb/psMaLKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs1gRVC01jxBPHwGNuBTzX5PZsSb8tfd33zWTe8H7G+NnEQ++5rtmHUe7wBwMMCQ0pTna

Dear List Members,

Please allow me to direct your attention to the violation of type
restrictions
in a presentation of Goedel's First Incompleteness Theorem:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-January/msg00029.html

Other theorem provers may be affected as well, such as
- Coq by INRIA et al. (proof claimed by Russell O'Connor), and
- John Harrison's HOL Light (proof claimed by John Harrison).

Kind regards,

Ken Kubota

____________________

Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100

[Coq-Club] The violation of type restrictions in a presentation of Goedel's First Incompleteness Theorem, Ken Kubota, 01/07/2016