建設的分析

直観主義論理では、次の形式の選言三段論法${\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}$実数の位置関係に関連する。

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

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

${\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}$両方の意味で肯定的な情報を伝えている。${\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}}$とゼロは、実数上の順序述語に関して関連しているが、後者の証明は、そのような条件の否定が矛盾を意味することを示している。さらに、例えば3次多項式であることについても、強い概念とより緩やかな概念が存在する。

したがって、除外された中間は${\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} }}$。

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

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

このようなモデルが与えられれば、より多くの集合論的概念を定義することが可能になります。実数の任意の部分集合に対して、上限について語ることができます。${\displaystyle b}$否定的に特徴付けられる${\displaystyle x\leq b}$最小上限については、「${\displaystyle \leq }$「.上限とは、実数列によって与えられる上限であり、${\displaystyle <}$「。上限を持つ部分集合が「」に関して良好な振る舞いをする場合${\displaystyle <}$（以下で説明するように）最高位がある。

構成的解析の形式化の一つとして、上述の順序特性をモデル化したものは、有理数列に関する定理を証明する。${\displaystyle x}$正則性条件を満たす${\displaystyle |x_{n}-x_{m}|\leq {\tfrac {1}{n}}+{\tfrac {1}{m}}}$代替案としては、よりタイトな${\displaystyle 2^{-n}}$の代わりに${\displaystyle {\tfrac {1}{n}}}$、後者の場合は非ゼロのインデックスを使用する必要があります。正則数列の有理数のどの2つも、${\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}$しかし、それは前者の論理的否定と同等であることが示された。^{[ 5 ] [ 6 ]}

上記の定義${\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}}$、同様に、そのような2つの実数の等価性についても同様である。また、有理数の列には収束係数が求められる場合もある。正値性は、ある有理数によって最終的に永遠に離れるものとして定義される。

機能選択${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$あるいは、より強力な原則がそのような枠組みを支援する。

注目すべきは、${\displaystyle {\mathbb {Q} }^{\mathbb {N} }}$それぞれが固有のサブクラスにマッピングできるため、かなりコンパクトにコーディングできます。${\displaystyle {\mathbb {N} }}$一連の根拠${\displaystyle i\mapsto {\tfrac {n_{i}}{d_{i}}}(-1)^{s_{i}}}$4つ組の集合としてエンコードされる可能性がある${\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}$これらは等号または実数と呼ばれます。ただし、2つのものを区別できる性質があることに注意してください。${\displaystyle \cong }$-関連実数。

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

この文脈では、理論や実数をデデキントカットの観点からモデル化することも可能である。${\displaystyle {\mathbb {Q} }}$少なくとも仮定すると${\displaystyle {\mathrm {PEM} }}$あるいは依存的な選択の場合、これらの構造は同型である。

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

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

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

任意の2組の実数に対して${\displaystyle a<b}$実数の任意の列${\displaystyle x_{n}}$現実が存在する${\displaystyle z}$と${\displaystyle a<z<b}$そして${\displaystyle \forall (n\in {\mathbb {N} }).x_{n}\,\#\,z}$。

明示的な法則を用いた実数の定式化により、個別の扱いが可能となる。

金森によれば、「対角線論法を非構成性と結びつける歴史的な誤解が永続化されてきた」が、対角線論法の構成的要素はすでにカントールの著作に現れている。^{[ 10 ]}