Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

September 12, 2011

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.

Posted at September 12, 2011 9:17 AM UTC

TrackBack URL for this Entry:

8 Comments & 0 Trackbacks

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.

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.

Posted by: Roger Witte on September 12, 2011 10:31 AM | Permalink | Reply to this

Re: Voevodsky on FOM

Thanks for sharing. I’m not familiar with Gentzen’s work. Does someone know enough about this to summarize? In particular, I’m confused about what is meant by “meta” in the following discussion (from the third blog post):

all the currently available proofs of the consistency of PA in fact rely on the very claim they prove, namely the consistency of PA, on the meta-level. (S. Awodey adds that it is a consequence of Gödel’s results that all proofs of consistency of PA must use methods that are stronger than PA in the meta-language.) So if PA was inconsistent, these proofs would still go through; in other words, there is a sense in which such proofs are circular in that they presuppose the very fact that they seek to prove. I raised a similar point before in comments here: if PA was unsound (which it would be if it were inconsistent), it might be able prove its consistency even if it is actually inconsistent (which also means that Hilbert’s original goal may have had a suspicious circular component all along). Now, we know by Gödel that PA cannot prove its own consistency, but the proofs of the consistency of PA available all seem to presuppose the consistency of PA (on the meta-level), so it boils down to roughly the same situation of epistemic uncertainty.

Posted by: Emily Riehl on September 12, 2011 5:31 PM | Permalink | Reply to this

Re: Voevodsky on FOM

Most of the time when discussing propositions or giving arguments, we give those arguments in some natural language like English. For example, “If n is even, then n is divisible by 2”. However, other times we give arguments in some formal language like first-order predicate calculus. For example, “even(n)2|neven(n) \Rightarrow 2\vert n”. But when we’re using a formal language, how do we know what that language means? What are the semantics of that language’s syntax?

A number of philosophers have wrangled with this question, Tarski most famously. But the end result (so far) is that, given a language L (e.g., PA or FOL), in order to talk about what sentences of L mean we must use another language M (e.g., English), which we assume we already know the meaning of. The language L that we are talking about is called the “object language”, and the language M that we are talking in (when we are talking about L) is called the “meta-language”.

Posted by: wren ng thornton on September 12, 2011 6:08 PM | Permalink | Reply to this

Re: Voevodsky on FOM

PA is a formal language in which we can prove statements (e.g., about natural numbers), but of course we can also prove things in the informal ‘meta’-language of regular mathematics (e.g., about PA itself). Godel’s proof works because he is able to code statements about PA like ‘PA proves p’ or ‘PA is consistent’ in PA itself. In this sense, PA can be a meta-language for itself (but as such cannot prove its own consistency).

It is possible to prove the consistency of PA in other meta-languages (in ZFC which is strictly stronger, and in Gentzen’s system which is incomparable). But then we must know that the meta-languages are themselves consistent since otherwise they would prove both the consistency and inconsistency of PA.

(On a sidenote, I’d rather use the term theory than language.)

Posted by: Paige North on September 13, 2011 6:25 AM | Permalink | Reply to this

Re: Voevodsky on FOM

One should say that Gentzen’s proof works over PRA (primitive recursive arithmetic) plus quantifier-free induction up to ϵ 0\epsilon_0 (the smallest fixed point of exponentiation). This theory is incomparable in strength to PA. I think that PRA alone is weaker than PA (it doesn’t have arbitrary induction), and Wikipedia says it is considered finitist.

Posted by: David Roberts on September 13, 2011 7:07 AM | Permalink | Reply to this

Re: Voevodsky on FOM

I understand this as being the sense: suppose we prove Con(PA). This proof itself must take place (in principle) in some theory T; since we’re using T to reason about PA, we call T the meta-theory.

Anyhow: we’ve proven Con(PA), from T. But this would be pointlessly trivial if T was inconsistent — it’s only a meaningful result if we believe T is consistent. So in terms of strengthening our confidence in PA, as a foundational system, our proof is only helpful if we believe T is more obviously secure. So we can say: “our proof of the consistency of PA presupposes the consistency of T, on the meta-level”.

Now, as I understand it, the line

proofs of the consistency of PA available all seem to presuppose the consistency of PA (on the meta-level)

is a slight overstatement, since the theory T is not always an extension of PA (Gentzen’s original proof is a case where it isn’t). At least the ones I’ve seen, though, all presuppose the consistency of something that’s no more self-evidently secure than PA — although that’s a pretty subjective criterion, of course.

Posted by: Peter LeFanu Lumsdaine on September 13, 2011 7:22 AM | Permalink | Reply to this

Re: Voevodsky on FOM

Jim Dolan gave a nice interpretation of ϵ 0\epsilon_0 in this comment, as the decategorification of the free cartesian closed category on one object.

ϵ 0\epsilon_0 can also be seen as the well-ordered set of finite rooted trees. Trees are such nice combinatorial objects (I should mention WW-types here), so it is natural to suppose this is even constructively trues.

Posted by: David Roberts on September 13, 2011 7:44 AM | Permalink | Reply to this

Re: Voevodsky on FOM

David, thanks so much for linking my posts, the stats over at M-Phi have gone through the roof in the last two days :)

But let me just clarify that M-Phi is not ‘my’ blog, it’s a group blog with many contributors (some not as frequent as others…). At any rate, we would love to have readers of The n-category cafe’ coming over :)

Posted by: Catarina Dutilh Novaes on September 13, 2011 4:36 PM | Permalink | Reply to this

Post a New Comment