非選択の公理

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

この原理は重要であるが、公理としては弱い理解力と関数を符号化する能力を持つ理論にのみ興味深い。これは、例えば、いくつかの弱い構成的集合論^[1]やいくつかの高階算術の場合である。

この原理は、すべてのドメイン について、各要素に対して、あるプロパティが成り立つような要素が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 {関数} (f)\land {\big (}\operatorname {ドメイン} (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}}}$

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

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

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

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