Axioma de elección dependiente

El axioma de elección dependiente es una forma más débil del axioma de elección, que permite construir la mayor parte de las matemáticas, mientras se evitan problemas tales como la paradoja de Banach-Tarski, en contraste, algunas demostraciones tales como el teorema general de Tychonoff no son posibles (dado que tal teorema, por ejemplo, es equivalente al axioma de elección).

Enunciado formal

Para cuales sean conjuntos A y la relación binaria $P\subset A\times A\,$

$[a\in A\,\land \,\forall x\in A\,\exists y\in A\,P(x,y)]\rightarrow \exists f:N\to A\,[f(0)=a\,\land \,\forall n\in N\,P(f(n),f(n+1))]$