Editing Constructive analysis (section)

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