There are 3 recent things that I’d very much like to work on and digest in the next year or so:

– Edward Nelson’s ongoing work (summary here), where he claims he found an inconsistency in Peano Arithmetic (namelly that there are superexponential recursions which do not terminate) , and proposes another weaker system as a foundation for elaborated mathematics, together with a new proof checker program which outputs human-readable proofs ; [**Update sept 28**: there might well be a flaw in Nelson’s proof, since in comments elsewhere both Terry Tao and David Madore have independently questioned the same part of the argument… **Update sept 29**: looks like a more detailed discussion between Terry Tao and Edward Nelson is taking place at the n-Category CafĂ©]

– the ongoing project started by Voevodsky, Awodey and Coquand on a new foundation for mathematics based on homotopy theory, called Univalent Type Theory (the website contains lots of things, an IAS program is also planned in 2012-2013) ;

– Jean-Yves Girard’s latest paper (in french) very much the culmination of decades of his deep work on “la syntaxe transcendantale” (started long ago with linear logic , and eventually dealing recently with subject/object distinction and normativity).

### Like this:

Like Loading...

*Related*

This entry was posted on September 27, 2011 at 10:11 pm and is filed under mathematics. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

## Leave a Reply