Skip to Content.
Sympa Menu

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

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/



Archive powered by MHonArc 2.6.19+.

Top of Page