On proofs and more

This is a transcript of an exchange on Twitter on what mathematicians and others expect from proofs. (A previous exchange on a different topic is here. Twitter produces surprisingly nice results sometimes. What follows is a bit meandering, but interesting points are made.)

It began at 7:56 am – 27 Jun 13, with the twitter account of Republic of Mathematics (a website started by Gary Davis) quoting from Bill Thurston‘s great essay On proof and progress in mathematics. The quoted sentence was a short excerpt from the following:

The question is not even “How do mathematicians make progress in mathematics?”
Rather, as a more explicit (and leading) form of the question, I prefer “How do mathematicians advance human understanding of mathematics?”
This question brings to the fore something that is fundamental and pervasive: that what we are doing is finding ways for people to understand and think about mathematics.

To this, the account of The True Beauty of Math replied with “[Which is] why computer proofs [are of] little use.” Republic of Mathematics objected to this position, and quoted from an article by Sara Billey titled Computer Proofs. What is the value of computer assisted proofs?. The quoted sentence is an excerpt from:

Some mathematicians have tried to protect their egos by proposing that human proofs are superior to computer assisted proofs. They claim that we don’t learn as much from computer assisted proofs as we do from a human proof. They claim computer proofs can be difficult to verify. They claim computer proofs are less elegant. I find these complaints to be naive.

This was retweeted by Guy Longsworth, which is how I saw it.

Advertisement

Woodin’s proof of the second incompleteness theorem for set theory

[Edit, Oct. 1, 2013: Robert Solovay has pointed out an inaccuracy in my presentation of Woodin’s argument: Rather than simply requiring that is a hereditary property of models, we must require that proves this. A corrected presentation of the argument will be posted shortly.]

As part of the University of Florida Special Year in Logic, I attended a conference at Gainesville on March 5–9, 2007, on Singular Cardinal Combinatorics and Inner Model Theory. Over lunch, Hugh Woodin mentioned a nice argument that quickly gives a proof of the second incompleteness theorem for set theory, and somewhat more. I present this argument here.

The proof is similar to that in Thomas Jech, On Gödel’s second incompleteness theorem, Proceedings of the American Mathematical Society 121 (1) (1994), 311-313. However, it is semantic in nature: Consistency is expressed in terms of the existence of models. In particular, we do not need to present a proof system to make sense of the result. Of course, thanks to the completeness theorem, if consistency is first introduced syntactically, we can still make use of the semantic approach.

Woodin’s proof follows.

502 – The constructible universe

In this set of notes I want to sketch Gödel’s proof that is consistent with the other axioms of set theory. Gödel’s argument goes well beyond this result; his identification of the class of constructible sets eventually led to the development of inner model theory, one of the main areas of active research within set theory nowadays.

A good additional reference for the material in these notes is Constructibility by Keith Devlin.

1. Definability

The idea behind the constructible universe is to only allow those sets that one must necessarily include. In effect, we are trying to find the smallest possible transitive class model of set theory.

is defined as

where for limit, and where

The first question that comes to mind is whether this definition even makes sense. In order to formalize this, we need to begin by coding a bit of logic inside set theory. The recursive constructions that we did at the beginning of the term now prove useful.

580 -Some choiceless results (3)

[Updated December 3. The previous proof that there is a canonical bijection for all infinite ordinals was seriously flawed. Thanks to Lorenzo Traldi for pointing out the problem.]

5. Specker’s lemma.

This result comes from Ernst Specker, Verallgemeinerte Kontinuumshypothese und Auswahlaxiom, Archiv der Mathematik 5 (1954), 332-337. I follow Akihiro Kanamori, David Pincus, Does GCH imply AC locally?, in Paul Erdős and his mathematics, II (Budapest, 1999), Bolyai Soc. Math. Stud., 11, János Bolyai Math. Soc., Budapest, (2002), 413-426 in the presentation of this and the following result. The Kanamori-Pincus paper, to which we will return next lecture, has several interesting problems, results, and historical remarks, and I recommend it. It can be found here.