構成的数学では、自然数からその集合への部分全射が存在する場合、その集合は部分可算である。これは と表現でき、 ここで はが からへの全射関数であることを表す。全射は の要素であり、ここで のサブクラスは集合であることが要求される。言い換えれば、部分可算集合のすべての要素は機能的に計数数のインデックス集合のイメージであり、したがって集合は可算集合 によって支配されていると理解できる。
議論
命名法
可算性と有限性の特性の命名法は大きく異なることに注意してください。これは、排中律を仮定すると、その多くが一致するためです。繰り返しますが、ここでの議論は、特徴付けられる集合への射影の観点から定義される特性に関するものです。ここでの用語は、構成的集合論のテキストでは一般的ですが、部分可算という名前は、特徴付けられる集合からの射影の観点から定義される特性にも与えられています。
定義内の集合も抽象化することができ、より一般的な概念ではの部分商と呼ぶことができます。
例
重要なケースとしては、問題の集合が計算可能性理論で研究されているより大きな関数のクラスのサブクラスである場合が挙げられます。文脈上、関数が全体であることは関数の決定可能な特性ではないことはよく知られています。実際、インデックス集合に関するライスの定理によれば、インデックスのドメインのほとんどは実際には計算可能な集合ではありません。
対角構成からの関数 で実証されるように、 から全計算可能関数の集合への計算可能射影は存在できず、そのような射影像には決して存在できません。しかし、すべての可能な部分計算可能関数のコード(これにより非終了プログラムも可能になります) により、全関数などの関数のサブセットは部分可算集合であることがわかります。全関数 は、自然数の厳密なサブセットの値域です。自然数の計算不可能な集合によって支配されているため、部分可算という名前は、集合がよりも大きくないことを意味します。同時に、関数空間の特定の制限的構成的意味論では、 が計算可能可算でないことが証明されている場合、そのようなも可算ではなく、 についても同じことが当てはまります。
部分可算性の定義では、すべての可算数と無限かつ非有限のインデックス セットとの間の有効なマップは主張されておらず、部分集合関係のみが主張されていることに注意してください。部分可算であると同時に証明は、それが古典的 (非構成的) に形式的に可算であることを意味しますが、これは有効な可算性を反映するものではありません。言い換えれば、すべての全関数を順番にリストするアルゴリズムをコード化できないという事実は、集合と関数の存在に関する古典的な公理では捉えられません。理論の公理によっては、部分可算性が可算性よりも証明可能である可能性が高いことがわかります。
排中律との関係
構成的論理と集合論では、無限(非有限)集合間の関数の存在が、決定可能性と場合によっては有効性の問題に結び付けられます。そこでは、部分可算性プロパティは可算性から分離されるため、冗長な概念ではありません。自然数のインデックス セットは、分離公理スキームなどの集合論的公理を介して、たとえばサブセットとして存在すると仮定できます。すると、 の定義により、になります。ただし、 このセットは 、 を公理として仮定せずには証明できない という意味で、分離 可能ではない可能性があります。このため、 計数数をインデックス セット にマッピングできない場合は、部分可算セットを効果的に数えることができない可能性があります。可算であることは、部分可算であることを意味します。マルコフの原理との適切なコンテキストでは、逆は排中律、つまりすべての命題に対して が成り立つことと同等です。特に、構成的にこの逆方向は一般には成り立ちません。
古典数学では
古典論理のすべての法則を主張すると、上で議論した の選言的性質は確かにすべての集合に対して成り立ちます。すると、空でない について、数値可能(ここでは がに注入されることを意味します)、可算(の値域として を持つ)、部分可算( のサブセットがに射影される)、および 非生産的( のサブセットに関して本質的に定義される可算性性質)の性質はすべて同値であり、集合が有限または可算無限 であることを表します。
非古典的な主張
排中律がなければ、古典的に(つまり非構成的に)自然数の濃度を超える集合の部分可算性を主張することは一貫している。構成的な設定では、におけるような完全な集合 の外側の関数空間についての可算性の主張は反証される可能性があることに注意してください。しかし、から事実上切り離せない集合による非可算集合の部分可算性は許可される場合があります。
構成的証明は古典的にも妥当である。集合が構成的に非可算であることが証明された場合、古典的な文脈ではそれが部分可算でないことが証明できる。これは に当てはまるため、大規模な関数空間を持つ古典的な枠組みは、ロシア構成主義の公理である構成的なチャーチのテーゼと両立しない。
部分可算とω生成は相互に排他的である
ある集合が-生成的であるとは、その集合のいずれかが- 上の何らかの部分関数の値域である場合に、その値域の補集合内に残る要素が常に存在することを意味する。 [1]
何らかの への任意の全射が存在する場合、前述の対応する補集合は空集合 に等しくなるため、部分可算集合が-生成的になることは決してありません。上で定義したように、-生成的であるという特性は、任意の部分関数の値域を、関数の値域 にない特定の値 に関連付けます。このように、集合が-生成的であることは、そのすべての要素を生成することがいかに難しいかを物語っています。つまり、単一の関数を使用して自然数からすべての要素を生成することはできません。-生成的特性は、部分可算性の障害となります。これは不可算性も意味するため、対角議論では、 1970 年代後半以降、明示的にこの概念が含まれることがよくあります。
計算可能列挙可能部分集合のみを考慮することによっての計算可能列挙可能性の不可能性を確立することができ、また、すべての妨害 の集合が、いわゆる生成関数の全再帰の像となることを要求することができる。
は、の部分集合のみを範囲とする 上の部分関数をすべて正確に保持する空間を表します。集合論では、関数はペアの集合としてモデル化されます。が集合であるときはいつでも、ペアの集合の集合を使用して上の部分関数の空間を特徴付けることができます。 -生成集合に対して は、
建設的に読むと、これは任意の部分関数をその関数の範囲外の要素に関連付けます。この特性は、 -生成集合と任意の全射関数 (部分関数の場合もある) との非互換性を強調します。以下では、これは部分可算性の仮定の研究に適用されます。
集合論
自然数の部分集合に関するカントル派の議論
参照理論として、構成的集合論CZFを検討します。これは、置換、有界分離、強い無限を持ち、冪集合の存在については不可知論ですが、集合も与えられれば任意の関数空間が集合であると主張する公理を含みます。この理論では、すべての集合が部分可算であると主張することも一貫しています。このセクションでは、無限の計数集合上の可能な全射を用いて、さまざまなさらなる公理の互換性について説明します。ここでは、標準的な自然数のモデルを示します。
関数については、全機能の定義により、ドメイン内の すべての値に対して一意の戻り値が存在することを思い出してください。
部分可算集合の場合、全射は の部分集合上で依然として全射である。構成的には、そのような存在的主張は古典的よりも証明可能が少なくなる。
以下で説明する状況(冪クラス上と関数空間上)は、互いに異なります。述語とその真理値(必ずしも真と偽だけが証明できるわけではない)を定義する一般的なサブクラスとは対照的に、関数(プログラミング用語では終了する)は、そのすべてのサブドメイン( のサブセット)のデータに関する情報にアクセスできるようにします。がサブセットの特性関数である場合、関数は戻り値を通じてサブセットのメンバーシップを決定します。一般に定義されたセットのメンバーシップは必ずしも決定可能ではないため、(全体の)関数はのすべてのサブセットと自動的に一対一になるわけではありません。そのため、構成的に、サブセットは特性関数よりも複雑な概念です。実際、CZF 上のいくつかの非古典的な公理のコンテキストでは、のすべてのサブセットのクラスなど、シングルトンの冪クラスでさえ、適切なクラスであることが示されています。
パワークラスへ
以下では、否定導入法の特殊なケースが矛盾していることを意味するという事実が使用されています。
議論を簡単にするために、 は集合であると仮定します。次に、部分集合 と関数 を考えます。さらに、カントールの冪集合に関する定理にあるように、[2] を定義します。ここで 、 これはの従属関係で定義された のサブクラスであり、 と書くこともできます 。 これは、分離を介して部分集合として存在します。 ここで、 を持つ数が存在すると仮定すると、矛盾が意味されます 。 したがって、集合として、 は、任意の与えられた全射に対して阻害を定義できるという点で生産的であることがわかります。 また、全射の存在は、CZF の置換を介して を自動的に集合にするため、この関数の存在は無条件に不可能であることに注意してください。
すべての集合は部分可算であると主張する部分可算性公理は、例えばべき集合公理によって暗示される集合であること と矛盾すると結論付けます。
上記の証明に従うと、どちらにもマッピングできないことが明らかになります。 境界付き分離は、実際に、どの集合も にマッピングされないことを意味します。
同様に、任意の関数 に対して、その値域の部分集合を用いた同様の解析により、 は単射ではないことが示される。関数空間の場合、状況はより複雑である。 [3]
Powersetやそれに相当するもののない古典的なZFCでは、集合である実数のすべてのサブクラスが部分可算であることも一貫しています。その文脈では、これは実数のすべての集合が可算であるというステートメントに変換されます。[4]もちろん、その理論には関数空間セットはありません。
関数空間へ
関数空間の定義により、集合は、証明可能な全関数である集合の部分集合を保持します。すべての集合の許容される部分可算性を主張すると、特に、部分可算集合になります。
そこでここでは、全射関数と のサブセットを[5]のように分離し 、対角化述語を として定義することを 考えます。これは、 否定なしで次のように表現することもできます 。 このセットは、古典的には の関数であることが証明可能であり、特定の入力 に対して値を取るように設計されています。また、これは、 の全射としての存在が実際には矛盾していることを証明するために古典的に使用できます。ただし、構成的には、その定義内の命題が決定可能で、セットが実際に関数割り当てを定義しない限り、このセットが関数空間のメンバーであることを証明することはできません。そのため、古典的な結論を導き出すことはできません。
この方法では、 の部分可算性が認められ、実際に理論のモデルが存在します。しかし、CZF の場合でも、定義域 を持つ完全な全射 の存在は確かに矛盾しています。 の決定可能なメンバーシップにより、集合も可算ではなく、つまり非可算になります。
これらの観察に加えて、任意の非ゼロ数 に対して、全射を含む内の関数は、同様の矛盾の議論によって のすべてに拡張できないことにも注意してください。これは、 内の完全関数に拡張できない部分関数が存在すると表現できます。 が与えられた場合、 かどうかを必ずしも決定できないため、 上の潜在的な関数拡張の値が、以前に特徴付けられた全射 に対してすでに決定されているかどうかさえ決定できないことに注意してください。
すべての集合が部分可算であると主張する部分可算性公理は、LEM を含む、可算にする新しい公理と互換性がありません。
モデル
上記の分析は、のコーディングの形式的な性質に影響を及ぼします。部分可算性公理によるCZF理論の非古典的な拡張のモデルが構築されています。[6] このような非構成的公理は選択原理と見なすことができますが、理論の 証明理論的強度をあまり高める傾向はありません。
- IZFのモデルの中には、分離関係を持つすべての集合が部分可算であるものがある。[7]
- CZF には、たとえばMartin-Löf 型理論 のモデルがあります。古典的に非可算な関数空間を持つこの構成的集合論では、すべての集合が可算であるという部分可算性公理を主張することは確かに一貫しています。議論したように、結果として得られる理論は、べき集合の公理および排中律と矛盾します。
- さらに強力なのは、関数空間公理のない理論であるクリプキ-プラテック集合論のいくつかのモデルで、すべての集合が可算であることさえ検証している点です。
大きさの概念
小さいサイズの判断としての部分可算性は、カントールが定義した濃度関係の標準的な数学的定義と混同されるべきではない。カントールの定義では、より小さい濃度は単射の観点から定義され、濃度の等価性は全単射の観点から定義される。構成的には、集合のクラス上の事前順序" " は、決定可能でも反対称でもない。適度に豊富な集合論における関数空間(および) は、カントールの対角線論証により、常に有限でも と一対一でもないことが分かる。これが非可算性を意味する。しかし、その集合の濃度が、ある意味で自然数の濃度を超えるという議論は、古典的なサイズの概念と、それが誘発する濃度による集合の順序付けのみに制限されている。
計算可能性理論で考察した関数空間の例でわかるように、 のすべての無限部分集合が と必ずしも構成的一対一になるわけではないため、構成的コンテキストにおける無数集合間のより洗練された区別が可能になる。上記のセクションを参考にすると、無限集合はクラス よりも「小さい」と考えられる。
関連プロパティ
部分可算集合は、部分可算にインデックス付けされているとも呼ばれます。定義内の「 」が、ある有限集合の部分集合である集合の存在に置き換えられた類似の概念が存在します。この特性は、部分有限にインデックス付けされているとも呼ばれます。
圏論では、これらすべての概念は部分商です。
参照
参考文献
- ^ Gert Smolka、スコーレムのパラドックスと構成主義、講義ノート、ザールラント大学、2015 年 1 月
- ^ Méhkeri, Daniel (2010)、集合論の簡単な計算的解釈、arXiv : 1005.4380
- ^ バウアー、A.「N^N から N への注入」、2011 年
- ^ Gitman, Victoria (2011)、べき乗集合のないZFC理論とは何か、arXiv : 1110.2430
- ^ Bell, John L. (2004)、「ラッセルのパラドックスと構成的文脈における対角化」(PDF)、Link, Godehard (編)、『ラッセルのパラドックスの 100 年』、De Gruyter Series in Logic and its Applications、第 6 巻、de Gruyter、ベルリン、pp. 221– 225、MR 2104745
- ^ Rathjen, Michael (2006)、「構成的集合論と古典的集合論における選択原理」(PDF)、Chatzidakis, Zoé、Koepke, Peter、Pohlers, Wolfram (編)、Logic Colloquium '02: Joint proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic and the Biannual Meeting of the German Association for Mathematical Logic and the Foundations of Exact Sciences (the Colloquium Logicum) held in Münster, August 3–11, 2002、Lecture Notes in Logic、vol. 27、La Jolla, CA: Association for Symbolic Logic、pp. 299– 326、MR 2258712
- ^ マッカーティ、チャールズ(1986)、「実現可能性の下での部分可算性」、ノートルダム形式論理ジャーナル、27(2):210〜220、doi:10.1305/ndjfl/1093636613、MR 0842149
