12
$\begingroup$

Coq lets you define an inductive type of the following form:

Inductive Foo :=
  | Base : Foo
  | Positive : (nat -> Foo) -> Foo.

because the position of Foo in the premise of the Positive constructor is considered by Coq to be a positive position.

Coq rejects an inductive definition where the type being defined appears in a negative position in a premise. Accepting such a definition would enable the construction of non-normalizing terms. In particular, it is not possible to create an induction principle for such a definition.

For example:

Inductive SnaFoo :=
  | Negative : (SnaFoo -> nat) -> SnaFoo.

is rejected with the error message:

Error: Non strictly positive occurrence of "SnaFoo" in "((SnaFoo -> nat) -> nat) -> SnaFoo".

But Coq also rejects the following definition:

Inductive Bar :=
  | IsItPositive : ((Bar -> nat) -> nat) -> Bar.

The position of Bar in the premise of the IsItPositive constructor is not obviously positive but I have seen a presentation (sorry, I can no longer find the link) that accepted this position as positive. I could formulate a plausible inductive principle for Bar as follows:

Definition Bar_ind (P : Bar -> Prop) :=
  (forall (F : (Bar -> nat) -> nat),
    (forall f g, (forall (b : Bar), P b -> f b = g b) -> F f = F g)
    -> P (IsItPositive F))
  -> forall (b : Bar), P b.

More importantly, assuming the existence of enough inaccessible cardinals, I think I can prove that there is a model of Coq's type theory that contains inductive types like Bar, with the inductive principle that I proposed. I did prove that the presence of $\omega^2$ inaccessibles is enough to accommodate Bar itself, assuming that all the other inductive types in the model conform to Coq's positivity rules. I don't know how many inaccessibles will be required to relax the positivity assumptions of Coq in general.

My question is twofold:

First, what is the reason that Coq does not admit definitions like Bar?

Second, what is a good reference for the topic of admissibility of inductive types?

$\endgroup$
6
  • 1
    $\begingroup$ You should write "inductive type" or "inductive family" instead of "induction-recursion". That means something else. None of your examples here are inductive-recursive. $\endgroup$ Nov 20, 2021 at 7:45
  • $\begingroup$ I took the liberty of renaming things. We don't want faulty nomenclature to spill over into the math community. $\endgroup$ Nov 20, 2021 at 9:33
  • 3
    $\begingroup$ You might be better off searching for an answer at cstheory.stackexchange.com, where such questions are discussed periodically. For example, the answers to this question has several useful references. $\endgroup$ Nov 20, 2021 at 9:36
  • $\begingroup$ Thanks András. I had a misconception about the meaning of the term. $\endgroup$
    – Dan Arnon
    Nov 20, 2021 at 15:25
  • 1
    $\begingroup$ By the way, how do you prove the existtence of a non-trivial Bar using inaccessibles? As soon as Bar has more than one element, the cardinality of $(B \to \mathbb{N}) \to mathbb{N}$ will exceed that of $B$. $\endgroup$ Nov 27, 2021 at 18:16

1 Answer 1

4
$\begingroup$

Assuming classical definite description there is a function

decide : forall {A : Prop} (P : A -> Prop), A -> nat

s.t.

(decide P x = 1 <-> P x) /\ (decide P x = 0 <-> ~ P x)

It follows under the assumption of propositional extensionality that, moreover

forall A (P Q : Q -> Prop), decide P = decide Q <-> (forall x, P x = Q x)

Thus, we would have

Definition contains_power (P : Bar -> Prop) : Bar := IsItPositive (fun x => decide P x).

Which would be injective.

As such, your type includes its own power set, which violates Cantor's theorem. For a more detailed account of the argument where Prop replaces nat, see https://coq.inria.fr/refman/language/core/inductive.html in the paragraph "it is less obvious why"

I know not how much of the classical argument here is needed to produce a contradiction, but it seems to me unlikely that there is a sets-and-functions model which has your Bar type in it (assuming, at least, that what ever large cardinals you need are consistent). But, I could imagine that there might be an alternative model, however, that exploits some of the constructive structure of the type theory--maybe this is what you have cooked up?

$\endgroup$
1
  • 1
    $\begingroup$ I think classicality isn't necessary to derive a contradiction; all you need is propositional resizing. There's an argument to this effect in section 5.6 of the HoTT Book. $\endgroup$ Nov 28, 2021 at 6:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.