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
Chronological Thread
- From: Ralf Jung <jung AT mpi-sws.org>
- 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 11:30:07 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
- Ironport-hdrordr: A9a23:3xRbWqOuya62u8BcThijsMiBIKoaSvp037BL7TENdfUxSKelfq+V/cjzqiWE7gr5NEtNpTnCAtj4fZqkz+8P3WBJB8bZYOCEghrVEGgB1+vfKlTbckWVygc678hdmsNFZeEYY2IVsS6GiDPIa+rIFOP3kpxB+Y/lvhBQpHlRGsJdBvBCe2Km++RNNWx7OaY=
- Ironport-phdr: A9a23:K6MwBxNVIeXtEBajukkl6nbsDRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDvKQr1wOVFtqGo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/229pHJbQhFizWwbbxwIRi2sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOSMn/mHZisJ+j6xVrxyuqBN934Hab5qYNOZ9c67HYd8WWWRMU8RXWidcAo28dYwPD+8ZMOhEtYb9o1UOpga6CwmxAuPvxSJDi3j03a0n1eQhHhrL3Ak4H9IPqXjUt9v0NLwIXeCy1qnIwizOYvVL0jjy9IbGaAouoe2QXb1ua8rRz1EiGQzLgFiQtYDoPC6Y2+QNvmWY8udtVf+jhmEjpgxxvDWixdsghpTNi44L1F3K9Tt1zYgoKdC2TEN1YdCpHIdfuiycKoB4TMQiQ2RytyY7zL0LoZu7fDALyJg+3B7eZeeHf5KP4hL5W+acJypzinF9eL+nmhq//0ytxvfhWsSwylpHrStInsPRun0NzxDe6MqKRuFg8kqixzqDzR7f5+9ALEwulafWL5gsyaMqmJUJq0TMBCr2lV32jKCIckUk/fCl6+b6YrX+p5+cK5F7ihvkPqQrgsy/AP00MgsKX2iA4uuwzrjj/VX2QLlQk/I5jLHVsJHcJcsFuq60GxJZ34gn5hqlEjur1M4UkHoGIV5fZR6Kj5DlO1TUL/D5Cfe/jU6skDBux/3ePL3hH5PNLnfYnbfkZbZ96ldQyBE9zNBE/Z5UDasBIP3rVk/rqNPYFgM5MxCzw+v/FNp90ZoeVXuTDa+dLaPdqkSF5vkvIumJfI8aoizxK/kj5/70jH82g0URfaez3chfVHftFfN/Zk6dfHDEg9EbEG5MsBBtYvbtjQi4WDpdL1SvWa10sjMmDo2OCJ/CA5uym/qGxijtTc4eXXxPFl3ZSSSgTI6DQfpZMEp6zedkij1BTqe6DYg72kP33Ocb47h6NuvI9zdesIrikdtx/OeVkAk9szB5XZz1O4SlSnl123gXXHkxxq8t+SRA
I think it would be in whatever meta-logic you use to formalize ZF.
You construct a Turing machine that enumerates *every possible* proof in ZF (every legal combination of inference rules and axioms). This is possible since valid proofs are recursively enumerable. You make the machine check if any one of them proves 'False'. If yes, the machine halts.
for proof in all_zf_proofs() { // infinite iterator / stream
if proof.statement() == Logic::False { break; }
}
Then you do a bunch of PL and compiler engineering to get that Turing machine down to 748 states.
Done.
(You can do this with any proof system, of course, not just ZF.)
; Ralf
On 24.06.21 11:07, Marco Servetto wrote:
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?
--
Website: https://people.mpi-sws.org/~jung/
- Re: [Coq-Club] True arithmetical proposition not provable, (continued)
- Re: [Coq-Club] True arithmetical proposition not provable, Pierre-Marie Pédrot, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Vincent Semeria, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Andrei Popescu, 06/22/2021
- [Coq-Club] Tacit implications in Goedel's theorems II – Re: True arithmetical proposition not provable, Ken Kubota, 06/23/2021
- Re: [Coq-Club] Tacit implications in Goedel's theorems II – Re: True arithmetical proposition not provable, Marco Servetto, 06/24/2021
- Re: [Coq-Club] Tacit implications in Goedel's theorems II – Re: True arithmetical proposition not provable, Pierre Courtieu, 06/24/2021
- Re: [Coq-Club] Tacit implications in Goedel's theorems II – Re: True arithmetical proposition not provable, Ralf Jung, 06/24/2021
- Re: [Coq-Club] Tacit implications in Goedel's theorems II – Re: True arithmetical proposition not provable, Ralf Jung, 06/24/2021
- Re: [Coq-Club] Tacit implications in Goedel's theorems II – Re: True arithmetical proposition not provable, Marco Servetto, 06/24/2021
- Re: [Coq-Club] Tacit implications in Goedel's theorems II – Re: True arithmetical proposition not provable, Ralf Jung, 06/24/2021
- Re: [Coq-Club] Tacit implications in Goedel's theorems II – Re: True arithmetical proposition not provable, Marco Servetto, 06/24/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Vincent Semeria, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Pierre-Marie Pédrot, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, roconnor, 06/29/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Louis Garde, 06/29/2021
- Re: [Coq-Club] True arithmetical proposition not provable, roconnor, 06/29/2021
- Re: [Coq-Club] True arithmetical proposition not provable, roux cody, 06/29/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Vedran Čačić, 06/30/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Marco Servetto, 06/30/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Vincent Semeria, 06/30/2021
- Re: [Coq-Club] True arithmetical proposition not provable, roconnor, 06/29/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Louis Garde, 06/29/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Vincent Semeria, 06/20/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Dominik Kirst, 06/22/2021
Archive powered by MHonArc 2.6.19+.