非選択公理

非選択公理は、一意選択公理、関数選択公理、関数内包原理とも呼ばれ、関数の存在公理です。選択公理との違いは、前提において、各 に対して の存在が一意であることが既に認められていることです。 ${\displaystyle y}$ ${\displaystyle x}$

この原理は重要ですが、公理としては、弱理解と関数の符号化能力を持つ理論においてのみ興味深いものとなります。例えば、一部の弱構成的集合論^[1]や一部の高階算術などがこれに該当します。

正式な声明

この原理は、すべての領域 に対して、各要素に対して、ある性質が成り立つようなものがちょうど一つ存在するならば、各要素を に写像し、それに応じて与えられた性質が成り立つような関数が存在する、というものである。正式には、これは次のように述べられる。 ${\displaystyle A}$ ${\displaystyle x\in A}$ ${\displaystyle y}$ ${\displaystyle f}$ ${\displaystyle A}$ ${\displaystyle x\in A}$ ${\displaystyle f(x)}$

${\displaystyle \forall x\in A\;\exists !y\;\psi (x,y)\;\to \;\exists f\;{\Big (}\operatorname {Function} (f)\land {\big (}\operatorname {Domain} (f)=A{\big )}\land \forall x\in A\;\psi {\big (}x,f(x){\big )}{\Big )}}$

を任意の述語とみなす場合、これは公理スキーマです。述語の複雑さに対する制限を考慮することができます。例えば、量指定子を含まない式のみが許可される場合があります。 ${\displaystyle \psi }$

公理は と表記されることもある。また、自然数から自然数への関数にのみ適用され、その場合は と呼ばれることもある。関数の値が数列である場合は と呼ばれることもある。理論的に定義すると、特定の余域の存在は定式化の一部となる場合がある。 ${\displaystyle {\mathrm {AC} }!}$ ${\displaystyle {\mathrm {AC} _{00}}!}$ ${\displaystyle {\mathrm {AC} _{01}}!}$

議論

算術と計算可能性

算術フレームワークでは、関数は数の列とみなすことができます。証明計算に排中律が含まれる場合、関数述語の概念も同様に自由主義的なものとなり、関数内包律は構成的なチャーチのテーゼと両立しない関数オブジェクトの存在を認めます。したがって、この 3 つの原理 (排中律、関数内包律、チャーチのテーゼ) は矛盾しています。最初の 2 つの採用は一般的な古典的な高階理論の特徴であり、最後の 2 つの採用は厳密に再帰的な数学の特徴ですが、関数内包律を採用しないことは計算可能性の古典的な研究にも関連がある可能性があります。実際、可算関数内包律は、弱い算術理論、さらには古典的な算術理論の計算可能モデルで検証する必要がないのです。

集合論

集合論では、関数はその関数グラフと同一視される。集合構築記法を用いると、対の集合は次のように特徴付けられる。

${\displaystyle f:={\big \{}\langle x,y\rangle \mid x\in A\land \psi (x,y){\big \}}.}$

ツェルメロ＝フランケル集合論における置換公理は、これが実際には上記の意味で集合かつ関数であることを意味する。したがって、一意選択は定理である。ただし、 は選択公理を採用していないことに注意されたい。 ${\displaystyle {\mathsf {ZF}}}$

直観主義ツェルメロ＝フランケル集合論およびいくつかのより弱い理論においては、一意選択も導出可能である。これは、算術理論の場合と同様に、特定の構成的公理がこれらの理論において厳密に構成的（反古典的）であることを意味する。 ${\displaystyle {\mathsf {IZF}}}$

型理論

公理は、特に理論が集合論をモデル化している場合に、型理論でも役割を果たすことがあります。

カテゴリー理論

矢印理論的に一意の選択の変形は、たとえば、有限極限と極限特性は良好だが、サブオブジェクト分類子の概念が弱められているだけの局所的デカルト閉カテゴリでは失敗する可能性があります。

リンク

• 選択公理
• 可算選択公理
• 置換公理
• 関数概念の歴史

参考文献

1. マイヒル, ジョン (1975). 「構成的集合論」.記号論理学ジャーナル. 40 (3): 347– 382. doi :10.2307/2272159. JSTOR  2272159.

外部リンク

• マイケル・J・ビーソン著『構成的数学の基礎』、シュプリンガー、1985年
• ビーソン, マイケル・J. (1988). 「集合論に基づく計算システムに向けて」.理論計算機科学. 60 (3): 297– 340. doi :10.1016/0304-3975(88)90115-6.