Stream: Coq users

Topic: Dealing with injection with Impredicative Set

Pierre Vial (Nov 04 2022 at 12:48):

Hello,
According to Coq wiki article, one cannot have injectivity of the constructor when Set is impredicative.
Such as it is, one reads "The question remains open whether injectivity is consistent on some large inductive types not expressive enough to encode known paradoxes (such as type I above)."

I would like to retrieve injectivity of the constructors in particular cases.
For instance, I have an inductive:

Inductive foo : Set :=
  | Foo : forall (c : Set), bar c -> foo
.

I would like to be able to have Foo c1 b1 = Foo c2 b2 implies c1 = c2 and b1 = b2 .

1. Could it be that it is provable? (bar is a record whose fields are probably nice)
2. If not, is it an ok solution to axiomatize the injectivity of Foo without causing (at least major) inconsistency?

Remark: it is possible that I add c1 = c2 as an hypo without danger

Paolo Giarrusso (Nov 04 2022 at 13:14):

That seems a problem.
Axiom foo_inj : forall c b1 b2, Foo c b1 = Foo c b2 -> b1 = b2 isn't _as clearly_ unsound, but since it isn't provable, I'd rather consider using

  Inductive foo (c : Set) : Set :=
    | Foo : bar c -> foo c
  .

Paolo Giarrusso (Nov 04 2022 at 13:17):

While the Burali-Forti's paradox is complicated, my personal rule of thumb is that for any universe U there are always "more" types T : U than values v : T : U, so an injection inj : U -> T with T : U is inconsistent.

Pierre Vial (Nov 04 2022 at 13:18):

Unfortunately, foo is given to me, so I don't have much choice.
However, I have validity predicates on foo, bar and other types which I have to deal with and regarding which I have some liberty, so maybe I can recover the property that I want somehow

Pierre Vial (Nov 04 2022 at 13:19):

Paolo Giarrusso said:

While the Burali-Forti's paradox is complicated, my personal rule of thumb is that for any universe U there are always "more" types T : U than values v : T : U, so an injection inj : U -> T with T : U is inconsistent.

Would you have references about the Burali-Forti paradox in the impredicative setting?

Paolo Giarrusso (Nov 04 2022 at 13:22):

... The "scare quotes" in my rule of thumb are necessary: this rule only makes sense in a specific kind of set-theoretic model (there's a set V_U of values for universe U, and types are modeled as the predicates 2^V_U). But scenarios that fail in this model seem often suffer from Burali-Forti/Girard/Hurken's paradox

Paolo Giarrusso (Nov 04 2022 at 13:32):

Can you rephrase Foo as:

  Inductive foo' (c : Set) : Set :=
    | Foo' : c -> foo' c
  .
  Inductive foo : Set :=
    | Foo c : foo' c -> foo
  .

Foo remains unusable, but at least Foo' is injective, and you might be able to use foo'/Foo' in enough places to fix your proof. Basically, this separates the "real datatype" foo' from the "potentially singleton" foo.

Re "references", https://www.cs.cmu.edu/~kw/scans/hurkens95tlca.pdf exists and I've been able to walk through it, but I haven't found it extremely helpful. Among the other answers one finds by googling, I'll highlight https://mathoverflow.net/a/235908/36016 and http://liamoc.net/posts/2015-09-10-girards-paradox.html.

Last updated: Sep 26 2023 at 12:02 UTC