On Saturday, May 3, 2014 3:04:33 AM UTC-4, muec...@rz.fh-augsburg.de wrote: > On Friday, 2 May 2014 22:32:14 UTC+2, Dan Christensen wrote:
> > No. That is the nature of formal proof. If you have a formal proof, you know exactly what rules, axioms and assumptions were used. > > > > And you can guess, most times, that the result is useless. For example there exists a formal proof that ever set can be well-ordered, but it is impossible to do so. This shows that this formal proof is rubbish. >
Not at all. The great thing about formal proofs is that, unlike your frantic hand-waving exercises here, every one of a formal proof's assumptions and rules of inference have been made explicit. There are no references to what "every 6-year-old knows," etc. (Actually, one of WM's favourite arguments!) So, if you take exception to the end result, you only have to go back to your assumptions and rules inference.
If, as in your example, you object to the well-ordering theorem, your should probably go back the axioms of set theory that are cited and explain why one of them might be invalid. So, which one is it, WM?