On Saturday, 3 May 2014 18:54:54 UTC+2, Dan Christensen wrote: > 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 every one of a formal proof's assumptions and rules of inference have been made explicit.
Wrong. Where is it made explicit, for instance, that everything has to be made explicit? Nowhere! So, why do you think that everything should be made explicit?
> There are no references to what "every 6-year-old knows,
Where is it made explicit that everything has to be made explicit?
> 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?
I know it. But if you want to make a formal search then it's enough to know that the result is wrong and look for remedy by excluding an axiom after the other until the results are no longer wrong.
That the result is wrong is proven by the fact that udefinable elements cannot be well-ordered.