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: Dominik Kirst <dominik.kirst AT cs.uni-saarland.de>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] True arithmetical proposition not provable
  • Date: Tue, 22 Jun 2021 20:57:43 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dominik.kirst AT cs.uni-saarland.de; spf=Pass smtp.mailfrom=dominik.kirst AT cs.uni-saarland.de; spf=None smtp.helo=postmaster AT theia.rz.uni-saarland.de
  • Ironport-hdrordr: A9a23:7LD+Na2aXVCV5c2P+NGhCAqjBKckLtp133Aq2lEZdPU1SKOlfq+V/MjzuSWZtN9VYgBEpTn/AtjlfZqsz/BICOAqVN/INmTbUSmTXeJfBODZogEIdReOlNK1rZ0QFJRDNA==
  • Ironport-phdr: A9a23:XMbJchDWZs+H54ubfmb0UyQU80MY04WdBeb1wqQuh78GSKm/5ZOqZBWZuaw8ygSVBM6CsaMMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5pnebx9GiTeyfL9+Iwi6oRvVu8ILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8qFmQwLqhigaLT406GHZhdB/g6xGrhyhqQJxzIzXbo+SL/dxZL/RfdYASGpBQspcVSpMCZ68YYsVCOoBOP5VoYf6p1sLrBu+AwisBODywTFNh3/2x7Y60/g8GgzBwQMgGNcOsHXSrNX0N6ceS+O1zKjSzTXYc/Nbwivy6JPSfhA8p/GMXKt8cdHLxkY1DQPFik+fqYr4MD+Py+sCrXGW4ux9Xu2gl2ApsRt+oiSzxsgykInJgJoYxF/E+Ch73Io4KtO1RFBnbNOgEJZduT+WOYV4TM4iQ2xluiQ3x7wGtJC0YSQHyYoqyh7RZfGGb4WF4hHuWeefLzp+mXlrdrW/hxOo/kihzO3xTtS00FBLriZcidnDrGoC1wbX6sedTPty412t1iuR2A3V9+pKIlg0mLLGJ5MvzbM8jJ4evEXZEiL0gkn7grKael0n9+S28ejrfKnqq52GO4NqhAzzML4iltGxDOk6NAUFQnKV9v6m1LL5+E30WLVKgeMykqneqJ3aOcQbqbC4AwBPyIoj8Re+Ay270NQenHkLNUlFdwidgIjzP1HBOvb4Auqlj1uxjjhn3/HGPrv/DZXRNnXPjbnscLln50NYyQc/19JS64haB70cOP7zX1X+tN3cDh83KQy0xOPnBc1g2YMZXGKPA6mZMKLRsVOS5eIvIvOMZJQJuDvmN/cl/OTijWI/mV8cZKWpxoEYZ2qiHvRiOUqZZ2fjjs0cHmgUpgY+VvDliEWeUT5PYHa/R74z5jYiCI6/EYjDQp2tj6ea0SegHpxWY3hGBUqWHXfpcYWEQfYMZziILs9viDxXHYSmHoQmzFSlsBLw47thNOvdvCMC5rz5090gy+rWlBcz9nRXDt6GzynZQ2Zxn2UJRHk13bpkvWR20RGe16k9mPVRD9ha4f8PXgpsZs2U9PBzF92nAlGJRdyOUlvzGr1O5Bk6VZQsxd5LeE90AdGriByF0yf4W9f9dpSXBJE1++TGzT7sIcc40H/Pzq0oiVVgTsYdbQVOaYZ07E7OAY+MiEyQjaKjc6ha0COfrQ++

Gödel's incompleteness theorem applies to any theory that extends arithmetic. Here I choose Coq as that extended theory, and InterpProp is what I imagine does the extension. So more arithmetical formulas are provable than with just the Peano axioms.

Sorry, I somehow thought you were just asking about Con_PA, now I see the question was about Con_Coq and of course agree to PMP’s analysis.

I am actually not sure about this either. How do we do when we apply Gödel's incompleteness to ZFC? I guess arithmetical propositions are likewise interpreted as ZFC formulas where variables become quantified over the set of natural numbers.

