選択シーケンス

直観主義数学では、選択列は列の構成的定式化である。LEJ Brouwerによって定式化された直観主義数学学派は、完全な無限の概念を否定するため、列 (古典数学では無限の対象) を使用するには、列と同じ目的を果たすことができる有限の構成可能な対象の定式化が必要となる。そのため、Brouwer は、抽象的な無限の対象ではなく、構成として与えられる選択列を定式化した。^{[ 1 ]}

法則のない数列と法則のある数列が区別される。^{[ 2 ]}法則のある数列とは、完全に記述できる数列、つまり完全に記述できる完成された構造のことである。例えば、自然数列がこれに該当する。${\displaystyle \mathbb {N} }$は法則的な数列と考えることができる。数列は、唯一の要素 0 と後継関数によって完全に構成的に記述できる。この定式化から、次のことがわかる。${\displaystyle i}$自然数列の 番目の要素は、${\displaystyle i-1}$同様に、関数${\displaystyle f:\mathbb {N} \mapsto \mathbb {N} }$自然数から自然数への写像は、それが取るあらゆる引数の値を効果的に決定し、それによって法則的な数列を記述する。

一方、法則のない（または自由な）シーケンスとは、あらかじめ決定されていないシーケンスのことです。これは、引数 0、1、2、... の値を生成する手順と考えることができます。つまり、法則のないシーケンスとは、${\displaystyle \alpha }$生成するための手順です$\displaystyle \alpha _{0}}$、$\displaystyle \alpha _{1}}$、...（シーケンスの要素）${\displaystyle \alpha }$) 次のようなもの:

• シーケンスの構築の任意の時点で${\displaystyle \alpha }$シーケンスの最初のセグメントのみが既知であり、将来の値には制約がない。${\displaystyle \alpha }$; そして
• 事前に最初のセグメントを指定することができる${\displaystyle \langle \alpha _{0},\alpha _{1},\ldots ,\alpha _{k}\rangle }$の${\displaystyle \alpha }$。

上記の最初の点はやや誤解を招く可能性があることに注意してください。たとえば、数列の値が自然数の集合からのみ抽出されるように指定することもできます。つまり、数列の範囲を事前に指定できるのです。

法則のない数列の典型的な例は、サイコロを振る一連の動作です。どのサイコロを使うかを指定し、必要に応じて最初のサイコロの値を事前に指定することもできます。${\displaystyle k}$ロール（${\displaystyle k\in \mathbb {N} }$さらに、シーケンスの値はセット内に限定します。${\displaystyle \{1,2,3,4,5,6\}}$この仕様は、問題となっている無秩序な数列を生成する手順を規定するものである。したがって、数列の将来の特定の値は、いかなる時点においても既知ではない。

上述の選択列について、特に成り立つと予想される公理が2つあります。${\displaystyle \alpha \in n}$関係「シーケンス」を表す${\displaystyle \alpha }$最初のシーケンスから始まります${\displaystyle n}$「選択シーケンス用」${\displaystyle \alpha }$有限セグメント${\displaystyle n}$（より具体的には、${\displaystyle n}$おそらく有限の初期シーケンスを符号化した整数になるでしょう。

我々は、すべての無秩序なシーケンスについて、オープンデータの公理と呼ばれる以下のことが成り立つと予想する。 $${\displaystyle A(\alpha )\rightarrow \exists n[\alpha \in n\,\land \,\forall \beta \in n[A(\beta )]]}$$ どこ${\displaystyle A}$は一項述語である。この公理の直観的な正当化は次のとおりである。直観主義数学では、 の検証は${\displaystyle A}$シーケンスを保持する${\displaystyle \alpha }$は手続きとして与えられます。この手続きの実行のどの時点でも、シーケンスの有限な初期セグメントのみを調べます。したがって、直感的には、この公理は、検証のどの時点でも、${\displaystyle A}$保持する${\displaystyle \alpha }$我々は、${\displaystyle A}$有限の初期シーケンスに対して成り立つ${\displaystyle \alpha }$;したがって、次のことが当てはまるはずです。${\displaystyle A}$あらゆる無法なシーケンスにも当てはまる${\displaystyle \beta }$この初期シーケンスを共有します。これは、検証手順のどの時点でも${\displaystyle A(\alpha )}$いかなる場合も${\displaystyle \beta }$の頭文字を共有している${\displaystyle \alpha }$エンコード${\displaystyle n}$すでに調査したとおり、同じ手順を実行すると、${\displaystyle \beta }$そうすれば、同じ結果が得られます。この公理は、任意の数の引数を取る任意の述語に一般化できます。

法則のない数列には、別の公理が必要となる。密度公理は次のように与えられる。 $${\displaystyle \forall n\,\exists \alpha [\alpha \in n]}$$ 任意の有限接頭辞（エンコードされたもの）について、${\displaystyle n}$何らかのシーケンスがあります${\displaystyle \alpha }$その接頭辞から始まる。選択シーケンスの集合に「穴」が生じないようにするために、この公理が必要である。この公理があるからこそ、無秩序な選択シーケンスの任意の長さの有限な初期シーケンスを事前に指定できることを要求するのである。この要件がなければ、密度公理は必ずしも保証されない。

• 構成主義（数学の哲学）– 存在証明は構成的でなければならないという哲学的見解