Dear Paul, a short reply to your mail about inconsistency of replacement. As Paul has already remarked in his mail the type-theoretic counterpart of replacement is that of universe `a la Martin-Loef. As in case of replacement the use of universes is that they allow for construction of families of types (as e.g. needed for inverse limit constructions in Domain Theory which cannot be performed in pure topos logic precisely for this reason). But as already observed in a survey article by Thierry Coquand (ftp://ftp.cs.chalmers.se/users/cs/coquand/meta.ps.Z) and, surely, known to Martin-Loef himself it holds that in type theory with n+1 universes one may prove the consistency of type theory with n universes simply by constructing a model using the n+1st universe. But, of course, this extra universe is needed for the consistency proof. Accordingly, one cannot prove the consistency of type theory with $\omega$ universes without postulating an $\omega$th universe. Quite the same phenomenon is going on in set theory as already pointed out by some previous replies. However, in set theory due to the presence of ``impredicative'' axioms the proof theoretic strength is incredibly stronger than set of Martin-Laoef type theory with $\omega4 universes. Best, Thomas
Using an old logician's trick (see eg Feferman on paths thru O, or even Goedel's original papers) as an April Fool joke may be amusing to some within the closed gates of a British University, but is irresponsible on the world network. Think of the hundreds of lurkers (who hesitate to speak up so that misconceptions can be discussed and clarified openly, but) who are now furthering the rumor that mathematics has somehow been proved inconsistent.The waves of such disinformation can last for years or even decades. ******************************************************************************* F. William Lawvere Mathematics Dept. SUNY wlawvere@acsu.buffalo.edu 106 Diefendorf Hall 716-829-2144 ext. 117 Buffalo, N.Y. 14214, USA *******************************************************************************
On Tue, 6 Apr 1999, F W Lawvere wrote:
Using an old logician's trick (see eg Feferman on paths thru O, or even Goedel's original papers) as an April Fool joke may be amusing to some within the closed gates of a British University, but is irresponsible on the world network. Think of the hundreds of lurkers (who hesitate to speak up so that misconceptions can be discussed and clarified openly, but) who are now furthering the rumor that mathematics has somehow been proved inconsistent.The waves of such disinformation can last for years or even decades.
Curiously, my reaction to this has been rather different. We were discussing Paul's note after the seminar here the other day, and apart from one reply, I rather had the idea that most replies were aware that this was a joke, but that it was a subtle one (not all that subtle, perhaps, but a lot more subtle that what often passes as humour on the net, for sure). And that finding the error was a respectable response. As for spreading disinformation, there has been no shortage of people who look serious, (I avoid the harder question as to whether they are, and what exactly that ought to mean) and who have been spreading tales of the inconsistency of maths for decades. As a graduate student, I often attended logic meetings where Edward Wette proved ever more basic fragments of our subject inconsistent (I recall he got as far as propositional logic, Peano arithmetic, and several branches of physics. I am not sure he made any serious distinction between the last case and the others.) Perhaps one point here is that anyone who believes all he reads is a fool, and anyone who believes all he reads on the net is a fool who cannot even learn from experience. (It takes about 5 minutes to uncover patently silly things on the net! - not even counting this one...) So - I agree Bill raises a serious matter, but I think in this case it may be an overreaction. Paul's note was certainly "fishy" (French reference for those not in a French environment), but it was essentially harmless. This group is comparitively closed (even your average academic journal is probably more open). And if anyone missed the joke up to now, surely that has been remedied. (If only in that refutations appeared quickly.) However, if I see a report on this on "60 minutes" I will eat my hat... - all the best, Robert = rags = ================================= <rags@math.mcgill.ca> <http://www.math.mcgill.ca/~rags>
As a lurker who failed to either notice the date or understand any detail of Paul's demonstration, I appreciate Lawvere's comments. I do feel, though, that he is overstating the impact of Paul's little jest. There were several immediate replies (to the effect, I think, that F(lim X) is not lim F X), and no riposte from Paul. My own reaction was: hmm, it'll be interesting if anything else comes out of this. I sympathise very much with Paul's "anti-ZF" stance; after all, hasn't Lawvere set the basis for a non-set foundation of practical mathematics? -----Original Message----- From: cat-dist@mta.ca [mailto:cat-dist@mta.ca]On Behalf Of F W Lawvere Sent: 06 April 1999 22:41 To: CATEGORIES@mta.ca Subject: categories: Re: incompleteness of ZF Using an old logician's trick (see eg Feferman on paths thru O, or even Goedel's original papers) as an April Fool joke may be amusing to some within the closed gates of a British University, but is irresponsible on the world network. Think of the hundreds of lurkers (who hesitate to speak up so that misconceptions can be discussed and clarified openly, but) who are now furthering the rumor that mathematics has somehow been proved inconsistent.The waves of such disinformation can last for years or even decades. ************************************************************************ ******* F. William Lawvere Mathematics Dept. SUNY wlawvere@acsu.buffalo.edu 106 Diefendorf Hall 716-829-2144 ext. 117 Buffalo, N.Y. 14214, USA ************************************************************************ *******
[Note from Moderator: With the posts just sent, this discussion should come to a close. Readers of the list, and those posting to it, should be aware that it contains about 500 addresses.] *Had* Paul posted his clever hoax on, say, sci.math (which, AFAIK, he did not) where it would be widely available to J. Random Lurker, I would share Bill Lawvere's concerns. Had he placed it permanently on his web server, with a big flashing link from his home page, advertised it by spamming 100,000 random netizens, and issued a trilingual press release, I would share those concerns to a much greater extent. However, CATEGORIES is a mailing list; probably everybody who received Paul's posting also received the two debunkings, Bill's comment, and is reading this even as, er, they read this. I don't imagine that we *have* hundreds of lurkers. (Lurkers! Please identify yourselves... I'm curious.) While Bill is undoubtedly correct that not all readers of CATEGORIES share his ability to look at Paul's joke and instantly recognize not only the fallacy but its antecedents [I offer myself as a proof of the nonemptiness of the complement], surely we all have been around the block enough times to distinguish between a full formal proof and what Paul presented? Even had it been in earnest, such an announcement would justify only the reaction "Somebody thinks he's shown ... but I don't think he has circulated a complete proof yet." I suppose that it is possible that somebody, browsing at random, *might* find it in the CATEGORIES archives, in years to come, and not read ahead to find out what the world had had to say about this discovery back in the mad, exciting days of the late C20. But anybody who could do this and not realize that there was something odd going on would probably either (a) not understand why anybody should care if ZF is consistent or not, or (b) have a vague feeling that Goedel, or Escher, or somebody, already proved that, or something, didn't he? -Robert Dawson
participants (5)
-
F W Lawvere -
Michael Abbott -
R.A.G. Seely -
Robert Dawson -
Thomas Streicher