coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tacit implications in Goedel's theorems II – Re: True arithmetical proposition not provable

From: Marco Servetto <marco.servetto AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Tacit implications in Goedel's theorems II – Re: True arithmetical proposition not provable
Date: Thu, 24 Jun 2021 21:07:38 +1200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=marco.servetto AT gmail.com; spf=Pass smtp.mailfrom=marco.servetto AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf1-f43.google.com
Ironport-hdrordr: A9a23:R8GekKlvdJ9lGjgcv5ZObw+zk4/pDfIW3DAbv31ZSRFFG/Fw9vre+sjzsCWetN9/Yh4dcLy7WZVoIkm9yXcW2+Us1N6ZNWGN1VdASrsSjrcKqAePJ8SRzJ846Y5QN4R4Fd3sHRxboK/BkW6F+g8bsbu6GXaT9ILj80s=
Ironport-phdr: A9a23:9KM+9hF2Jvj738sqEBk+x51GfzpMhN3EVzX9CrIZgr5DOp6u447ldBSGo6k03RmSAdmQtK8MotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5pnebx9GiTeybr5+Ixe7oAXMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM2/2/Xhc5wgqxVoxyvugJxzJLbboyOKPp+Z7nQcc8GSWZdXMtcUTFKDIOmb4sICuoMJeFWoJPnp1QSqhu1GBSiC/31yj9WmHD2wbE60+M8GgzB2QwvBcgOv2jTrNnvL6cdT/q1zLfWwjXfc/NW3izw6IfNch87oPGMWah8ftbWyUkqDg7IiEibpoP5MT2PzOsNr3Sb4PR6VeKpk2MrtRx8rzqyyssyhYTEm4wbxF/Y+Ch6zog4Kty1RVB0b9O4EJZduCGXOopoTs4mXWxluzg2x7MYtJO/fiUG1YgqyhjCYPKEa4iF+gzvWPqVLDtih39oeKiziwuz/EWi0OHxWce53VBXpSRfiNbMrGoC1xnL58iHVPR9+kCh1C6K1w/J6+FEJVk4la7VK5I827IwmJUevErZEi/5n0X2i6CWdkE69eSy9+vnZbDmqoedN49ylA7+LrwjltKjDek8KAQDXGiW9f6h2LDi/0D1WrpHg/Munqncqp/aJMAbpqCjAw9S14Yu8xO/AC280NsEmnkLNklFdwydj4j3JV7OPOz4DfCkjlSjlTdk3fHGPrn7DprRKXjDla/tfaxh5E5E1Aoz0ddf6opIBbEGOfL/Q1P+tNjFDhAiKAG02ObmCNBl1owEQ26PA6mZMLnTsVCS/O4vLfOMN8cpv2P2LOFg7Przh1c4n0UcdO+nx8g5cne9S9FvOU6eKUHhmMkMDXsN9l47RfbhjxuZXCRNamquWIoz4zg6DMStCoKVFdPlu6CIwCruRs4eXWtBEF3ZSR8Akq2LXv4NbGSZJcozylTsupCuToYg0VelswqoktKPz8LR8ywc8JbtjZ17u7aVmhY1+jh5Sc+a1jPVJ1w=

Just out of curiosity, how does anyone even attempt to prove a statement like
> There’s an explicit 748-state Turing machine that halts iff ZF is
inconsistent.
Is it a formal proof inside of ZF?

Re: [Coq-Club] True arithmetical proposition not provable, (continued)
- Re: [Coq-Club] True arithmetical proposition not provable, Dominik Kirst, 06/20/2021
  - Re: [Coq-Club] True arithmetical proposition not provable, Vincent Semeria, 06/20/2021