Editing Constructive analysis (section)

==Logical preliminaries==
The base logic of constructive analysis is [[intuitionistic logic]], which means that the [[principle of excluded middle]] <math>{\mathrm {PEM}}</math> is not automatically assumed for every [[proposition]]. If a proposition <math>\neg\neg\exists x.\theta(x)</math> is provable, this exactly means that the non-existence claim <math>\neg\exists x.\theta(x)</math> being provable would be absurd, and so the latter cannot also be provable in a consistent theory. The double-negated existence claim is a logically negative statement and implied by, but generally not equivalent to the existence claim itself. Much of the intricacies of constructive analysis can be framed in terms of the weakness of propositions of the logically negative form <math>\neg\neg\phi</math>, which is generally weaker than <math>\phi</math>. In turn, also an implication <math>\big(\exists x.\theta(x)\big)\to \neg\forall x.\neg\theta(x)</math> can generally be not reversed.

While a constructive theory proves fewer theorems than its classical counter-part in its classical presentation, it may exhibit attractive meta-logical properties. For example, if a theory <math>{\mathsf {T}}</math> exhibits the [[disjunction property]], then if it proves a disjunction <math>{\mathsf {T}}\vdash \phi\lor \psi</math> then also <math>{\mathsf {T}}\vdash \phi</math> or <math>{\mathsf {T}}\vdash \psi</math>. Already in classical arithmetic, this is violated for the most basic propositions about sequences of numbers - as demonstrated next.

===Undecidable predicates===
A common strategy of formalization of real numbers is in terms of sequences or rationals, <math>{\mathbb Q}^{\mathbb N}</math> and so we draw motivation and examples in terms of those. So to define terms, consider a [[decidable problem|decidable]] predicate on the naturals, which in the constructive vernacular means <math>\forall n. \big( Q(n)\lor\neg Q(n) \big)</math> is provable, and let <math>\chi_Q\colon{\mathbb N}\to\{0, 1\}</math> be the characteristic function defined to equal <math>0</math> exactly where <math>Q</math> is true. 
The associated sequence <math>q_n\,:=\,{\textstyle\sum}_{k=0}^n \chi_Q(n) / 2^{k+1}</math> is monotone, with values non-strictly growing between the bounds <math>0</math> and <math>1</math>. 
Here, for the sake of demonstration, defining an extensional equality to the zero sequence <math>(q\cong_\mathrm{ext} 0)\,:=\,\forall n. q_n=0</math>, it follows that <math>q\cong_\mathrm{ext} 0 \leftrightarrow\forall n. Q(n)</math>. Note that the symbol "<math>0</math>" is used in several contexts here. For any theory capturing arithmetic, there are many yet undecided and even provenly independent such statements <math>\forall n. Q(n)</math>. Two <math>\Pi_1^0</math>-examples are the [[Goldbach conjecture]] and the [[Rosser's trick|Rosser sentence]] of a theory. 

Consider any theory <math>{\mathsf{T}}</math> with quantifiers ranging over [[primitive recursive]], rational-valued sequences. Already [[minimal logic]] proves the non-contradiction claim for any proposition, and that the negation of excluded middle for any given proposition would be absurd. This also means there is no consistent theory (even if anti-classical) rejecting the excluded middle disjunction for any given proposition. Indeed, it holds that
:<math>{\mathsf{T}}\,\,\,\vdash\,\,\,\forall(x\in{\mathbb Q}^{\mathbb N}).\,\neg\neg\big((x\cong_\mathrm{ext} 0)\lor\neg(x\cong_\mathrm{ext} 0)\big)</math>
This theorem is [[Intuitionistic logic#Non-interdefinability of operators|logically equivalent]] to the non-existence claim of a sequence for which the excluded middle disjunction about equality-to-zero would be disprovable. No sequence with that disjunction being rejected can be exhibited.
Assume the theories at hand are [[consistency|consistent]] and arithmetically sound. Now [[Gödel's theorems]] mean that there is an explicit sequence <math>g\in{\mathbb Q}^{\mathbb N}</math> such that, for any fixed precision, <math>{\mathsf{T}}</math> proves the zero-sequence to be a good approximation to <math>g</math>, but it can also meta-logically be established that <math>{\mathsf{T}}\,\nvdash\,(g\cong_\mathrm{ext} 0)</math> as well as <math>{\mathsf{T}}\,\nvdash\,\neg(g\cong_\mathrm{ext} 0)</math>.<ref>{{cite book |last1=Smith |first1=Peter |title=An introduction to Gödel's Theorems |date=2007 |url=http://www.godelbook.net/ |publisher=Cambridge University Press |location=Cambridge, U.K. |isbn=978-0-521-67453-9 |mr=2384958}}</ref> Here this proposition <math>g\cong_\mathrm{ext} 0</math> again amounts to the proposition of universally quantified form.
Trivially
:<math>{\mathsf{T}}+{\mathrm{PEM}}\,\,\,\vdash\,\,\,\forall(x\in{\mathbb Q}^{\mathbb N}).\,(x\cong_\mathrm{ext} 0)\lor\neg(x\cong_\mathrm{ext} 0)</math>
even if these disjunction claims here do not carry any information. In the absence of further axioms breaking the meta-logical properties, constructive entailment instead generally reflects provability. Taboo statements that ought not be decidable (if the aim is to respect the provability interpretation of constructive claims) can be designed for definitions of a custom equivalence "<math>\cong</math>" in formalizations below as well. For implications of disjunctions of yet not proven or disproven propositions, one speaks of [[Constructive proof#Brouwerian counterexamples|weak Brouwerian counterexamples]].

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

===Invertibility===
In the commutative ring of real numbers, a provably non-invertible element equals zero. This and the most basic locality structure is abstracted in the theory of [[Heyting field|Heyting fields]].