User talk:Abcxyz/Sandbox/Real Numbers/Real Addition is Closed
Regarding $1/2$
If we're building the reals from the rationals, we probably want to have made some basic definitions within and proved some basic properties about the rationals first, such as the fact that there is a rational $2>0$, and thus a rational $1/2 > 0$, and that $1/2 + 1/2 = 1$. Can't we factor such basic facts about the rationals out of this proof about the reals? Or are you trying to improve efficiency by holding off on all such until the reals are constructed? --Dfeuer (talk) 03:56, 24 January 2013 (UTC)
Refactor?
You have this arranged by property, rather than by construction. This strikes me as awkward. The proof 1/proof 2/proof 3 don't provide alternative proofs of the same theorem, but proofs of parallel theorems for different constructions. --Dfeuer (talk) 07:58, 24 January 2013 (UTC)
- They do. It is understood that on any page other than the definition and the "Equiv of Def" page, all definitions are known to be equivalent. The way these have been set up allows to refer to (the apt proof of) these results in the proof of equivalence without introducing circularity. As such I consider the approach taken valuable and am considering implementing it in other areas as well. --Lord_Farin (talk) 08:03, 24 January 2013 (UTC)
- It is also necessary to have this page (well maybe this isn't the best example) to reference to when the result occurs in a particular source that doesn't concern itself with four or more definitions of the real numbers. It is progress that we have proofs for the theorem from all these definitions, as this will make it accessible for people that have only seen one of the approaches. --Lord_Farin (talk) 08:27, 24 January 2013 (UTC)