NCM 09 (part 2)

... and the postponed report on Non-Classical Mathematics 2009 continues...

The second talk was given by Giovanni Sambin. He talked about his minimalist foundation and about a way constructive topology can be developed over a minimalist foundation. It's quite interesting to see how much stuff can be done constructively. Also, Giovanni is a devoted and areally charming constructivist. I was chatting with him at a pub one night and only by finding myself almost converted to constructivism I knew it was time to go home.

By the way, among many inaccurate things that are being said about Godel's theorem (like these) you can find a remark that Godel's incompleteness and undefinability proofs/theorems don't work in intuitionistic mathematics. Actually, they do. And the person to talk to is Giovanni, who worked out all the details making sure everything is constructive.

Arnon Avron talked about a new approach to Predicative Set Theory. Roughly,the underlying principles of the predicative mathematics are:

I. Higher-order constructs are acceptable only when introduced through non-circular definitions referring only to constructs introduced by previous definitions.

II. The natural number sequence is a well understood concept and as a totality it constitutes a set.

It is well known that Feferman has pursued the project and has shown how a large part of classical analysis can be developed within it. The system, however, is not too popular, partially because it uses a rather complex hierarchy of types, which makes the theory more complicated than, say, ZFC.

Arnon Avron discussed an attempt to simplify predicative mathematics by getting rid of the type hierarchy and developing a type-free predicative set theory. The idea is that the comprehension schema is restricted to those formulas that satisfy a syntactically defined safety relation between formulas and variables. The relation resembles a syntactic approximation to the notion of domain-independence used in database theory, and the intuition is that acceptable formulas define a concept in an acceptable way independent of any extension of the universe.