Editing Constructive analysis (section)

===Order vs. disjunctions===
The theory of the [[real closed field]] may be axiomatized such that all the non-logical axioms are in accordance with constructive principles. This concerns a [[commutative ring]] with postulates for a positivity predicate <math>x>0</math>, with a positive unit and non-positive zero, i.e., <math>1>0</math> and <math>\neg(0>0)</math>. In any such ring, one may define <math>y > x\,:=\,(y - x > 0)</math>, which constitutes a strict total order in its constructive formulation (also called linear order or, to be explicit about the context, a [[pseudo-order]]). As is usual, <math>x < 0</math> is defined as <math>0 > x</math>.

This [[first-order logic|first-order]] theory is relevant as the structures discussed below are model thereof.<ref>Erik Palmgren, ''An Intuitionistic Axiomatisation of Real Closed Fields'', Mathematical Logic Quarterly, Volume 48, Issue 2, Pages: 163-320, February 2002</ref> However, this section thus does not concern aspects akin to [[topology]] and relevant arithmetic substructures are not [[Definable set|definable]] therein.

As explained, various predicates will fail to be decidable in a constructive formulation, such as these formed from order-theoretical relations. This includes "<math>\cong</math>", which will be rendered equivalent to a negation. Crucial disjunctions are now discussed explicitly.

====Trichotomy====
In intuitonistic logic, the [[disjunctive syllogism]] in the form <math>(\phi\lor\psi)\to(\neg\phi\to\psi)</math> generally really only goes in the <math>\to</math>-direction. In a pseudo-order, one has
:<math>\neg(x>0 \lor 0>x) \to x\cong 0</math>
and indeed at most one of the three can hold at once. But the stronger, ''logically positive'' '''[[law of trichotomy]] disjunction does not hold in general''', i.e. it is not provable that for all reals,
:<math>(x>0 \lor 0>x) \lor x\cong 0</math>
See [[limited principle of omniscience|analytical <math>{\mathrm {LPO}}</math>]]. Other disjunctions are however implied based on other positivity results, e.g. <math>(x + y > 0) \to (x>0 \lor y>0)</math>. Likewise, the asymmetric order in the theory ought to fulfill the weak linearity property <math>(y > x) \to (y > t \lor t > x)</math> for all <math>t</math>, related to locatedness of the reals.

The theory shall validate further axioms concerning the relation between the positivity predicate <math>x > 0</math> and the algebraic operations including multiplicative inversion, as well as the [[intermediate value theorem]] for polynomials. 
In this theory, between any two separated numbers, other numbers exist.

====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.

====Non-strict partial order====
Lastly, the relation <math>0\ge x</math> may be defined by or proven equivalent to the '''logically negative''' statement <math>\neg(x > 0)</math>, and then <math>x \le 0</math> is defined as <math>0 \ge x</math>. Decidability of positivity may thus be expressed as <math>x > 0\lor 0\ge x</math>, which as noted will not be provable in general. But neither will the totality disjunction <math>x\ge 0 \lor 0\ge x</math>, see also [[limited principle of omniscience|analytical <math>{\mathrm {LLPO}}</math>]].

By a valid [[De Morgan's laws#In intuitionistic logic|De Morgan's law]], the conjunction of such statements is also rendered a negation of apartness, and so
:<math>(x\ge y \land y\ge x)\leftrightarrow (x\cong y)</math>
The disjunction <math>x > y \lor x\cong y</math> implies <math>x\ge y</math>, but the other direction is also not provable in general. In a constructive real closed field, '''the relation "<math>\ge</math>" is a negation and is not equivalent to the disjunction in general'''.

====Variations====
Demanding good order properties as above but strong completeness properties at the same time implies <math>{\mathrm {PEM}}</math>. Notably, the [[Dedekind–MacNeille completion|MacNeille completion]] has better completeness properties as a collection, but a more intricate theory of its order-relation and, in turn, worse locatedness properties. While less commonly employed, also this construction simplifies to the classical real numbers when assuming <math>{\mathrm {PEM}}</math>.