Zulip Chat Archive
Stream: general
Topic: induction recursion?
Max New (Apr 25 2018 at 19:58):
Does lean support inductiverecursive definitions?
Mario Carneiro (Apr 26 2018 at 02:52):
No. You can simulate a reasonably broad subclass of inductiverecursive definitions, but general inductionrecursion proves lean's consistency.
Sean Leather (Apr 26 2018 at 06:42):
general inductionrecursion proves lean's consistency.
?
Mario Carneiro (Apr 26 2018 at 07:00):
You can construct the valid contexts and well typed terms in that context by inductionrecursion. Then you can prove any lean term has a denotation by induction
Sean Leather (Apr 26 2018 at 07:08):
What do you mean by “proving the consistency of Lean”?
Mario Carneiro (Apr 26 2018 at 07:10):
I mean you can encode lean inside lean and prove of that objectlean that it can't prove false
Mario Carneiro (Apr 26 2018 at 07:10):
i.e. exactly the thing Godel says is impossible
Kevin Buzzard (Apr 26 2018 at 07:29):
...unless Lean is inconsistent ;)
Reid Barton (Apr 28 2018 at 17:27):
Is the following a definition by inductionrecursion?

An $(n+1)$dimensional CW complex $X_{n+1}$ consists of the data of
 an $n$dimensional CW complex $X_n$,
 a set $C_{n+1}$ of "$(n+1)$dimensional cells", and
 for each $i \in C_{n+1}$, an "attaching" map $e_i$ from $S^n$ to the underlying topological space of $X_n$.

The underlying topological space of $X_{n+1}$ is obtained from that of $X_n$ by attaching a copy of $D^{n+1}$ along the attaching map of each cell.
Kenny Lau (Apr 28 2018 at 17:31):
aha!
Kenny Lau (Apr 28 2018 at 17:31):
I formalized CW complex a while ago lol
Kenny Lau (Apr 28 2018 at 17:31):
https://math.stackexchange.com/a/2712786/328173
Kenny Lau (Apr 28 2018 at 17:31):
a month ago
Kenny Lau (Apr 28 2018 at 17:32):
Isn't it just an inductive type?
Reid Barton (Apr 28 2018 at 17:34):
The last field (the attaching maps) involves the function "underlying topological space" which (it seems to me) you need to define simultaneously with the inductive type
Reid Barton (Apr 28 2018 at 17:34):
If you could define an infinite alternating list of inductive types and functions, it would be one of those.
Reid Barton (Apr 28 2018 at 17:34):
I haven't tried actually writing it out in lean though.
Kenny Lau (Apr 28 2018 at 17:35):
you don't need to know that X_n is a topological space, I think?
Reid Barton (Apr 28 2018 at 17:35):
Well I omitted the word, but it has to be a continuous map
Reid Barton (Apr 28 2018 at 17:35):
The attaching maps
Kenny Lau (Apr 28 2018 at 17:35):
oh right
Kenny Lau (Apr 28 2018 at 17:36):
there might be other approaches, but I have an ugly approach in mind
Kenny Lau (Apr 28 2018 at 17:36):
define the sigma type inductively
Kenny Lau (Apr 28 2018 at 17:36):
(not sure if it works, after I say it)
Reid Barton (Apr 28 2018 at 17:39):
(I had some idea of how to formalize this in lean, but I'm curious to hear others, and also I didn't write down my idea and I think it was kind of ugly.)
Reid Barton (Apr 28 2018 at 18:03):
I'd also appreciate a type theory expert confirming whether or not this is an example of inductionrecursion at all, since inductionrecursion is an unfamiliar thing and the typical examples are even more unfamiliar things, while CW complexes are something that all mathematicians learn about.
Last updated: Aug 03 2023 at 10:10 UTC