建設的な分析

数学において、構成的分析とは、構成的数学のいくつかの原理に従って行われる数学的分析です。

この分野の名称は、古典的解析とは対照的である。古典的解析とは、この文脈では、より一般的な古典数学の原理に従って行われる解析を意味する。しかし、構成的解析には様々な学派があり、多くの異なる形式化が存在する。^[1]何らかの形で古典的であろうと構成的であろうと、そのような解析の枠組みは、何らかの方法で実数直線、つまり有理数とを拡張した集合を非対称な順序構造から定義可能な分離関係で公理化する。中心となるのは、ゼロに等しい を支配する正値述語（ここでは と表記）である。集合のメンバーは、一般に単に実数と呼ばれる。この用語は分野内でこのように多用されているが、すべての枠組みは、古典的解析の定理でもある広範な共通結果の中核を共有している。 ${\displaystyle x>0}$${\displaystyle x\cong 0}$

その定式化のための構成的枠組みは、を含む型によるHeyting 算術の拡張、構成的二階算術、またはの構成的対応物であるなどの十分に強いトポス、型、または構成的集合論です。もちろん、直接的な公理化も研究することができます。 ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {ZF}}}$

構成的分析の基本論理は直観主義論理であり、これは排中律が すべての命題に対して自動的に想定されるわけではないことを意味します。命題が証明可能であれば、これはまさに、存在しないという主張 が証明可能であることは不合理であり、したがって、後者は一貫した理論では証明できないことを意味します。二重否定の存在の主張は論理的に否定的なステートメントであり、 によって含意されますが、一般的には存在の主張自体と同等ではありません。構成的分析の複雑さの多くは、よりも一般的に弱い論理的に否定的な形式の命題の弱さという観点から組み立てることができます。同様に、含意も一般的には逆転できません。 ${\displaystyle {\mathrm {PEM} }}$${\displaystyle \neg \neg \exists x.\theta (x)}$${\displaystyle \neg \exists x.\theta (x)}$${\displaystyle \neg \neg \phi }$${\displaystyle \phi}$${\displaystyle {\big (}\exists x.\theta (x){\big )}\to \neg \forall x.\neg \theta (x)}$

構成的理論は、古典的な表現では古典的な理論よりも証明される定理の数が少ないですが、魅力的なメタ論理的特性を示すことがあります。たとえば、理論が選言特性 を示す場合、選言 が証明されると、または も証明されます。次に示すように、古典的な算術ではすでに、数の列に関する最も基本的な命題でこれが破られています。 ${\displaystyle {\mathsf {T}}}$${\displaystyle {\mathsf {T}}\vdash \phi \lor \psi }$${\displaystyle {\mathsf {T}}\vdash \phi }$${\displaystyle {\mathsf {T}}\vdash \psi }$

実数の形式化の一般的な戦略は、数列または有理数に関するものであり、したがって、それらに関して動機付けと例を示します。したがって、用語を定義するには、構成的な俗語では証明可能であることを意味する自然数に関する決定可能な述語を考え、が正確に等しいと定義される特性関数であるとします。ここで、が真です。関連付けられている数列は単調で、値は境界との間を非厳密に増加します。ここで、デモンストレーションのために、ゼロ数列への外延的等式を定義すると、 となります。ここでは、記号「」がいくつかのコンテキストで使用されていることに注意してください。算術を捉える理論には、そのようなステートメントが多数存在し、証明されても独立です。2 つの例として、理論の ゴールドバッハ予想とロッサー文があります。${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$${\displaystyle \forall n.{\big (}Q(n)\lor \neg Q(n){\big )}}$${\displaystyle \chi _{Q}\colon {\mathbb {N} }\to \{0,1\}}$${\displaystyle 0}$${\displaystyle Q}$${\displaystyle q_{n}\,:=\,{\textstyle \sum }_{k=0}^{n}\chi _{Q}(n)/2^{n+1}}$${\displaystyle 0}$${\displaystyle 1}$${\displaystyle (q\cong _{\mathrm {ext} }0)\,:=\,\forall n.q_{n}=0}$${\displaystyle q\cong _{\mathrm {ext} }0\leftrightarrow \forall nQ(n)}$${\displaystyle 0}$${\displaystyle \forall nQ(n)}$${\displaystyle \Pi _{1}^{0}}$

原始的な再帰的、有理数値列にわたる量化子を持つ理論を考えてみましょう。最小論理はすでに、あらゆる命題に対する無矛盾の主張と、あらゆる命題に対する排中律の否定が不合理であることを証明しています。これはまた、あらゆる命題に対する排中律の否定を否定する一貫した理論（たとえ反古典的であっても）が存在しないことを意味します。実際、それは ${\displaystyle {\mathsf {T}}}$

${\displaystyle {\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 )}}$

