The Coq mailing list

[Dominik Kirst <dominik.kirst AT cs.uni-saarland.de>]

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:

https://www.ps.uni-saarland.de/extras/axiomatisations/

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.