[FOM] "Salvaging" Voevodsky's talk

[Hendrik Boom]

On Sat, Jun 04, 2011 at 06:51:22PM -0400, Timothy Y. Chow wrote:
> 
> The last part of his lecture argues that constructive type theory is a 
> better approach to foundations than traditional approaches are, because it 
> is more robust to possible contradictions.

Voevodsky is willing to trust constructive type theory, but not PA.  Now 
it's trivial to formulate natural numbers in type theory, and you even 
get induction. Is there some essential difference between this induction 
and the induction in PA?  Does it perhaps lie in the predicates you have 
available to do induction with?

-- hendrik