On Fri, Apr 3, 2015 at 8:02 AM, Keean Schupke <[email protected]> wrote: > On 3 April 2015 at 12:21, Matt Oliveri <[email protected]> wrote: ... >> > Starting with universes, we can clearly define natural numbers and >> > arithmetic, using nothing but intuitionistic logic. As we can define all >> > of >> > mathematics using set theory from the natural numbers (ie the >> > correctness of >> > set theory us proved by mapping to natural numbers), and we can define >> > these >> > from intuitionistic logic, we have a simple axiomatic system for all >> > mathematics. >> >> You are completely ignoring the issue of consistency. Yes, you can >> model sets as natural numbers, but using which theory of naturals? Not >> Peano arithmetic. And certainly not Twelf's logic programming engine. > > Yes, Peano arithmetic: > > http://web.mat.bham.ac.uk/R.W.Kaye/publ/papers/finitesettheory/finitesettheory.pdf
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? 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. >> 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? >> > 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.) _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
