Inductive Types vs. Axioms

Stream: new members

[Marcus Rossel]

IIRC, using the constant keyword in Lean is the same as declaring an axiom. So e.g:

constant fruit : Type*
constant apple : fruit

would axiomatically define a fruit type with a member apple.

What I don't understand is how inductive type declarations are different from this. E.g. if I write ...

inductive fruit : Type*
| apple : fruit

... then where are this new type and value coming from, if not by axioms?

[Ruben Van de Velde]

My understanding is that you're right that they're essentially similar, but inductive is more limited in what axioms it creates, so it can't make your logic inconsistent

[Kevin Buzzard]

Right -- you have the guarantee that you didn't just enable a proof of false with the inductive definition. You can just make a constant term of type false

[Kevin Buzzard]

The inductive definition also makes a recursor, which is also defined as a constant

[Kevin Buzzard]

Check out #print fruit.rec

[Kevin Buzzard]

And then an internal system makes a bunch more stuff -- check out #print prefix fruit

[Kevin Buzzard]

The recursor says "apples are the only fruit" -- you don't get this with the constant definition

[Marcus Rossel]

Wow ok, so we are in fact adding axioms with every inductive type definition.
Would there be other ways of creating new types, or is there a particular reason we need to do it by adding axioms?

[Kevin Buzzard]

I'm not a type theorist. My basic understanding is that this is just how the calculus of inductive constructions works

[Kevin Buzzard]

There are three ways of making types in lean, inductive types, function types and quotient types, and as far as I am concerned each thing just happens by magic

[Marcus Rossel]

That's why we need @Mario Carneiros in this world :D

[Kevin Buzzard]

You make terms of inductive types using the constructors (which were magically added as constants when the inductive type was made), you make terms of function types with lambdas, and you make terms of quotient types with quot.mk

[Marcus Rossel]

I never knew that quotient types were so foundational. Do they basically behave as "take a type and make a new one by collapsing members according to a given equivalence relation"?

[Mario Carneiro]

That's what it means to be a quotient type, but if it were just that you could build them with set-quotients

[Mario Carneiro]

The reason they are axiomatic is so that they get the computational rule lift f h (quot.mk a) = f a

[Mario Carneiro]

you can't add custom definitional equalities in lean's type theory, so any new defeqs have to be axiomatized as part of the theory

[Mario Carneiro]

Same thing with inductive types - you can kind of build them using church encodings if you don't care about the computational rules

[Mario Carneiro]

that doesn't completely work though because inductive types are magical in that the recursor for a (large-eliminating) inductive type mentions a free universe variable

[Mario Carneiro]

inductive nat' : Type
| zero : nat'
| succ : nat' → nat'

#print nat'.rec
-- protected eliminator nat'.rec : Π {C : nat' → Sort l}, C nat'.zero → (Π (ᾰ : nat'), C ᾰ → C ᾰ.succ) → Π (n : nat'), C n

where did that universe l come from? :thinking:

[Mario Carneiro]

Here's a definition of nat using church encodings:

def nat' : Type 1 :=
{ f : Π {C : Type}, C → (C → C) → C //
  ∀ A B (e : A → B) (a0 : A) (b0 : B) (h0 : e a0 = b0)
    (as : A → A) (bs : B → B) (h1 : ∀ a, e (as a) = bs (e a)),
    e (f a0 as) = f b0 bs }

You can kind of tell this definition has a universe issue though, because it's in the wrong universe - it lives in Type 1 but the recursor for this type only works in Type instead of Type u like the axiomatic inductive type nat