Yes I think so, one could for instance show that ZFC is an example of the abstraction identified by Popescu and Traytel in their already mentioned paper. A more lightweight route to abstract incompleteness is to demand that the axiomatisation is able to faithfully express an undecidable problem p, i.e. that p x iff T |- phi_x. Then the deductive theory of T is undecidable and therefore T is incomplete (since complete axiomatisations have a decidable deductive theory). This route imposes much fewer syntactic conditions on T and can be instantiated with non-arithmetic problems p that might be easier to encode in T, at the cost of being much less explicit in not providing a concrete independent Gödel/Rosser sentence.

Btw, I think the confusion regarding both notions of completeness (semantic and deductive) can be explained by the following characterisation: a theory T true in the standard model N is deductively or negation-complete (T derives phi or ~phi for every phi) iff for every phi with N |= phi there is a derivation T |- phi (which looks like semantic completeness but doesn’t quantify over all models of T).

Best wishes,
Dominik



On Sun, Jun 20, 2021, 22:40 Dominik Kirst <dominik.kirst AT cs.uni-saarland.de> wrote:
Hi Vincent,

could you also explain in what sense InterpProp can be seen as the provability predicate for PA? To me it looks like the usual Prop-valued evaluation of formulas in the standard model. If you formulate the provability predicate instead as a concrete inductive predicate just relying on the syntax, you end up with a relation that can indeed be shown strictly weaker than InterpProp. In fact, InterpProp is easily shown negation-complete if you assume LEM on Prop while negation-incompleteness of the provability predicate has already been mechanised a couple of times, not only in Coq.

We’ll actually be presenting one of these mechanisations at ITP in two weeks, maybe the paper is interesting for you as you also mentioned ZFC:

Best wishes,
Dominik



On 19. Jun 2021, at 10:22, Vincent Semeria <vincent.semeria AT gmail.com> wrote:

Gödel's incompleteness theorem asserts that the consistency of first-order theories (such as Peano arithmetic or ZFC) is an arithmetical formula which is true in the standard model of arithmetic, but which is not provable by the theory in question.

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. And not provable would mean that its InterpProp is not provable (as a Prop). However I also proved that InterpBool and InterpProp are equivalent, by an easy induction on the formula. Then I don't see how a true arithmetical formula would be not provable. Is there a problem in my interpretations, or maybe is it because Coq is a second-order logic, in which incompleteness manifests differently ?

Fixpoint InterpProp (varValues : nat -> nat) (p : PeanoProp) {struct p} : Prop :=
  match p with
  | Eq a b => InterpTerm varValues a = InterpTerm PS varValues b
  | Not q => ~InterpProp varValues q
  | And q r => InterpProp varValues q /\ InterpProp varValues r
  | Or q r => InterpProp varValues q \/ InterpProp varValues r
  | Implies q r => InterpProp varValues q -> InterpProp varValues r
  | Forall n q (* i.e. forall Xn, q *)
    => forall m:Inat PS, InterpProp (SetVarValue n m varValues) q
  | Exists n q
    => exists m:Inat PS, InterpProp (SetVarValue n m varValues) q
  end.

Axiom LPO : forall un : nat -> bool, { exists n:nat, un n = true } + { forall n:nat, un n = false }.

Fixpoint InterpBool (varValues : nat -> nat) (p : PeanoProp) {struct p} : bool :=
  match p with
  | Eq a b => Nat.eqb (InterpTerm PeanoNat varValues a)
                     (InterpTerm PeanoNat varValues b)
  | Not q => negb (InterpBool varValues q)
  | And q r => andb (InterpBool varValues q) (InterpBool varValues r)
  | Or q r => orb (InterpBool varValues q) (InterpBool varValues r)
  | Implies q r => implb (InterpBool varValues q) (InterpBool varValues r)
  | Forall n q (* i.e. forall Xn, q *)
    => if LPO (fun m:nat => negb (InterpBool (SetVarValue n m varValues) q))
      then false else true
  | Exists n q
    => if LPO (fun m:nat => InterpBool (SetVarValue n m varValues) q)
      then true else false
  end.

Lemma InterpBoolPropEquiv : forall (p : PeanoProp) (varValues : nat -> nat),
    (InterpBool varValues p = true <-> InterpProp PeanoNat varValues p).
Proof.
induction p. ...
Qed.





Archive powered by MHonArc 2.6.19+.

Top of Page