On 3 April 2015 at 18:36, Matt Oliveri <[email protected]> wrote: > > Well it sounds like this set theory has the _same_ strength as Peano > arithmetic, so you couldn't prove it consistent _in_ Peano arithmetic. > But that's a technicality. This is actually kind of interesting. Do > you know if this set theory is actually pleasant to use? >
Well, you cannot prove set theory consistent by mapping it to Peano arithmetic. As they are equivalent you cannot prove Peano arithmetic in set theory, nor set theory in Peano arithmetic. Until Godel's "T", we just assumed that natural arithemtic was intuitively complete and consistent. Anyway, Twelf's logic programming engine is weaker than Peano > arithmetic. So using only that is still doomed. But I now realize I'm > pointing out the wrong weakness: LF doesn't have negation. > > >> It's not. To be more specific, Vladimir Voevodsky wants to use ZFC to > >> prove the consistency of HoTT using his Kan simplicial set model. None > >> of the others have called for set theory specifically, but they are > >> depending on it implicitly until they develop a model in some other > >> system. While the models use category theory, and category theorists > >> claim that proper developments in category theory do not depend on set > >> theory, I don't think anyone has actually checked that all the > >> necessary machinery can be developed in any other system. > >> (Realistically, it probably can be, possibly with minor > >> modifications.) > > > > I don't think this is the right approach. > > Be more specific. I said I lot, and I don't know what you're referring to. > You can prove set theory in type-theory + transfinite induction. (Godel's "T"). >> More importantly, the intended way to use HoTT is *absolutely not* to > >> just bootstrap up to set theory. If anything, it should be the other > >> way around. > > > > I think we disagree here. > > It's odd to disagree about other people's stated intents. Why don't > you pop over there and ask them how they intend to use set theory? > Sorry, I didn't mean it that way. I want to bootstrap mathematics from type-theory + transfinite induction. I shouldn't speak for anyone else (although I am sure I am not the only person to have the idea, although it would be great to come up with something original). > > >> > Set theory can be defined within the proof-relevant world of type > >> > theory, but > >> > not the other way around (you cannot recover proof relevance from > proof > >> > irrelevance). > >> > >> Wrong again. Just interpret proof-relevant propositions as sets of > >> proof objects. Piece of cake > > > > Prof. Bob Harper would disagree here, unless he has changed his mind, and > > can probably make the point better than I can. > > I suspect that you've misinterpreted him. Set theory was the original > interpretation of MLTT. It's the no-brainer interpretation. The > symbols for the MLTT type constructors are even the same as for the > corresponding set theoretic constructions. (Well, W types were new, I > think.) Well, its caught on camera in his video lecture series on HoTT. He literally says that you cannot recover proof relevance from proof irrelevance and makes a big deal about it. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
