### Voevodsky on FOM

#### Posted by David Corfield

I’m just back from the Belgian city of Ghent, where I heard from Catarina Dutilh Novaes that earlier this year there was quite a storm on the FOM (Foundations of Mathematics) mailing list over comments by Voevodsky suggesting that he didn’t understand Gödel’s incompleteness results. I gave up reading FOM several years ago after the tone of the attacks on my friend Colin McLarty, who was defending category theoretic foundations, reached a particular low. I hear that generally it’s a friendlier place now.

You can read about the Voevodsky case at Caterina’s blog – M-Phi – here and the two follow-up posts. She sums up in the third of these posts:

So it would seem that the main conclusion to be drawn from these debates, and as pointed out by Steve Awodey in one of his messages to FOM, is that the consistency of PA is really a minor, secondary issue within a much broader and much more ambitious new approach to the foundations of mathematics.

Yes, better to spend your time learning about Univalent Foundations, I’m sure. And a very good place to start is Mike Shulman’s series of six posts on *Homotopy Type Theory* listed here.

## Re: Voevodsky on FOM

Well Caterina’s blog certainly looks like some worthwhile reading, so thanks for the reference.

Actually the argument seems to be one in favour of paraconsistent or relevant foundations so that should an inconsistency be discovered in one area, it doesn’t infect the entirety of mathematics.

http://en.wikipedia.org/wiki/Paraconsistent_logic

http://en.wikipedia.org/wiki/Relevance_logic

In this case type theory provides the insulation: if one type proves inconsistent, arguments not involving that type nor any types dependant on it, should still be safe.