On 3 April 2015 at 19:30, Matt Oliveri <[email protected]> wrote: > > > 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.
I just used Twelf as an example to illustrate a particular point. I was using LF as an abbreviation for logical-framework. Referencing prof. Harper again, Godel's "T" was a in effect an intuitionistic type system, but Godel could not have realised that because, as you say MLTT hadn't been formulated. Retrospectively we can recognise what "T" is, and we can then trace the story back futher than MLTT. It also allows us to bring Godel's work into the context of Type Theory. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
