Zulip Chat Archive

Stream: new members

Topic: why do inductive functions have to return prop


Huỳnh Trần Khanh (May 29 2021 at 08:20):

they can't return anything else, can they? i guess inductive functions are used to define deduction rules for a particular system, e.g. the MIU system (derivable predicate) or the data.list.perm predicate

Horatiu Cheval (May 29 2021 at 08:28):

You can give inductive definitions into any sort. So, Prop, Type 0, Type 1 and so on. There is nothing restricting them to Prop.
For example docs#nat, the definition of natural numbers lives in Type.

Horatiu Cheval (May 29 2021 at 08:30):

I wouldn't say that you "inductively define functions" but rather that you "inductively define types". Propositions are a particular example of types so the Prop case falls into this. In some cases people refer to inductively defined propositions as "inductive predicates" but it's really the same notion.

Horatiu Cheval (May 29 2021 at 08:30):

What is MIU?

Huỳnh Trần Khanh (May 29 2021 at 08:30):

https://github.com/leanprover-community/mathlib/tree/master/archive/miu_language

Eric Rodriguez (May 29 2021 at 08:30):

structures and classes are essentially inductive functions with syntax sugar

Eric Rodriguez (May 29 2021 at 08:30):

MIU is the formal system used in Gödel Escher Bach @Horatiu Cheval

Horatiu Cheval (May 29 2021 at 08:32):

And it's indeed a good way of thinking them as rules of deduction, or as rules of constructions. inductive basically says "everything that can be constructed, or derived if you prefer, from these rules and these rules only"

Eric Wieser (May 29 2021 at 08:40):

"inductive functions" isn't the normal terminology for the inductive keyword in lean, is it?

Kevin Buzzard (May 29 2021 at 08:47):

(deleted)

Horatiu Cheval (May 29 2021 at 08:53):

Right, it's "inductive type" and the like, predicate, family etc. Inductive function would be misleading in my opinion since functions are not something inductive.


Last updated: Dec 20 2023 at 11:08 UTC