Editing Constructive analysis (section)

====Apartness====
In the context of analysis, the auxiliary '''logically positive''' predicate
:<math>x\# y\,:=\,(x > y\lor y > x)</math>
may be independently defined and constitutes an ''[[apartness relation]]''. With it, the substitute of the principles above give tightness
:<math>\neg(x\# 0)\leftrightarrow(x\cong 0)</math>
Thus, apartness can also function as a definition of "<math>\cong</math>", rendering it a negation. All negations are stable in intuitionistic logic, and therefore
:<math>\neg\neg(x\cong y)\leftrightarrow(x\cong y)</math>
The elusive trichotomy disjunction itself then reads
:<math>(x\# 0) \lor \neg(x\# 0)</math>
Importantly, a '''proof of the disjunction <math>x\# y</math> carries positive information''', in both senses of the word. Via <math>(\phi\to\neg\psi)\leftrightarrow(\psi\to\neg\phi)</math> it also follows that <math>x\# 0\to\neg(x\cong 0)</math>. In words: A demonstration that a number is somehow apart from zero is also a demonstration that this number is non-zero. But constructively it does not follow that the doubly negative statement <math>\neg(x\cong 0)</math> would imply <math>x\# 0</math>. Consequently, many classically equivalent statements bifurcate into distinct statement. For example, for a fixed polynomial <math>p\in {\mathbb R}[x]</math> and fixed <math>k\in {\mathbb N}</math>, the statement that the <math>k</math>'th coefficient <math>a_k</math> of <math>p</math> is apart from zero is stronger than the mere statement that it is non-zero. A demonstration of former explicates how <math>a_k</math> and zero are related, with respect to the ordering predicate on the reals, while a demonstration of the latter shows how negation of such conditions would imply to a contradiction. In turn, there is then also a strong and a looser notion of, e.g., being a third-order polynomial.

So the excluded middle for <math>x\# 0</math> is apriori stronger than that for <math>x\cong 0</math>. However, see the discussion of possible further axiomatic principles regarding the strength of "<math>\cong</math>" below.