coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] True arithmetical proposition not provable

From: Anders Lundstedt <a AT anderslundstedt.se>
To: coq-club AT inria.fr
Cc: Vincent Semeria <vincent.semeria AT gmail.com>
Subject: Re: [Coq-Club] True arithmetical proposition not provable
Date: Sun, 20 Jun 2021 23:02:58 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=a AT anderslundstedt.se; spf=Pass smtp.mailfrom=anders AT anderslundstedt.se; spf=None smtp.helo=postmaster AT mail-lj1-f181.google.com
Ironport-hdrordr: A9a23:EgXE3qzYIWn/8+7DG80MKrPwFb1zdoMgy1knxilNoH1uA7WlfqWV9sjzuiWE7Qr5NEtQ++xofZPwIk80lqQV3WByB8bHYOCOggLBR72Kr7GD/9SKIVyYygcy79YHT0G8MrHN5JpB4PoSLDPWLz/o+re6zJw=
Ironport-phdr: A9a23:nDpviBProg43priy1tUl6nbeDRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDvKQr1wSWFtyCtLptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uyv/5DfeQtFiTS/bL99MRm6sAfcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/9KpgVgPmhzkbOD446GHXi9J/jKRHoBK6uhdzx5fYbJyJOPZie6/Qe84RS2hcUcZLTyFODY28YIkPAeQPPuhWspfzqEcBoxalGQmsHfnixiNUinPq36A31fkqHwHc3AwnGtIDqGjZrNPoO6gMS+C117TDwzPeb/NQxDj985TIfQ48rvGQQLl9dtDexFI1GAPDk1qft5blPyiR1uQQtWiU8vFgVf6xhGE6twF9uCOvydk1h4TPm4kaxUzK+z9jz4YpOd23VlR7Ydi8HZVetCyWKol7T8wsTWx0pSo3y7kLtJC4cSUKyZkqxR7RZuKIfYWJ/x7vSOacLCp2inxlfL+zmRm8/FWuxODgVcS51ktBoCldktTUqHwByxje5tKER/Z95EutxyqD2gPJ5u1ZIk04iKzWIIM7zLEqjJocq0HDEzf2mEroiK+WcV0p+u2y5OTmZrXqv5ucN41phg3nPKQih8+yDfkiPggBWGib/uu81Ln98kHjXLpKifg2nrHYsJDcO8sbura0DxFJ3osn8RqyDDer3M4GkXUbL19JYg+Lgov0N13WJfD3F/a/g1CikDdxwPDGO6XsDY/LLnfejrjhZ6195lVGxwo10N9Q+YhUCqoFIPLuXE/+qcfYDgMnPAOp3+brEs592Z0GVWKVHqCZKL/SsUOP5u83P+aMY5YVtC/hJPgh+v7hlmQ0mUQdfKmsxZsYcmq0HvVgI0WDYHrjmM0NEWkQvll2cOu/g1qbFDVXenyaXqQm5zh9Bpj1I53EQ9WEhrCMxjzzOoBQantaB1yQWSPhX4yCV/oWcyaPJMN6jjEISf66RtlyhlmVqAbmxu8/faLv8SoCuMemjYAtjwUyvRQ79DgxC8bElm/UHzgykWQPSDs7mqt4pB4lor9s+aF+j/FCDthO4f9STgo2KdjHwr4jYzgXcgvHctqTU1K7RNm9HTw9UpQqzo1WC3s=

On Sat, Jun 19, 2021 at 2:25 PM Pierre-Marie Pédrot
<pierre-marie.pedrot AT inria.fr> wrote:
> There are deep reasons why Gödel went into the study of constructive
> logic after the discovery of incompleteness. Being able to compute is a
> very good way to trust some statements.

Sounds intriguing! For someone who is somewhat ignorant of both
fundamental issues and the history of the subject, could you perhaps
expound on this, or provide some references?

Best,

Anders Lundstedt

[Coq-Club] True arithmetical proposition not provable, Vincent Semeria, 06/19/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Pierre-Marie Pédrot, 06/19/2021
  - Re: [Coq-Club] True arithmetical proposition not provable, Anders Lundstedt, 06/20/2021
    - Re: [Coq-Club] True arithmetical proposition not provable, Marco Servetto, 06/20/2021
      - Re: [Coq-Club] True arithmetical proposition not provable, Christopher Ernest Sally, 06/21/2021
        
        Re: [Coq-Club] True arithmetical proposition not provable, Ian Shillito, 06/22/2021
        
        Re: [Coq-Club] True arithmetical proposition not provable, Christopher Ernest Sally, 06/22/2021
        
        Re: [Coq-Club] True arithmetical proposition not provable, Ian Shillito, 06/22/2021
      - Re: [Coq-Club] True arithmetical proposition not provable, Peter LeFanu Lumsdaine, 06/21/2021
        
        Re: [Coq-Club] True arithmetical proposition not provable, Vedran Čačić, 06/21/2021
        
        Re: [Coq-Club] True arithmetical proposition not provable, Xavier Leroy, 06/21/2021
        
        Re: [Coq-Club] True arithmetical proposition not provable, Peter LeFanu Lumsdaine, 06/22/2021
  - Re: [Coq-Club] True arithmetical proposition not provable, Vincent Semeria, 06/22/2021