3 recent themes in logic

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).


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: