Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • To: coq-club AT inria.fr, Vincent Semeria <vincent.semeria AT gmail.com>
  • Subject: Re: [Coq-Club] True arithmetical proposition not provable
  • Date: Sat, 19 Jun 2021 14:25:06 +0200
  • Ironport-hdrordr: A9a23:xJM3Daslcg4p+6bfK6x97vHh7skDadV00zEX/kB9WHVpm62j5qKTdZsguyMc5Ax9ZJhko6HiBEDiexPhHPxOjrX5VI3KNDUO+lHDEGgI1+ffKlPbcBEWutQ96Ztd

pOn 19/06/2021 10:22, Vincent Semeria wrote:
> Assuming LPO, I defined interpretations of arithmetical formulas in Coq,
> both in bool and in Prop, as shown below. I imagine that Coq's
> consistency is an arithmetical formula that would be interpreted to true
> by InterpBool.

No. Since you use a non-computable axiom you'll get a stuck term which
is neither true nor false. And you won't be able to prove that it is
indeed one of true or false, with the disjunction in the meta, i.e.
there is neither a proof of "InterpBool Φ = true" nor a proof of
"InterpBool Φ = false".

More generally, by Gödel's theorem Π01 formulae are the worm in the
apple, since they can encode the soundness of an arbitrarily complex
problem. Identifying Prop with bool is just moving the problem in
another place.

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.

PMP

Attachment: OpenPGP_signature
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.19+.

Top of Page