Grelling–Nelson Paradox (in Coq)

GrellingParadox.v

(** Grelling–Nelson Paradox.

  Module [GnpLogic] is the basic logical analysis,
  with the conclusion "phi is incomplete".

  Module [GnpExtLogic] is the first attempt at extending
  the logic, but fails to change the conclusion: indeed
  it turns out rather indicative that the "paradox" holds
  regardless of the specifics of [phi]: having the *type of*
  [phi] in the context (IOW, that the class of such functions
  is expressible in the language) turns out to be condition
  enough.

  Module [GnpCloLogic] is an attempt at closing the logic by
  extending the domain of discourse, but only partially
  extending (the type of) [phi].  This seems to work...
  "Revenge" anyone?
*)

Module Type GnpSpec.
  Parameter U : Set.
  Parameter phi : U -> U -> Prop.
End GnpSpec.

Module GnpLogic (Spec : GnpSpec).

  Include Spec.

  Definition peq (p q : U -> Prop) : Prop :=
    forall (x : U), p x <-> q x.

  Definition rep (x : U) (p : U -> Prop) : Prop :=
    peq (phi x) p.

  Definition aut (x : U) : Prop := phi x x.
  Definition het (x : U) : Prop := ~ aut x.

  Theorem no_het_in_phi :
    ~ exists (h : U), rep h het.
  Proof.
    unfold rep, peq, het, aut.
    intros [h H].
    destruct (H h) as [HPN HNP].
    assert (HP : phi h h).
    {
      apply HNP.
      intros HP.
      apply (HPN HP HP).
    }
    apply (HPN HP HP).
  Qed.

End GnpLogic.

Module GnpLogic_NatEq.  (* a usage example *)

  Module GnpNatEqSpec <: GnpSpec.
    Definition U : Set := nat.
    Definition phi (x y : U) : Prop := x = y.
  End GnpNatEqSpec.

  Module GnpNatEq := GnpLogic GnpNatEqSpec.

  Import GnpNatEq.

  Compute phi 1.
    (* = fun x : U => 1 = x : U -> Prop *)

End GnpLogic_NatEq.

Module Type GnpExtSpec <: GnpSpec.
  Include GnpSpec.
  Parameter psi_fi : U -> Prop.
  Parameter psi_if : U -> Prop.
End GnpExtSpec.

Module GnpExtLogic (Spec : GnpExtSpec).

  Include Spec.

  Inductive W : Set :=
    | W_f : U -> W
    | W_i : W.  (* single non-standard element *)

  (* The case [psi] from [W_i] to [W_i] is not defined,
     so [psi W_i W_i] is provably false... but,
     it doesn't matter, see below... *)
  Inductive psi' (w1 w2 : W) : Prop :=
    | Psi_ff (u1 u2 : U)        (* [psi] over [phi] *)
        (E1 : W_f u1 = w1) (E2 : W_f u2 = w2) (H : phi u1 u2)
    | Psi_fi (u1 : U) (w2 : W)  (* [psi] from [U] to [W_i] *)
        (E1 : W_f u1 = w1) (E2 : W_i    = w2) (H : psi_fi u1)
    | Psi_if (w1 : W) (u2 : U)  (* [psi] from [W_i] to [U] *)
        (E1 : W_i    = w1) (E2 : W_f u2 = w2) (H : psi_if u2).

  (* [psi] is an uninhabited type,
     so [psi w1 w2] is identically false. *)
  Inductive psi : W -> W -> Prop := .

  Definition peq (p q : W -> Prop) : Prop :=
    forall (x : W), p x <-> q x.

  Definition rep (x : W) (p : W -> Prop) : Prop :=
    peq (psi x) p.

  Definition aut (x : W) : Prop := psi x x.
  Definition het (x : W) : Prop := ~ aut x.

  Theorem no_het_in_psi :
    ~ exists (h : W), rep h het.
  Proof.
    unfold rep, peq, het, aut.
    intros [h H].
    destruct (H h) as [HPN HNP].
    assert (HP : psi h h).
    {
      apply HNP.
      intros HP.
      apply (HPN HP HP).
    }
    apply (HPN HP HP).
  Qed.

  (* A specific consequence of [psi] empty. *)
  Lemma psi_totally_incomplete :
    forall (p : W -> Prop),
      (exists (x : W), p x) ->
      ~ exists (h : W), rep h p.
  Proof.
    unfold rep, peq.
    intros p [x HPx] [h H].
    destruct (H x) as [_ HPS].
    assert (HNS : ~ psi h x)
      by intros [].
    apply HNS.
    apply (HPS HPx).
  Qed.

End GnpExtLogic.

Module GnpCloLogic (Spec : GnpSpec).

  Module GnpLogic := GnpLogic Spec.

  Include GnpLogic.

  Inductive W : Set :=
    | W_f : U -> W
    | W_i : W.  (* a single non-standard element *)

  (* [psi] is (as) a partial function on [W*W]. *)
  Definition psi (w : W) (u : U) : Prop :=
    match w with
    | W_f u' => phi u' u
    | W_i    => het u
    end.

  Definition rex (w : W) (p : U -> Prop) : Prop :=
    peq (psi w) p.

  Theorem het_in_psi :
    exists (h : W), rex h het.
  Proof.
    exists W_i.
    unfold rex, peq.
    simpl.
    intros u.
    split
    ; intros H
    ; apply H.
  Qed.

End GnpCloLogic.

<<Indeed, together with a notion of functional extensionality (represented by 'peq'), that 'phi' is a total function seems all it takes for the "paradox" to apply. >> "Grelling–Nelson Paradox (in Coq)" at sci.logic