In article <email@example.com>, firstname.lastname@example.org 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.
There is no such theorem in ZF, or any other set theory in which no form of that axiom of choice is assumed. > > Another formla proof proves the existence of uncountably many real numbers.
If one defines real numbers as LUBs or limits, as usual, then there are provably more of them than one can find individual definitions for from any merely countable set of definitions.
> Alas, they do not exist in mathematics.
They have long since existed in mathematics, and will continue to do so in mathematics, everywhere outside of WM's wild weird world of WMytheology, which is increasingly putting itself totally outside of mathematics.. --