[FOM] "Salvaging" Voevodsky's talk
hendrik at topoi.pooq.com
Sat Jun 4 21:28:25 EDT 2011
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?
More information about the FOM