Editing Constructive analysis (section)

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