この定理は、ゼロとの等価性に関する排中選言が反証可能なシーケンスが存在しないという主張と論理的に同等である。その選言が否定されるシーケンスは示されない。手元の理論が一貫しており、算術的に正しいと仮定する。ここでゲーデルの定理は、任意の固定された精度に対してゼロシーケンスが の良好な近似値であることを証明するような明示的なシーケンスが存在することを意味するが、と同様に であることもメタ論理的に確立できる。^[2]ここでこの命題は再び普遍量化形式の命題となる。自明なことに ${\displaystyle g\in {\mathbb {Q} }^{\mathbb {N} }}$${\displaystyle {\mathsf {T}}}$${\displaystyle g}$${\displaystyle {\mathsf {T}}\,\nvdash \,(g\cong _{\mathrm {ext} }0)}$${\displaystyle {\mathsf {T}}\,\nvdash \,\neg (g\cong _{\mathrm {ext} }0)}$${\displaystyle g\cong _{\mathrm {ext} }0}$

${\displaystyle {\mathsf {T}}+{\mathrm {PEM} }\,\,\,\vdash \,\,\,\forall (x\in {\mathbb {Q} }^{\mathbb {N} }).\,(x\cong _{\mathrm {ext} }0)\lor \neg (x\cong _{\mathrm {ext} }0)}$

ここでのこれらの選言の主張が何の情報も持たないとしても。メタ論理的性質を破るさらなる公理がない場合、構成的含意は一般に証明可能性を反映します。決定可能ではないはずのタブーなステートメント（構成的主張の証明可能性の解釈を尊重することが目的である場合）は、以下の形式化でもカスタム同値「 」の定義用に設計できます。まだ証明または反証されていない命題の選言の含意については、弱い Brouwerian 反例と呼ばれます。 ${\displaystyle \cong}$

実閉体の理論は、すべての非論理的公理が構成原理に従うように公理化できる。これは、正の単位と非正のゼロを持つ、つまりおよび である、正値述語 の公理を持つ可換環に関する。このような環では、 を定義でき、これはその構成的定式化において厳密な全順序 (線型順序、または文脈を明示的にするために擬似順序とも呼ばれる) を構成する。通常どおり、は として定義される。 ${\displaystyle x>0}$${\displaystyle 1>0}$${\displaystyle \neg (0>0)}$${\displaystyle y>x\,:=\,(yx>0)}$${\displaystyle x<0}$${\displaystyle 0>x}$

この第一階理論は、以下で説明する構造がそのモデルであるため重要です。^{[3]しかし、このセクションでは}位相に似た側面については触れず、関連する算術的サブ構造は定義できません。

説明したように、さまざまな述語は、順序理論的な関係から形成されるものなど、構成的な定式化では決定できません。これには「」が含まれますが、これは否定と同等になります。重要な選言については、ここで明示的に説明します。 ${\displaystyle \cong}$

直観論理学では、形式における選言的三段論法は、一般的には-方向のみに進む。擬似順序では、 ${\displaystyle (\phi \lor \psi )\to (\neg \phi \to \psi )}$${\displaystyle \to}$

${\displaystyle \neg (x>0\lor 0>x)\to x\cong 0}$

