inductive types = set theory?

Stream: new members

[Huỳnh Trần Khanh]

why are inductive types equivalent to set theory? they look different, how can they be equivalent

[Huỳnh Trần Khanh]

like set theory is all about awkward encoding of ordinary mathematical objects and inductive types are more natural

[Mario Carneiro]

That sounds like you read it somewhere?

[Ken Lee]

Huỳnh Trần Khanh said:

why are inductive types equivalent to set theory? they look different, how can they be equivalent

source? I did hear in a talk by Voevodsky that you can see a set as a tree that's determined by its branches (set extensionality).

[Mario Carneiro]

I would not say that inductive types are like set theory at all. They are quite different approaches. Inductive types postulate (at great complication) the existence of initial algebras to a certain class of strictly positive type equations (narrowly avoiding the known inconsistencies in the area), while set theory is about using a simple axiom system and building everything you need by encoding. To me, the fact that they are roughly equivalent in consistency strength speaks well for the set theoretic approach, because it is easier to justify.

In ZFC you have to prove that an algebraic equation has a solution before you can start using the smallest one. In CIC they just... exist, for no clear reason. They don't have definitions or an encoding to consult to see why they should exist. Personally I think the "naturalness" is an illusion. It would sure be nice if they exist but I can say the same thing about the liar sentence or the set of all sets (or the category of categories, for that matter). Having a reasonable way to work with the object doesn't mean it is actually reasonable to assume its existence

[Huỳnh Trần Khanh]

Heh, yes, the inductive keyword gives you a new way of adding constants and axioms to the system :-) But this is a rather more controlled approach than the constant one! In particular, didn't some kid prove that it was equiconsistent with set theory at some point?

Ah, "equiconsistent", not "equivalent". What does "equiconsistent" mean then and what does that proof look like?

[Mario Carneiro]

The "some kid" referred to in that quote is me, and the proof is https://github.com/digama0/lean-type-theory/releases/tag/v1.0

[Mario Carneiro]

What I proved is that Lean's axiomatic system is equiconsistent with ZFC + {there are n inaccessible cardinals | n < omega}

[Mario Carneiro]

And what that means is that the consistency of either of these systems implies the consistency of the other

[Mario Carneiro]

that is, if lean can prove false, then there is some n such that ZFC + "there are n inaccessible cardinals" can also prove false

[Mario Carneiro]

Less formally, given two equiconsistent theories, it's not philosophically coherent to doubt one more than the other

[Huỳnh Trần Khanh]

Why couldn't you just prove that Lean's foundation is consistent? Is it because of some arcane technical difficulty that I don't know of?

[Mario Carneiro]

The issue with consistency proofs is that they always beg the question, consistent relative to what assumptions?

[Kevin Buzzard]

Huỳnh Trần Khanh said:

Why couldn't you just prove that Lean's foundation is consistent? Is it because of some arcane technical difficulty that I don't know of?

Go read Goedel :-) That tells you you can't prove it in Lean (unless it's inconsistent)

[Mario Carneiro]

https://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems

[Mario Carneiro]

Consistency strength is a way to put all formal theories on a single scale. Since Lean is able to construct a model of ZFC (see set_theory.zfc), we know that lean is strictly stronger than ZFC in consistency strength, and the theorem I proved shows just how much stronger it is (not by much, since inaccessible cardinals are one of the weaker large cardinal assumptions to make)

[Mario Carneiro]

But knowing that it's on the scale at all is good news. The real headliner when the proof came out was "lean can't prove false"