Zulip Chat Archive
Stream: new members
Topic: inductive type constructor parameterized by Pi to itself
Chris M (Jul 31 2020 at 11:28):
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:
- How is
const5
andind4
well-defined? It seems like in order to construct the typeΠ x:X, ind4
we first need to have constructed the typeind4
. I can vaguely imagine that this doesn't lead to contradictions and hence is ok, e.g. by arguing that in definingconst5 f
, the functionf
must be a function that doesn't haveconst5 f
itself in its image. Nevertheless it seems a bit suspect and I'm not sure how to justify this. - Even more suspect seems to me the use of
rec
for this. It has the typeind4.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 thatb
only outputs members ofind4
for which the recursion "has already been done"?
I might be misunderstanding something more fundamental.
Kevin Buzzard (Jul 31 2020 at 14:20):
Are you happy with the definition of the natural numbers?
Kevin Buzzard (Jul 31 2020 at 14:20):
Is your situation any different?
Kevin Buzzard (Jul 31 2020 at 14:22):
The inductive
command makes ind4
and ind4.const5
and ind4.rec
all appear at the same time
Chris M (Jul 31 2020 at 17:21):
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 (Jul 31 2020 at 18:34):
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)
Alistair Tucker (Jul 31 2020 at 19:14):
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 (Aug 01 2020 at 17:52):
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)
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 (Aug 01 2020 at 18:11):
Oh come on. What do you mean by "know"?
Kevin Buzzard (Aug 01 2020 at 18:12):
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 (Aug 01 2020 at 18:12):
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 (Aug 01 2020 at 18:13):
A proof assuming what?
Kevin Buzzard (Aug 01 2020 at 18:14):
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 (Aug 01 2020 at 18:17):
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 (Aug 01 2020 at 18:18):
you might find it helpful to read some of mario's msc thesis
https://github.com/digama0/lean-type-theory
Jalex Stark (Aug 01 2020 at 18:20):
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 (Aug 01 2020 at 18:21):
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 (Aug 01 2020 at 18:36):
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 (Aug 01 2020 at 18:37):
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 (Aug 01 2020 at 18:39):
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 prove0=1
Lean would be inconsistent. This is just the definition of negation, if you accept to extend it to anyType u
Right, I hadn't thought of it that way, thanks :)
Kevin Buzzard (Aug 01 2020 at 21:06):
@Chris M I think that actually Lean is equiconsistent with ZFC + infinitely many universes, but mathematicians use universes when push comes to shove...
Last updated: Dec 20 2023 at 11:08 UTC