そして実際、3つのうち最大で1つが同時に成立する。しかし、より強い、論理的に肯定的な 三分法の選言法則は一般には成立しない。つまり、すべての実数に対して、

${\displaystyle (x>0\lor 0>x)\lor x\cong 0}$

解析的な を${\displaystyle {\mathrm {LPO} }}$参照してください。ただし、他の正値性の結果に基づいて、他の選言が暗示されます。同様に、理論の非対称順序は、実数の位置に関連するすべての に対して弱線形性プロパティを満たす必要があります。 ${\displaystyle (x+y>0)\to (x>0\lor y>0)}$${\displaystyle (y>x)\to (y>t\lor t>x)}$${\displaystyle t}$

この理論は、正値述語と乗法反転を含む代数演算との関係、および多項式の中間値定理に関するさらなる公理を検証します。この理論では、任意の 2 つの離れた数の間には、他の数が存在します。 ${\displaystyle x>0}$

分析の文脈では、補助的な論理的肯定述語

${\displaystyle x\#y\,:=\,(x>y\lor y>x)}$

独立して定義され、分離関係を構成する。これにより、上記の原則の代替は緊密性を与える。

${\displaystyle \neg (x\#0)\leftrightarrow (x\cong 0)}$

このように、分離性は「」の定義としても機能し、それを否定する。すべての否定は直観主義論理では安定しており、したがって ${\displaystyle \cong}$

${\displaystyle \neg \neg (x\cong y)\leftrightarrow (x\cong y)}$

とらえどころのない三分法の分離自体は次のようになる。

${\displaystyle (x\#0)\lor \neg (x\#0)}$

重要なのは、選言の証明は、${\displaystyle x\#y}$単語の両方の意味で、正の情報 を伴うということです。 を介して、 も導かれます。言葉で言うと、ある数が何らかの形でゼロから離れていることの証明は、この数がゼロでないことも証明します。しかし、構成的には、二重に否定的なステートメントがを意味することにはつながりません。その結果、多くの古典的に同値なステートメントが、異なるステートメントに分岐します。たとえば、固定された多項式と固定されたについて、の 番目の係数がゼロから離れているというステートメントは、それがゼロでないという単なるステートメントよりも強力です。前者の証明は、実数上の順序述語に関して、 と 0 がどのように関連しているかを説明します。一方、後者の証明は、そのような条件の否定がどのようにして矛盾を意味するかを示します。次に、たとえば が 3 次多項式である という強い概念とより緩い概念もあります。 ${\displaystyle (\phi \to \neg \psi )\leftrightarrow (\psi \to \neg \phi )}$${\displaystyle x\#0\to \neg (x\cong 0)}$${\displaystyle \neg (x\cong 0)}$${\displaystyle x\#0}$${\displaystyle p\in {\mathbb {R} }[x]}$${\displaystyle k\in {\mathbb {N} }}$${\displaystyle k}$${\displaystyle a_{k}}$${\displaystyle p}$${\displaystyle a_{k}}$

したがって、 の排中原理はの排中原理よりもアプリオリに強いことになります。ただし、以下の「 」 の強さに関するさらなる公理原理の議論を参照してください。${\displaystyle x\#0}$${\displaystyle x\cong 0}$${\displaystyle \cong}$

最後に、関係は論理的に否定的な命題によって定義されるか、それと同等であることが証明され、 はと定義されます。したがって、正値の決定可能性は と表現されますが、前述のように、これは一般には証明できません。ただし、全体性選言 も同様です。解析も参照してください。 ${\displaystyle 0\geq x}$${\displaystyle \neg (x>0)}$${\displaystyle x\leq 0}$${\displaystyle 0\geq x}$${\displaystyle x>0\lor 0\geq x}$${\displaystyle x\geq 0\lor 0\geq x}$${\displaystyle {\mathrm {LLPO} }}$

有効なド・モルガンの法則によれば、このような文の結合は分離性の否定にもなり、したがって

${\displaystyle (x\geq y\land y\geq x)\leftrightarrow (x\cong y)}$

論理和はを意味しますが、他の方向も一般には証明できません。構成的実閉体では、関係 " " は否定であり、一般に の論理和と同等ではありません。 ${\displaystyle x>y\lor x\cong y}$${\displaystyle x\geq y}$${\displaystyle \geq }$

上のような良好な順序特性と強い完全性を同時に要求することは、 を意味します。特に、マクニール完備化はコレクションとしてより完全な特性を持ちますが、その順序関係の理論はより複雑で、その代わりに位置特性は悪くなります。あまり一般的には採用されませんが、この構成も を仮定すると古典的な実数に簡略化されます。 ${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathrm {PEM} }}$

実数の可換環では、証明可能な非可逆元はゼロに等しい。これと最も基本的な局所構造は、Heyting 体の理論で抽象化されている。

一般的なアプローチは、実数を の不揮発性シーケンスと同一視することです。定数シーケンスは有理数に対応します。加算や乗算などの代数演算は、高速化のために体系的な再インデックスとともに、成分ごとに定義できます。シーケンスに関する定義により、目的の公理を満たす厳密な順序 " " の定義も可能になります。上で説明した他の関係も、シーケンスに関して定義できます。特に、 以外の任意の数、つまり は、最終的には、それを超えるとすべての要素が逆になるインデックスを持ちます。^[4] 関係間およびさまざまな特性を持つシーケンス間のさまざまな意味合いが証明されます。 ${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$${\displaystyle >}$${\displaystyle x}$${\displaystyle 0}$${\displaystyle x\#0}$

有理数の有限集合上の最大値は決定可能であるため、実数上の絶対値写像を定義することができ、コーシー収束と実数列の極限を通常どおり定義できます。

収束係数は、実数列のコーシー列の構成的研究でよく使用されます。これは、任意の と適切なインデックス（それを超えると、列は よりも近くなります）との関連付けが、明示的な厳密に増加する関数 の形式で要求されることを意味します。このような係数は、実数列に対して考慮される場合がありますが、すべての実数自体に対して考慮される場合もあります。その場合、実際にはペアの列を扱っていることになります。 ${\displaystyle \varepsilon >0}$${\displaystyle \varepsilon }$${\displaystyle \varepsilon \mapsto N(\varepsilon )}$

このようなモデルが与えられると、より多くの集合論的概念の定義が可能になります。実数の任意の部分集合 について、 を用いて否定的に特徴付けられる上限 について話すことができます。" " に関して最小の上限 について話すことができます。上限は、実数のシーケンスを通じて与えられる上限であり、" " を用いて肯定的に特徴付けられます。上限を持つ部分集合が " " に関して適切に動作する場合 (後述)、上限が存在します。 ${\displaystyle b}$${\displaystyle x\leq b}$${\displaystyle \leq }$${\displaystyle <}$${\displaystyle <}$

構成的解析の1 つの形式化は、上記の順序特性をモデル化することで、正則性条件を満たす有理数列の定理を証明します。別の方法としては、の代わりにより緊密な を使用し、後者の場合は非ゼロのインデックスを使用する必要があります。正則列内の有理数要素のうち 2 つが より離れることはないため、任意の実数を超える自然数を計算できます。正則列に対して、論理的に正の緩い正値特性を と定義します。ここで、右辺の関係は有理数に関するものです。形式的には、この言語における正の実数は、自然な目撃正値を伴う正則列です。さらに、は否定 と論理的に同値です。これは推移的であることが証明されており、同値関係です。この述語により、バンド内の正則列はゼロ列と同値であるとみなされます。このような定義は、もちろん古典的な調査と互換性があり、そのバリエーションは以前にもよく研究されていました。として存在します。また、 は、すべてのと同様に、数値的非負性の性質から定義されるが、その場合は前者の論理否定と同等であることが示される。^{[5] [6]}${\displaystyle x}$${\displaystyle |x_{n}-x_{m}|\leq {\tfrac {1}{n}}+{\tfrac {1}{m}}}$${\displaystyle 2^{-n}}$${\displaystyle {\tfrac {1}{n}}}$${\displaystyle {\tfrac {3}{2}}}$${\displaystyle x>0\,:=\,\exists n.x_{n}>{\tfrac {1}{n}}}$${\displaystyle x\cong y\,:=\,\forall n.|x_{n}-y_{n}|\leq {\tfrac {2}{n}}}$${\displaystyle \neg \exists n.|x_{n}-y_{n}|>{\tfrac {2}{n}}}$${\displaystyle |x_{n}|\leq {\tfrac {2}{n}}}$${\displaystyle y>x}$${\displaystyle (y-x)>0}$${\displaystyle x\geq 0}$${\displaystyle x_{n}\geq -{\tfrac {1}{n}}}$${\displaystyle n}$

上記の定義では、共通境界 が使用されています。他の形式化では、任意の固定境界 に対して、数と は最終的には少なくとも永遠に同じくらい近くなる必要があることを直接定義として採用しています。指数関数的に下がる境界も使用され、たとえば実数条件や、2 つのそのような実数の等式にも使用されます。また、有理数列には収束係数が必要になる場合もあります。正値特性は、何らかの有理数によって最終的には永遠に離れていると定義される場合があります。 ${\displaystyle x\cong y}$${\displaystyle {\tfrac {2}{n}}}$${\displaystyle {\tfrac {2}{N}}}$${\displaystyle x}$${\displaystyle y}$${\displaystyle 2^{-n}}$${\displaystyle \forall n.|x_{n}-x_{n+1}|<2^{-n}}$

機能の選択やより強力な原則は、このようなフレームワークに役立ちます。 ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$

のシーケンスは、それぞれが の一意のサブクラスにマップされるため、かなりコンパクトにコード化できることは注目に値します。有理数のシーケンスは、4 倍体の集合 としてコード化できます。次に、これは算術の基本定理を使用して一意の自然数 としてコード化できます。より経済的なペアリング関数や、拡張エンコード タグやメタデータもあります。このエンコードを使用する例として、シーケンス、またはを使用してオイラー数を計算し、上記のコード化によりのサブクラスにマップできます。この例 (明示的な和のシーケンス) はそもそも全再帰関数ですが、エンコードはこれらのオブジェクトが 2 階算術の量指定子のスコープ内にあることも意味します。 ${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$${\displaystyle {\mathbb {N} }}$${\displaystyle i\mapsto {\tfrac {n_{i}}{d_{i}}}(-1)^{s_{i}}}$${\displaystyle \langle i,n_{i},d_{i},s_{i}\rangle \in {\mathbb {N} }^{4}}$${\displaystyle 2^{i}\cdot 3^{n_{i}}\cdot 5^{d_{i}}\cdot 7^{s_{i}}}$${\displaystyle i\mapsto {\textstyle \sum }_{k=0}^{i}{\tfrac {1}{k}}}$${\displaystyle 1,2,{\tfrac {5}{2}},{\tfrac {8}{3}},\dots }$${\displaystyle \{15,90,24300,6561000,\dots \}}$${\displaystyle {\mathbb {N} }}$

いくつかの解析フレームワークでは、このような行儀の良い数列や有理数に実数という名前が付けられ、 などの関係は等式または実数と呼ばれます。ただし、 に関連する 2 つの実数を区別できる特性があることに注意してください。 ${\displaystyle x\cong y}$${\displaystyle \cong }$

対照的に、自然数をモデル化し、古典的に非可算な関数空間の存在さえも検証する集合論では（そして確かにやさえも）、における " "に関して同値な数は集合に集められ、これはコーシー実数と呼ばれる。その言語では、正則有理数列はコーシー実数の単なる代表に格下げされる。それらの実数の等式は集合の等式によって与えられ、これは集合論的外延性公理によって支配される。結論として、集合論は、論理的等式を使用して表現される実数、すなわちこの集合のクラスの性質を証明する。適切な選択公理が存在する構成的実数はコーシー完全であるが、自動的に順序完全ではない。^[7]${\displaystyle {\mathbb {N} }}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {ZFC}}}$${\displaystyle \cong }$${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$

この文脈では、理論または実数をのデデキント切断でモデル化することも可能です。少なくともまたは 従属選択を仮定する場合、これらの構造は同型です。 ${\displaystyle {\mathbb {Q} }}$${\displaystyle {\mathrm {PEM} }}$

別のアプローチは、実数を、存在する、ペアごとに交差する区間を表すペアを保持する の特定のサブセットとして定義することです。 ${\displaystyle {\mathbb {Q} }\times {\mathbb {Q} }}$

集合論における基数" "の事前順序は、注入存在として定義される主要な概念であることを思い出してください。その結果、基数順序の構成的理論は、古典的な理論から大幅に逸脱する可能性があります。ここで、 のような集合や、実数のいくつかのモデルは、部分可算であると見なすことができます。 ${\displaystyle \leq }$${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$

とはいえ、のような冪集合とのような平易な関数空間の非可算性を証明するカントールの対角線構成は直観的に妥当である。または可算選択公理を仮定すると、 のモデルは構成的枠組み上でも常に非可算である。^[8]現在の文脈に関連する対角線構成の1つの変形は、次のように定式化でき、有理数の列としての実数に対して可算選択とを使用して証明される。^[9]${\displaystyle {\mathcal {P}}{\mathbb {N} }}$${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathbb {R} }}$

任意の 2 つの実数のペアと任意の実数列に対して、およびを満たす実数が存在します。${\displaystyle a<b}$${\displaystyle x_{n}}$${\displaystyle z}$${\displaystyle a<z<b}$${\displaystyle \forall (n\in {\mathbb {N} }).x_{n}\,\#\,z}$

明示的なモジュライによって支援された実数の定式化により、個別の処理が可能になります。

金森によれば、「対角化を非構成性と関連付ける歴史的な誤解が永続化している」が、対角線上の議論の建設的な要素はすでにカンターの著作に現れていた。^[10]

これらすべての考慮は、トポスまたは適切な依存型理論でも行うことができます。

実用的な数学では、従属選択公理がさまざまな学派で採用されています。

マルコフの原理は、ロシアの再帰的数学の学派で採用されています。この原理は、厳密な等式の証明された否定の影響を強化します。いわゆる解析的な形式では、またはが与えられます。より弱い形式が定式化されることもあります。 ${\displaystyle \neg (x\leq 0)\to x>0}$${\displaystyle \neg (x\cong 0)\to x\#0}$

ブローワー学派は広がりの観点から推論し、古典的に有効なバー帰納法を採用します。

さらなる一貫した公理を任意に採用することで、決定可能性の否定が証明可能になる場合があります。たとえば、ブラウワー連続性原理または再帰的数学におけるチャーチのテーゼを採用すると、ゼロへの等号は決定可能であると拒否されます。 ^[11]弱い連続性原理は を反駁するだけでなく も反駁します。スペッカー列の存在はから証明されます。このような現象は実現可能性トポイにも発生します。注目すべきことに、互いに両立しない 2 つの反古典派があります。この記事では、古典理論と両立する原理について説明し、選択が明示的に示されます。 ${\displaystyle {\mathrm {CT} _{0}}}$${\displaystyle x\geq 0\lor 0\geq x}$${\displaystyle {\mathrm {CT} _{0}}}$

多くの古典的な定理は、古典論理上で論理的に同等な定式化でのみ証明できます。一般的に言えば、構成的解析における定理の定式化は、分離可能な空間で最も近い古典理論を反映しています。一部の定理は、近似によってのみ定式化できます。

簡単な例として、中間値定理(IVT) を考えてみましょう。古典的な解析では、IVT は、閉区間[ a , b ]から実数直線Rへの任意の連続関数 f が与えられた場合、f ( a ) が負でf ( b ) が正であれば、その区間に実数c が存在し、 f ( c ) はちょうど0 になることを意味します。構成的解析では、これは成り立ちません。存在量化の構成的解釈 (「存在する」) では、実数c を構成できることが求められるためです(有理数によって任意の精度で近似できるという意味で)。しかし、f がその定義域に沿った区間で 0 付近を推移する場合、これは必ずしも実行できません。

しかし、構成的解析は IVT のいくつかの代替定式化を提供します。これらはすべて、構成的解析ではそうではないものの、古典的解析では通常の形式と同等です。たとえば、古典的定理と同じfの条件下では、任意の自然数 n (大きさに関係なく) が与えられた場合、区間内にf ( c _n )の絶対値が 1/ n未満になるような実数c _{n が}存在します (つまり、構築できます)。つまり、正確にゼロになるcを構築できない場合でも、ゼロに好きなだけ近づくことができます。

あるいは、古典的な IVT と同じ結論（f ( c ) が正確にゼロとなる単一のc ）を維持しながら、 fの条件を強化することもできます。f が局所的に非ゼロであることが要求されます。つまり、区間 [ a , b ] 内の任意の点xと任意の自然数m が与えられた場合、区間内に | y - x | < 1/ mかつ | f ( y )| > 0 となる実数y が存在する（構築できる）ということです。この場合、目的の数c を構築できます。これは複雑な条件ですが、これを暗示し、一般的に満たされる他の条件がいくつかあります。たとえば、すべての解析関数は局所的に非ゼロです（f ( a ) < 0 かつf ( b ) > 0 を既に満たしていると仮定）。

この例を別の角度から見ると、古典論理によれば、局所的に非ゼロの条件が満たされない場合、特定の点xで満たされなければならないこと、そしてf ( x ) が 0 になること、そして IVT が自動的に有効になることに注目してください。したがって、古典論理を使用する古典解析では、完全な IVT を証明するには、構成的バージョンを証明すれば十分です。この観点からすると、構成的解析では完全な IVT が満たされないのは、構成的解析が古典論理を受け入れないからです。逆に、古典数学においても、IVT の真の意味は、局所的に非ゼロの条件を含む構成的バージョンであり、その後に完全な IVT が「純粋論理」に続くものであると主張する人もいます。一部の論理学者は、古典数学が正しいことを認めながらも、構成的アプローチの方が、ほぼこのように、定理の真の意味をより深く理解できると考えています。

古典的解析と構成的解析のもう 1 つの違いは、構成的解析では最小上界原理、つまり実数直線Rの任意の部分集合に最小上界(または上限)があり、その上限は無限大である可能性があるという原理が証明されないことです。ただし、中間値定理と同様に、代替バージョンが存在します。構成的解析では、実数直線の任意の配置された部分集合には上限があります。(ここで、 Rの部分集合S は、 x < yが実数である場合は常に、 x < sとなるSの元s が存在するか、 yがSの上限である場合に配置されます。) 繰り返しますが、これは古典的には完全な最小上界原理と同等です。なぜなら、古典数学ではすべての集合が配置されているからです。また、配置された集合の定義は複雑ですが、すべての区間とすべてのコンパクト セットを含む、一般的に研究される多くの集合によって満たされます。

これと密接に関連して、構成的数学では、コンパクト空間の特徴付けのうち構成的に有効なものはほとんどありません。あるいは別の観点から言えば、古典的には同値だが構成的には同値ではない異なる概念がいくつかあります。実際、区間 [ a , b ] が構成的解析において順次コンパクトであれば、例の最初の構成的バージョンから古典的な IVT が導かれます。つまり、 c を無限列( c _n ) _{n ∈ N}のクラスター点として見つけることができます。

• 計算可能な分析
• 構成的非標準分析
• ヘイティングフィールド
• 分解不可能性（構成的数学）
• 擬似秩序

• ビショップ、エレット（ 1967）。構成的分析の基礎。ISBN 4-87187-714-0。
• ブリッジャー、マーク（2007年）。『実分析：構成的アプローチ』ホーボーケン：ワイリー。ISBN 0-471-79230-6。