## Stream: general

### Topic: induction recursion?

#### Max New (Apr 25 2018 at 19:58):

Does lean support inductive-recursive definitions?

#### Mario Carneiro (Apr 26 2018 at 02:52):

No. You can simulate a reasonably broad subclass of inductive-recursive definitions, but general induction-recursion proves lean's consistency.

#### Sean Leather (Apr 26 2018 at 06:42):

general induction-recursion 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 induction-recursion. 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 object-lean 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 induction-recursion?

• 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.

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

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

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 induction-recursion at all, since induction-recursion 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: Dec 20 2023 at 11:08 UTC