inductive type constructor parameterized by Pi to itself

Stream: new members

[Chris M]

I was reading the reference manual on inductive types and didn't understand how rec deals with so called "recursive arguments". It states: "The ith minor premise is a function which takes [...] an argument of type Π (d : δ), C (bⱼ d) corresponding to each recursive argument (bⱼ : βᵢⱼ), where βᵢⱼ is of the form Π (d : δ), foo (the recursive values of the function being defined)"

I didn't understand this, so tried this out:

universes v u
constant X:Type
inductive ind4 : Type (u+1)
| const5 : Π b:(Π x:X, ind4), ind4

#check @ind4.rec

There are two things I don't understand about this:

1. How is const5 and ind4 well-defined? It seems like in order to construct the type Π x:X, ind4 we first need to have constructed the type ind4. I can vaguely imagine that this doesn't lead to contradictions and hence is ok, e.g. by arguing that in defining const5 f, the function f must be a function that doesn't have const5 f itself in its image. Nevertheless it seems a bit suspect and I'm not sure how to justify this.
2. Even more suspect seems to me the use of rec for this. It has the type ind4.rec : Π {C : ind4 → Sort u_1}, (Π (b : X → ind4), (Π (x : X), C (b x)) → C (ind4.const5 b)) → Π (n : ind4), C n. The part of this that seems suspect is (Π (b : X → ind4), (Π (x : X), C (b x)) → C (ind4.const5 b)), because it's not obvious to me that this induces a well-founded recursion: How do we know that b only outputs members of ind4 for which the recursion "has already been done"?

I might be misunderstanding something more fundamental.

[Kevin Buzzard]

Are you happy with the definition of the natural numbers?

[Kevin Buzzard]

Is your situation any different?

[Kevin Buzzard]

The inductive command makes ind4 and ind4.const5 and ind4.rec all appear at the same time

[Chris M]

After thinking about it more, it seems like we at least want the condition \forall x:X, \forall (b:\Pi x:X, ind4), (b x) \neq (const5 b), and I'm guessing that this is automatically satisfied.

[Chris B]

There's no way to actually create an element of your type (if b's domain type is inhabited) . Mario Carneiro showed this proof in another thread, but it applies here.

universe u
variable {A : Type}

inductive ind4 : Type (u+1)
| const5 : Π b:(Π x:A, ind4), ind4

def no_ind4 [inst1 : inhabited A] : ind4 -> false :=
λ h, ind4.rec_on h (λ h1 h2, false.elim $ h2 inst1.default)

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Basic.20building.20block.20tactics/near/189382869

[Alistair Tucker]

This is like a bastardised version of the type I suggested in your other thread:

inductive tree {α : Type} (β : α → Type)
| mk (a : α) (φ : β a → tree) : tree

The addition of dependent types makes it more useful. Say α is ℕ and β is fin. A leaf node can be constructed with a = 0 because fin 0 is empty. You can construct further nodes out of those, parametrised by a the number of children. In general you have to understand that the only terms of a type are those you can actually construct. This way of thinking may seem a little alien if you have taken more maths classes than CS classes.

[Chris M]

Chris B said:

There's no way to actually create an element of your type (if b's domain type is inhabited) . Mario Carneiro showed this proof in another thread, but it applies here.

universe u
variable {A : Type}

inductive ind4 : Type (u+1)
| const5 : Π b:(Π x:A, ind4), ind4

def no_ind4 [inst1 : inhabited A] : ind4 -> false :=
λ h, ind4.rec_on h (λ h1 h2, false.elim $ h2 inst1.default)

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Basic.20building.20block.20tactics/near/189382869

To be clear, this doesn't actually prove that it's impossible to construct an instance of ind4, does it? It just proves that if this would be possible, Lean's type theory would be inconsistent. Do we actually know that it's consistent?

[Kevin Buzzard]

Oh come on. What do you mean by "know"?

[Kevin Buzzard]

I know it's consistent in the sense that it's equiconsistent with the system that me and gazillions of other mathematicians are using every day. But by Gödel we can't prove this within the system, we can only prove it within a system strictly more likely to be inconsistent

[Chris M]

For the purpose of that comment, I meant "have a proof of". I'm not saying I doubt it, I'm just curious in the meta mathematics of this

[Kevin Buzzard]

A proof assuming what?

[Kevin Buzzard]

Certainly lean can't prove its own consistency, in common with every consistent system strong enough to construct the natural numbers, by godel

[Chris M]

I think Godel's theorem tells us that we can't prove the consistency of a set of axioms within a logic, not that we can't prove the consistency of a formal deductive system of that logic?

[Jalex Stark]

you might find it helpful to read some of mario's msc thesis
https://github.com/digama0/lean-type-theory

[Jalex Stark]

Chris M said:

I think Godel's theorem tells us that we can't prove the consistency of a set of axioms within a logic, not that we can't prove the consistency of a formal deductive system of that logic?

i have a hard time imagining a difference between the two sides of the "not that"

[Jalex Stark]

i think if you want to have a nuanced discussion about the evidence for the consistency of lean, you need to start from precise definitions

[Anatole Dedecker]

Chris M said:

To be clear, this doesn't actually prove that it's impossible to construct an instance of ind4, does it? It just proves that if this would be possible, Lean's type theory would be inconsistent. Do we actually know that it's consistent?

Then I guess you can say that we can never prove 0≠1, we can just prove that if it was possible to prove 0=1 Lean would be inconsistent. This is just the definition of negation, if you accept to extend it to any Type u

[Chris M]

Ah mario's thesis says that ZFC and CIC can prove each other's consistency. That's basically what I wanted to know. :)

[Chris M]

Anatole Dedecker said:

Chris M said:

To be clear, this doesn't actually prove that it's impossible to construct an instance of ind4, does it? It just proves that if this would be possible, Lean's type theory would be inconsistent. Do we actually know that it's consistent?

Then I guess you can say that we can never prove 0≠1, we can just prove that if it was possible to prove 0=1 Lean would be inconsistent. This is just the definition of negation, if you accept to extend it to any Type u

Right, I hadn't thought of it that way, thanks :)

[Kevin Buzzard]

@Chris M I think that actually Lean is equiconsistent with ZFC + infinitely many universes, but mathematicians use universes when push comes to shove...