On Fri, Apr 3, 2015 at 8:44 AM, Keean Schupke <[email protected]> wrote: > On 3 April 2015 at 13:02, Keean Schupke <[email protected]> wrote: >> On 3 April 2015 at 12:21, Matt Oliveri <[email protected]> wrote: ... >>> > 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. > > > Also I would like to reference "Computational Trinitarianism": > > http://ncatlab.org/nlab/show/computational+trinitarianism > > Logic = Type Theory = Category Theory > > So if Category-theory does not depend on set-theory, and category theory = > type-theory, then type-theory does not depend on set-theory.
I agree that type theory does not depend on set theory. Here are some things you need to realize: - The "Type Theory" in that pseudocode equation is not specifically MLTT, but almost any sufficiently-pure type system. - The correspondence between type theory and category theory is not as tight as between type theory and logic. Constructive logic and type theory are basically the same field now, AFAICT, but type theory and category theory are still used as different, complementary techniques in some of the same situations. - The ability to interpret system X in system Y does not constitute a dependency of system X on system Y. There is no contradiction in MLTT having a set theoretic interpretation, and also not depending on set theory. Kind of like that Emacs can run on Windows, but doesn't depend on it. > In general so far every proof in mathematics exists by proving a mapping to > an already accepted theory. At the end of the chain we have natural > numbers/arithmetic, which Godel proved consistent using inuitionistic logic > and transfinite induction (Godel's T is a kind of intuitionistic logic). > > So indirecty, every proof maps to natural numbers, and we can define natural > numbers in type-theory, and type theory is equivalent to intuitionistic > logic. Your story is only partially right. The part that all math gets reduced to natural numbers isn't right. (Or at best, it's misleading.) Only the syntax is typically reduced to natural numbers. The semantics usually stops at set theory. Specifically ZFC, which is waaaaay stronger than Peano arithmetic. > So you can reduce the whole of mathematics to natural numbers (which we > cannot prove completeness/consistency of), or you can reduce the whole of > mathematics to intuitionistic logic (which we cannot prove the consistency > of in itself) + transfinite induction. These are actually both true, I think. But it's not at all what I thought you were proposing to do. You cannot do this using only Twelf's logic programming engine. And getting back to the original argument, this is nothing like "constructing everything from types", which you never managed to explain sensibly. > So my choice is to start from intuitionistic type theory and > transfinite-induction, and you can prove the consistency of peano arithmetic > in such a system. Hold on there, you didn't say anything about transfinite induction until this email I'm replying to. Twelf doesn't provide transfinite induction. And intuitionistic type theory is MLTT, which wasn't invented yet when Gödel proved things, so I'm not sure you mean that. MLTT would be a pretty good starting point for formalizing math. But you've been talking about Twelf, which is different. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
