On Sun, 28 Oct 2012 07:31:24 +0000 (UTC), "Peter Webb" <webbfamilyDIEspamDie@optusnet.com.au> wrote:
>> I suppose at worst it could be made an optional axiom, or some >> statement of principle could be added as an additional axiom to allow >> it to be true. >> >> J. > >Its a theorem in ZF. It doesn't need an axiom.
It seems a little involved to be the kind of thing we like to call a theorem, and I believe it was Poincare who said it (or was he just broad-brushing all of Cantor?) only works by assuming its conclusion. What would it take to make Poincare happy with this one particular theorem?
I think there may be another line of criticisms that the diagonal argument asserts certain properties to the two-dimensional lists of numbers on which it draws diagonals, that cannot really be assumed so freely.
This is separate from what may still be true about ZFC and CH, after all Cantor started without the diagonal argument and maybe he was better off that way after all.
But in answer to my question, so far nobody has pointed out the kind of formalized treatments of these objections, fwiw.