広がり（直観主義）

直観主義数学において、スプレッドは有限の決定可能な特性によって定義される無限列の種の特定の種類です。ここで、種はコレクションであり、種がそのメンバーによって決定されるという点で古典的なセットに似た概念です。

スプレッドの概念は、 LEJ Brouwer (1918B) によって初めて提案され、連続体を定義するために使用されました。彼のアイデアが発展するにつれて、スプレッドの使用は直観主義数学、特に選択シーケンスと直観主義解析を扱うときに一般的になりました(Dummett 77、Troelstra 77 を参照)。後者では、実数は自然数または整数のドレスドスプレッドによって表されます。

より制限されたいわゆるファンは、数学の直観主義的基礎において特に興味深いものです。そこでは、ファンは主にファン定理（バーに関するもので、ここでは説明しません）の議論で使用されます。ファン定理自体は、一様連続定理の導出に使用される結果です。

現代の用語では、スプレッドは、閉じたシーケンスの集合です。スプレッドは、有限シーケンスに対して(決定可能な)「チェック」を実行するスプレッド関数によって定義されます。無限シーケンスのすべての有限初期部分がスプレッド関数の「チェック」を満たす場合、その無限シーケンスはスプレッドに許容されると言います。スプレッドの概念とそのスプレッド関数は、文献では互換性があります。 グラフ理論的には、スプレッドは、数値の頂点ラベルが付いたルート付き有向木として考えることができます。ファンは、有限スプレッドとも呼ばれ、特殊なタイプのスプレッドです。グラフ用語では、有限に分岐します。最後に、ドレスドスプレッドは、有限シーケンスに作用する関数を組み合わせたスプレッドです。

この記事では、シーケンスの開始と終了を表すために「」と「」を使用します。要素のないシーケンス、いわゆる空のシーケンスは で示されます。 ${\displaystyle \langle}$${\displaystyle \rangle}$${\displaystyle \langle \rangle }$

無限シーケンス が与えられたとき、 かつかつ... かつ の場合にのみ、有限シーケンスはの初期セグメントであるといえます。 ${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$${\displaystyle \langle y_{1},y_{2},\ldots ,y_{i}\rangle }$${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$${\displaystyle x_{1}=y_{1}}$${\displaystyle x_{2}=y_{2}}$${\displaystyle x_{i}=y_{i}}$

スプレッド関数は 、次の特性を満たす有限シーケンス上の関数です。 ${\displaystyle s}$

• または のいずれかの有限シーケンスが与えられた場合。言い換えると、テストされるプロパティはを介し​​て決定可能でなければなりません。${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=1}$${\displaystyle s}$
• ${\displaystyle s(\langle \rangle )=0}$。
• となる有限列が与えられた場合、となるような列が存在します。${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$${\displaystyle k}$${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i},k\rangle )=0}$

有限シーケンスが与えられた場合、 が0 を返す場合、シーケンスはを通じて与えられたスプレッドに許容され、そうでない場合はに許容されません。空のシーケンスは許容されるため、すべてのスプレッドの一部となります。スプレッド内のすべての有限シーケンスは、シーケンスの末尾に余分な要素を追加することで、スプレッド内の別の有限シーケンスに拡張できます。このように、スプレッド関数は、多くの長い有限シーケンスを受け入れる 特性関数として機能します。${\displaystyle s}$${\displaystyle s}$

また、無限シーケンスがスプレッド関数によって定義されるスプレッドに許容されるのは、 のすべての初期セグメントがに許容される場合に限ります。たとえば、法則のような無限の数列を特徴付ける述語の場合、それが何らかのスプレッド関数に関して許容されるかどうかを検証できます。 ${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$${\displaystyle s}$${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$${\displaystyle s}$

非公式には、スプレッド関数は、スプレッドに許容される有限シーケンスが与えられた場合、このシーケンスの末尾に追加できる可能性のある値が有限個しかないため、新しい拡張有限シーケンスがスプレッドに許容される場合にファンを定義します。または、スプレッドに許容されるシーケンスの各要素の値に上限があると言うこともできます。正式には、次のように なります。${\displaystyle s}$

• スプレッド関数は、スプレッドに許容される任意のシーケンスが与えられたときに、任意のシーケンスが与えられたときに、${\displaystyle s}$${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$${\displaystyle k}$${\displaystyle j>k}$${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i},j\rangle )=1}$

したがって、ファンに許容されるシーケンスが与えられた場合、ファンに許容される可能性のある拡張は有限個しか存在せず、拡張が許容されたままになるように許容シーケンスに追加できる最大要素がわかります。

スプレッドの簡単な例としては

• 偶数列の集合
• 1から6までの整数の列の集合
• 有効な端末コマンドのシーケンスのセット。^{[説明が必要]}

• チェスの合法的な動きのシーケンスのセット
• 無限二進数列の集合
• 文字列の集合

以下は、文献でよく使用される 2 つのスプレッドです。

任意の有限シーケンス が与えられると、 が成り立ちます。言い換えると、これはすべての可能なシーケンスを含む広がりです。この広がりは、すべての選択シーケンスのコレクションを表すためによく使用されます。 ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$

任意の有限シーケンス について、すべての要素 ( ) が 0 または 1 の場合は、それ以外の場合は です。言い換えると、これはすべてのバイナリ シーケンスを含むスプレッドです。 ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$${\displaystyle x_{1},x_{2},\ldots ,x_{i}}$${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=1}$

ドレスドスプレッドの例としては、 ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$

${\displaystyle \forall y.(0<y\leq i)\to {\big (}(x_{i}=0)\lor (x_{i}=2\cdot x_{y-1}\pm 1){\big )}}$、

関数 と組み合わせると 、実数を表します。 ${\displaystyle f(\langle x_{1},x_{2},\ldots ,x_{i}\rangle)=x_{i}\cdot 2^{2-i}}$

• バー誘導
• 選択シーケンス
• 建設的な分析

• LEJ Brouwer Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten。エルスター・テイル、アルゲマイネ・メンゲンレーレ、KNAW Verhandelingen、5: 1–43 (1918A)
• マイケル・ダメット 『直観主義の要素』オックスフォード大学出版局（1977年）
• AS トロルストラ 『選択列: 直観主義数学の一章』クラレンドン プレス (1977)