Radical predicativism

This isn't really on-topic for this blog, but I can't resist posting this: the Princeton mathematician Edward Nelson claims to have found an inconsistency in arithmetic! On the FOM mailing list, he posted:

I am writing up a proof that Peano arithmetic (P), and even a small fragment of primitive-recursive arithmetic (PRA), are inconsistent. This is posted as a Work in Progress at http://www.math.princeton.edu/~nelson/books.html

A short outline of the book is at:

http://www.math.princeton.edu/~nelson/papers/outline.pdf

The outline begins with a formalist critique of finitism, making the case that there are tacit infinitary assumptions underlying finitism. Then the outline describes how inconsistency will be proved. It concludes with remarks on how to do modern mathematics within a consistent theory.

There's some discussion of this at The n-Category Cafe, including a brief (so far) discussion between Terry Tao and Nelson himself. Obviously, I expect a flaw will be found in his proof -- but I sure hope he's right! That would mean all of mathematics will be in need of revision.

Update: Nelson says that Tao has indeed found a hole in the proof. Exponentiation remains total, for now.

The most surprising paper at ICFP

I was just at ICFP, which was very nice -- it was my first trip ever to Japan, and I found the people very friendly. (The cuisine, alas, is not so vegetarian-friendly, if you do not regard fish as a vegetable. But the people made up for it!) There were many excellent talks, but only one result which really shocked me:

Linearity and PCF: a semantic insight!, by Marco Gaboardi, Luca Paolini, and Mauro Piccolo.

Linearity is a multi-faceted and ubiquitous notion in the analysis and the development of programming language concepts. We study linearity in a denotational perspective by picking out programs that correspond to linear functions between coherence spaces.

We introduce a language, named SlPCF*, that increases the higher-order expressivity of a linear core of PCF by means of new operators related to exception handling and parallel evaluation. SlPCF* allows us to program all the finite elements of the model and, consequently, it entails a full abstraction result that makes the reasoning on the equivalence between programs simpler.

Denotational linearity provides also crucial information for the operational evaluation of programs. We formalize two evaluation machineries for the language. The first one is an abstract and concise operational semantics designed with the aim of explaining the new operators, and is based on an infinite-branching search of the evaluation space. The second one is more concrete and it prunes such a space, by exploiting the linear assumptions. This can also be regarded as a base for an implementation.

In this paper, the authors considered a really simple language based on coherence spaces, consisting of the flat coherence space of natural numbers and the linear function space. The nice thing about this model is that tokens of function spaces are just trees with natural numbers at the leaves, with branching determined by the parenthesization of the function type. This really shows off how concrete, simple, and easy-to-use coherence spaces are. Then they found the extension to PCF for which this model was fully abstract, as semanticists are prone to doing.

But: the additional operator and its semantics are really bizarre and ugly. I don't mean this as a criticism -- in fact it is exactly why I liked their paper so much! It implies that there are fundamental facts about linear types which we don't understand. I asked Marco Gaboardi about it after his talk, and he told me that he thinks the issue is that the properties of flat domains in coherence spaces are not well understood.

Anyway, this was a great paper, in a "heightening the contradictions" sort of way.