The Coq mailing list

[Vincent Semeria <vincent.semeria AT gmail.com>]

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.