ディアコネスキュの定理

選択はすべての有限集合において有効である。古典的な集合論では、ここで考察する集合はすべて有限集合（濃度がちょうど1または2である）であることが証明されているため、同値の順方向が確立される。

逆方向を証明するには、2 つの区別可能な要素を持つ任意のダブルトンの 2 つの部分集合を考える。${\displaystyle 0\neq 1}$便利な選択肢は再び${\displaystyle \{0,1\}}$。したがって、分離を使用して、

${\displaystyle U=\{x\in \{0,1\}\mid (x=0)\vee P\}}$

そして

${\displaystyle V=\{x\in \{0,1\}\mid (x=1)\lor P\}.}$

両方${\displaystyle U}$そして${\displaystyle V}$人が住んでいる、${\displaystyle 0\in U}$そして${\displaystyle 1\in V}$.もしその命題が${\displaystyle P}$証明できる場合、これら2つの集合は等しい${\displaystyle \{0,1\}}$。 特に、${\displaystyle P\,\to \,U=V}$外延性によって。さらに、任意の数学関数に対して${\displaystyle g}$これら両方の集合を引数として受け取ることができるものを見ると、${\displaystyle P\,\to \,g(U)=g(V)}$の対偶は${\displaystyle g(U)\neq g(V)\,\to \,\neg P}$。

残りの証拠は、ペアに関するものである。${\displaystyle X:=\{U,V\}}$居住集合の集合。（実際、${\displaystyle X}$それ自体が居住しており、さらに検証する${\displaystyle X\leq ^{*}2}$つまり、有限インデックスであるということです。ただし、排中律が仮定されていない場合は、${\displaystyle X}$（全単射の意味で、証明可能な有限である必要はない。）

選択機能${\displaystyle f}$の上${\displaystyle X}$定義上、一般和集合にマッピングされる必要があり、ここでは${\displaystyle \{0,1\}}$、そして満たす

${\displaystyle f(U)\in U\,\land \,f(V)\in V.}$

2つの部分集合の定義と関数の確立された値域を用いると、これは次のように簡略化される。

${\displaystyle {\big (}f(U)=0\lor P{\big )}\land {\big (}f(V)=1\lor P{\big )}.}$

分配法則を用いると、これは次のことを意味する。${\displaystyle P\lor {\big (}f(U)\neq f(V){\big )}}$関数に関する前述のコメントから、この集合上に選択関数が存在するということは、次の論理和を意味する。${\displaystyle P\lor \neg P}$これで補題の証明は完了です。

前述のとおり、${\displaystyle P}$定義された両方の集合が等しいことを意味する${\displaystyle \{0,1\}}$その場合、ペアは${\displaystyle \{U,V\}}$シングルトンセットに等しい${\displaystyle \{\{0,1\}}$そしてその領域には2つの選択関数があり、どちらかを選ぶことができます${\displaystyle 0}$または${\displaystyle 1}$代わりに、${\displaystyle P}$拒否される可能性がある、つまり${\displaystyle \neg P}$保持して、それから${\displaystyle U=\{0\}}$そして${\displaystyle V=\{1\}}$そういう場合${\displaystyle U\neq V}$適切なペアで${\displaystyle \{\{0\},\{1\}\}}$選択関数は1つしかなく、各シングルトンセットの固有の住人を選択します。この最後の割り当て「${\displaystyle U\mapsto 0}$そして${\displaystyle V\mapsto 1}$「は実行可能ではない」${\displaystyle P}$が成り立つ場合、2 つの入力は実際には同じです。同様に、前の 2 つの割り当ては、次の場合には実行可能ではありません。${\displaystyle \neg P}$が成り立つのは、その場合、2 つの入力に共通の要素がないからである。選択関数が存在する場合、それは次の値を取ると言える。${\displaystyle \{0,1\}}$そして選択関数が存在する${\displaystyle 0}$から${\displaystyle U}$、そして（おそらく同じ機能）を選択する${\displaystyle 1}$から${\displaystyle V}$。

二値意味論においては、上記の３つの明示的な候補が、考えられるすべての選択割り当てとなる。

ある集合を命題の観点から定義することができる。${\displaystyle P}$そして、排中律を用いて、古典集合論においてこれらの集合が選択関数を構成することを証明する。${\displaystyle f\colon \{U,V\}\to \{0,1\}}$このような集合は、${\displaystyle P}$保持します。${\displaystyle P}$が真か偽かを判断できる場合、そのような集合は明示的に上記の３つの候補のいずれかに単純化されます。しかし、いずれの場合も、必ずしもどちらかを確立できるとは限りません。${\displaystyle P}$または${\displaystyle \neg P}$実際、それらは対象となる理論とは明らかに独立している可能性がある。そして、前述の 2 つの明示的な候補はそれぞれ 3 番目の候補と互換性がないため、一般的に選択関数の戻り値の両方を明示的に特定することはできない。${\displaystyle f(U)}$そして${\displaystyle f(V)}$2つの用語のうち${\displaystyle 0}$そして${\displaystyle 1}$したがって、それは、明示的に識別可能な値の範囲に評価できるという意味での関数ではありません。

要約すると、関数は等価性に関係しており（機能で使用される一意存在の定義による）、等価性はメンバーシップに関係しており（外延性の公理を通して直接的に、また集合における選択の形式化を通して）、メンバーシップは述語に関係している（分離の公理を通して）。選言三段論法を用いると、次の命題は${\displaystyle P}$最終的には、2 つの集合の外延的等価性に等しくなります。そして、それに対する排中文は、ある選択関数の存在に等しくなります。${\displaystyle \{U,V\}}$両方とも通過する${\displaystyle P}$集合分離原理で使用できる。

分離の形式が限定されている理論では、命題の種類は${\displaystyle P}$選択によって排中律が暗示される場合も制限される。特に、述語分離の公理図式では、集合境界量化子を持つ文のみを用いることができる。しかしながら、その文脈で証明可能な排中律の制限された形式は、構成的にはまだ受け入れられない。例えば、算術にモデルがある場合（関連することに、自然数の無限集合が量化可能な集合を形成する場合）、集合境界を持つが決定不能な命題を表現できる。