coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Louis Garde <louis.garde AT free.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] True arithmetical proposition not provable
Date: Tue, 29 Jun 2021 18:07:40 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=louis.garde AT free.fr; spf=Pass smtp.mailfrom=louis.garde AT free.fr; spf=None smtp.helo=postmaster AT smtp3-g21.free.fr
Ironport-hdrordr: A9a23:p6JFFa6zaJAphplBrAPXwN/XdLJyesId70hD6qkDc20wTiX4rbHKoB11737JYVoqN03I3OrwWpVoIkmslqKdg7N+AV7KZmCP01dAbrsP0WKI+Vfd8kPFm9K1mZ0BT5RD
Ironport-phdr: A9a23:pf4zvR09RY0T+D2XsmDOeQQyDhhOgF0UFjAc5pdvsb9SaKPrp82kYBWOo64z1BSSDc3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmTowZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsiq0+2+4ZPebgRUiDayb75/Lwi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkaKTA5/mHZhM9+gq1Vrx2upQBwzpXOb42JLvdzZL/RcN0YSGdHQ81fVzZBAoS5b4YXCeQBOvtYr4jmp1ATrBWxHxOsC/7xxTRVgXL22ao60/kgEQHdxgAgEMgBsG7Jo9rrL6oSX/q1w7fWwjnZYfNWwy7w5Y7VeR8uvf+CR6h/cdbNyUYxDQPFiE2dp4P4Mj+LyOgArXaW4u5gW+6yhWMqrw58riSzy8ouloXHiZwYxk7Z+Sh6wos7Jd+1RkFnbNK6DZZdtCGXOpV1T84kXmpmtiE6yrgctp66eigH0Jomxx/ca/yGa4iH/A/sVOeLLjtig3JlYr2/ihCv+kaj0u3xTte43EtUoiZfjNXBtGoB2hPN5sSdRPZx5lmt1iyT2wzO7+xLP1w4mrDeJpE93LE9k5QTvl/eESPqnUj7grKae0Eq9+Wt6enqYLrrq5uZOoJ7lg3zMKoul8mwDOgmMAUOUW6W8vmm2rL55032WrBKg+U2kqbHtJDaItwWprW8Aw9JyoYu5Q+zDzi43NgFh3UHIkhFdwyZgITzNVHOOuj0Dfa5g1uyjDdm3+7KMqD/DpnXMHTOkq3tcLlj50JGxgc/1dVf6IhVCrEFLvLzQEjxtNnAAx89NAy03ufnCM5n2oMRQ22PGLKWP73JvF+G/OIgPfeDaJUbuDbnM/Ql/eLhjWclmV8BeqmkxYcYaHehHvh/P0qZZWfsjcwaHGcRvgs+SfTqh0eYXT5SYXayRaM86SshBIKoF4eQDryq1beGxWKwGoBcTmFAEFGFV3nyJKueXPJZTCWPI9QpvTUeWbXpH4smyBC18gDz0bZqBuTO9yBeu4i1h4s93PHaiRxnrW88NM+ayWzYFwmcf0sTQiMuh+Vw+xU7xE2O3O52ma4AfTS2z/1TXwp8O4SOl4SS5Pj8QA/MONmTGg/Ofw==

Le 29/06/2021 à 17:12, roconnor AT theorem.ca a écrit :

Thus the Goedel sentence G is true when ¬G is not provable.

It is a fact that the notion of truth is not formally part of the Gödel theorem itself, which is "just" the exhibition of an unprovable sentence. To introduce the concept of truth as you have done, you had to specify an interpretation of the sentence, and therefore you had to work at the meta level, which is just the point of Pierre Marie Pédrot.

There is no doubt that the Gödel sentence is true in some interpretations, and in the natural one. There is also no doubt that the Gödel sentence is false in some other interpretations, see for instance Truth of the Gödel sentence.

Louis.

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
    - Re: [Coq-Club] True arithmetical proposition not provable, Dominik Kirst, 06/22/2021