Constructive analysis

In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics. The name of the subject contrasts with classical analysis, which in this context means analysis done according to the more common principles of classical mathematics. However, there are various schools of thought and many different formalizations of constructive analysis. Whether classical or constructive in some fashion, any such framework of analysis axiomatizes the real number line by some means, a collection extending the rationals and with an apartness relation definable from an asymmetric order structure. Center stage takes a positivity predicate, here denoted , which governs an equality-to-zero . The members of the collection are generally just called the real numbers. While this term is thus overloaded in the subject, all the frameworks share a broad common core of results that are also theorems of classical analysis. Constructive frameworks for its formulation are extensions of Heyting arithmetic by types including , constructive second-order arithmetic, or strong enough topos-, type- or constructive set theories such as , a constructive counter-part of . Of course, a direct axiomatization may be studied as well. The base logic of constructive analysis is intuitionistic logic, which means that the principle of excluded middle is not automatically assumed for every proposition. If a proposition is provable, this exactly means that the non-existence claim 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 , which is generally weaker than . In turn, also an implication can generally be not reversed.