non-positive occurrence of datatype being declared?

Stream: general

[SnowFox]

set x is defined as x -> Prop. Why is this an invalid inductive? Is there a way to have an inductive contain functions over it?

inductive bar : Type
| alpha : bar
| beta (bars : set bar) : bar

arg #1 of bar.beta has a non positive occurrence of the datatypes being declared

[Adam Topaz]

How would you map out of it?

[SnowFox]

What do you mean? The set should be little different than a list. It is just a function; as is list after erasing abstractions.

[Adam Topaz]

To define an inductive type you need to define its recursor, which tells you how to map out of the inductive type.

[Floris van Doorn]

Constructors in inductive types (like alpha and beta) are provably injective.
Your beta gives an injection from bar -> Prop into bar, contradicting Cantor's diagonal argument. So your inductive type would make the theory inconsistent.

[Floris van Doorn]

Here is an answer to a similar earlier question: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/question.20about.20game.20theory/near/162067308

[SnowFox]

Sorry, I don't follow. Mind elaborating?

[Mario Carneiro]

The beta constructor is injective, but this implies that set bar is smaller than bar, which is a violation of Cantor's theorem, so you can prove false from the existence of bar

[SnowFox]

How is set bar different from list bar or even bar?

[Floris van Doorn]

set bar is the collection of all subsets of bar, i.e. the power set of bar.

[SnowFox]

A list of bars already has unbounded cardinality.

[Floris van Doorn]

That depends on bar. But it's irrelevant. set bar contains arbitrary collections of elements of bar and list bar only contains finite collections (and the order matters). That's the difference.

[SnowFox]

I see... Hmm. Thanks everyone.

[Mario Carneiro]

@SnowFox The general rule is that as long as the type operator has a cardinality-bounded number of "slots" into which to put the type being defined, an inductive type satisfying the condition exists. This is the "bound" in "bounded natural functors" that are used for the analogue of this kind of inductive construction in isabelle. In the case of list, the bound is nat, and you can do it in lean without even using nested inductives with mk : (nat -> bar) -> bar, and in fact you can even use mk : (A -> bar) -> bar, or even mk (A : Type) : (A -> bar) -> bar, where we are generalizing over all types in Type; in this case the cardinality bound lives in the next universe. But set bar -> bar doesn't have a bounded number of slots at all, the number of slots just keeps growing as you add more elements. In lean, this is implemented through a syntactic check - (bar -> Prop) -> bar contains a use of bar on the left of the left of an arrow and that is not allowed.