nLab finite choice



The principle of finite choice states that the dependent product of a finite family of inhabited sets is itself inhabited.

Finite choice is provable in most set theories, including strongly predicative and constructive set theories, as well as set theories without quotient sets.

In dependent type theory, finite choice is definable and provable, provided one has identity types, dependent sum types, bracket types, finite sets, and dependent tuple types in the type theory:

Γn:Γ,i:Fin(n)A(i)typeΓ,a:(i:Fin(n))[A(i)]finitechoice(a):[(i:Fin(n))A(i)]\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma, i:\mathrm{Fin}(n) \vdash A(i) \; \mathrm{type}}{\Gamma, a:(i:\mathrm{Fin}(n)) \to \left[A(i)\right] \vdash \mathrm{finitechoice}(a):\left[(i:\mathrm{Fin}(n)) \to A(i)\right]}

One could express the principle of finite choice as two separate cases representing the case with zero and two inhabited sets:

In dependent type theory, the former follows from the definition of a singleton or contractible type as an inhabited mere proposition, and the latter is given by the following rule:

ΓAtypeΓBtypeΓ,a:[A],b:[B]binarychoice(a,b):[A×B]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, a:[A], b:[B] \vdash \mathrm{binarychoice}(a, b):\left[A \times B\right]}

 See also


  • Which axioms of ZF are used for finite choice?, MathOverflow, (web)

  • Finite choice without AC, Mathematics Stackexchange, (web)

  • Finite axiom of choice: how do you prove it from just ZF?, MathOverflow, (web)

Last revised on January 10, 2023 at 13:56:48. See the history of this page for a list of all contributions to it.