teorema de diaconescu

En lógica matemática , el teorema de Diaconescu , o teorema de Goodman-Myhill , establece que el axioma de elección completo es suficiente para derivar la ley de las formas medias excluidas o restringidas del mismo.

El teorema fue descubierto en 1975 por Radu Diaconescu ^[1] y posteriormente por Goodman y Myhill . ^[2] Ya en 1967, Errett Bishop planteó el teorema como ejercicio (Problema 2 en la página 58 en Fundamentos del análisis constructivo ^[3] ).

En la teoría de conjuntos

El teorema es una conclusión inevitable respecto de la lógica clásica, donde se supone la ley del tercero excluido. Por lo tanto, la siguiente prueba se proporciona utilizando los medios de una teoría de conjuntos constructiva . De la demostración se desprende claramente cómo el teorema se basa en el axioma de emparejamiento así como en un axioma de separación , del cual existen variaciones notables. El axioma de extensionalidad también desempeña un papel crucial en la prueba de la teoría de conjuntos . Las sutilezas que introducen los dos últimos axiomas se analizan más adelante.

Fijación de terminología para la prueba: Llame finito a un conjunto si existe una biyección con un número natural , es decir, un ordinal de von Neumann finito . En particular, escriba , y . Por ejemplo, un conjunto es finito con cardinalidad uno (un singleton habitado) si y sólo si existe comprobadamente una función biyectiva fuera del conjunto . La siguiente prueba es sencilla en el sentido de que no requiere distinciones patológicas con respecto al conjunto vacío. Que un conjunto tenga elección significará que si todos sus miembros están habitados , es dominio de una función de elección . Por último, para habitado , denotado por la proposición que sobreyecta a . ${\displaystyle 0:=\{\}}$ ${\displaystyle 1:=\{0\}}$ ${\displaystyle 2:=\{0,1\}}$ ${\displaystyle 1}$ ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle X\leq ^{*}Y}$ ${\displaystyle Y}$ ${\displaystyle X}$

La estrategia de la prueba es acoplar una proposición dada a un dominio de elección potencial . Y al final sólo se debe hacer uso de una forma bastante restringida de elección plena. Para mayor concreción y simplicidad, la sección supone una teoría de conjuntos constructiva con separación completa , es decir, permitimos la comprensión que involucra cualquier proposición . En ese contexto, el siguiente lema aísla más claramente la idea central: ${\displaystyle P}$ ${\displaystyle X}$ ${\displaystyle P}$

La ley del tercero excluido equivale a la elección en todos los conjuntos habitados . ${\displaystyle X\leq ^{*}2}$

Una vez que se da la dirección hacia atrás de esta equivalencia, entonces el axioma de elección , en particular el otorgamiento de una función de elección en todos los conjuntos de esta forma, implica un término medio excluido para todas las proposiciones.

Prueba del lema

La elección es válida en todos los conjuntos finitos. Dado que en la teoría de conjuntos clásica los conjuntos aquí considerados son probablemente todos finitos (con exactamente las cardinalidades uno o dos), se establece así la dirección directa de la equivalencia.

Para demostrar la dirección hacia atrás se consideran dos subconjuntos de cualquier doubleton con dos miembros distinguibles. Como , una elección conveniente es nuevamente . Entonces, usando Separación, dejemos ${\displaystyle 0\neq 1}$ ${\displaystyle \{0,1\}}$

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

y

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

Ambos y están habitados, como atestiguan y . Si la proposición se puede probar, entonces ambos conjuntos son iguales . En particular, por extensionalidad. A su vez, para cualquier función matemática que pueda tomar ambos conjuntos como argumento, se encuentra , cuyo contrapositivo es . ${\displaystyle U}$ ${\displaystyle V}$ ${\displaystyle 0\in U}$ ${\displaystyle 1\in V}$ ${\displaystyle P}$ ${\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}$

El resto de la prueba se refiere a la pareja , un conjunto de conjuntos habitados. (De hecho, está en sí mismo habitado e incluso valida , lo que significa que está finitamente indexado . Sin embargo, tenga en cuenta que cuando no se supone un medio excluido, no es necesario que sea demostrablemente finito, en el sentido de biyección). ${\displaystyle X:=\{U,V\}}$ ${\displaystyle X}$ ${\displaystyle X\leq ^{*}2}$ ${\displaystyle X}$

Una función de elección por definición tiene que corresponder a la unión general y cumplir ${\displaystyle f}$ ${\displaystyle X}$ ${\displaystyle \{0,1\}}$

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

Usando la definición de los dos subconjuntos y el codominio establecido de la función, esto se reduce a

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

Usando la ley de distributividad , esto a su vez implica . Por el comentario anterior sobre funciones, la existencia de una función de elección en este conjunto implica así la disyunción . Esto concluye la prueba del lema. ${\displaystyle P\lor {\big (}f(U)\neq f(V){\big )}}$ ${\displaystyle P\lor \neg P}$

Discusión

Como se señaló, implica que ambos conjuntos definidos son iguales . En ese caso, el par es igual al conjunto singleton y hay dos funciones de elección posibles en ese dominio, eligiendo o o . Si, en cambio, se puede rechazar, es decir, si se cumple, entonces y . Entonces, en ese caso , y en el par adecuado, solo hay una función de elección posible, elegir el habitante único de cada conjunto singleton. Esta última asignación " y " no es viable si se cumple, ya que las dos entradas son en realidad las mismas. De manera similar, las dos primeras asignaciones no son viables si se cumplen, ya que las dos entradas no comparten ningún miembro común. Lo que se puede decir es que si existe una función de elección, entonces existe una función de elección que elige entre y otra (posiblemente la misma función) que elige entre . ${\displaystyle P}$ ${\displaystyle \{0,1\}}$ ${\displaystyle \{U,V\}}$ ${\displaystyle \{\{0,1\}\}}$ ${\displaystyle 0}$ ${\displaystyle 1}$ ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle U=\{0\}}$ ${\displaystyle V=\{1\}}$ ${\displaystyle U\neq V}$ ${\displaystyle \{\{0\},\{1\}\}}$ ${\displaystyle U\mapsto 0}$ ${\displaystyle V\mapsto 1}$ ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle 0}$ ${\displaystyle U}$ ${\displaystyle 1}$ ${\displaystyle V}$

Para la semántica bivalente , los tres candidatos explícitos anteriores son todas las asignaciones de elección posibles.

Se pueden definir ciertos conjuntos en términos de la proposición y, utilizando el tercero excluido, en la teoría de conjuntos clásica demostrar que estos conjuntos constituyen funciones de elección . Tal conjunto representa una asignación condicionada a si se cumple o no. Si se puede decidir verdadero o falso, entonces dicho conjunto se simplifica explícitamente a uno de los tres candidatos anteriores. ${\displaystyle P}$ ${\displaystyle f\colon \{U,V\}\to \{0,1\}}$ ${\displaystyle P}$ ${\displaystyle P}$

Pero, en cualquier caso, ni ni necesariamente puede establecerse. De hecho, pueden incluso ser independientes de la teoría en cuestión. Dado que los dos primeros candidatos explícitos son incompatibles con el tercero, generalmente no es posible identificar ambos valores de retorno de la función de elección, y , entre los términos y . Por tanto, no es una función en el sentido de la palabra que pueda evaluarse explícitamente en su codominio de valores distinguibles. ${\displaystyle P}$ ${\displaystyle \neg P}$ ${\displaystyle f(U)}$ ${\displaystyle f(V)}$ ${\displaystyle 0}$ ${\displaystyle 1}$

finitud

En una teoría que no asume la disyunción ni ningún principio que la implique, ni siquiera se puede probar que deba ser cierta una disyunción de los enunciados de igualdad de conjuntos anteriores. De hecho, constructivamente también los dos conjuntos y ni siquiera son demostrablemente finitos . (Sin embargo, cualquier ordinal finito se inyecta en cualquier conjunto infinito de Dedekind y, por lo tanto, un subconjunto de un ordinal finito valida la noción lógicamente negativa de finitud de Dedekind. Este es el caso tanto para como para , en los cuales no se puede inyectar. Como comentario aparte, También es consistente con lo clásico en que existen conjuntos que no son ni infinitos según Dedekind ni finitos.) ${\displaystyle P\lor \neg P}$ ${\displaystyle U}$ ${\displaystyle V}$ ${\displaystyle U}$ ${\displaystyle V}$ ${\displaystyle \{0,1,2\}}$ ${\displaystyle {\mathsf {ZF}}}$

A su vez, el binomio también resulta esquivo. Está en la imagen sobreyectiva del dominio , pero con respecto a las asignaciones de elección no se sabe cómo se pueden hacer asignaciones de valores explícitas para ambos y , o incluso cuántas asignaciones diferentes tendrían que especificarse. Por lo tanto, generalmente no existe una definición (conjunto) tal que una teoría constructiva demuestre que la asignación conjunta (conjunto) es una función de elección con dominio . Tenga en cuenta que tal situación no surge con el dominio de funciones de elección otorgado por los principios más débiles de elección contable y dependiente , ya que en estos casos el dominio es siempre justo , el primer cardinal infinito trivialmente contable. ${\displaystyle \{U,V\}}$ ${\displaystyle 2}$ ${\displaystyle U}$ ${\displaystyle V}$ ${\displaystyle \{U,V\}}$ ${\displaystyle \mathbb {N} }$

Adoptar el axioma completo de elección o la lógica clásica implica formalmente que la cardinalidad de es o , lo que a su vez implica que es finita. Pero un postulado como este mero axioma de existencia de función todavía no resuelve la cuestión de qué cardinalidad exacta tiene este dominio, ni determina la cardinalidad del conjunto de posibles valores de salida de esa función. ${\displaystyle \{U,V\}}$ ${\displaystyle 1}$ ${\displaystyle 2}$

Papel de la separación

En resumen, las funciones están relacionadas con la igualdad (por la definición de existencia única utilizada en funcionalidad), la igualdad está relacionada con la membresía (directamente a través del axioma de extensionalidad y también a través de la formalización de la elección en conjuntos) y la membresía está relacionada con los predicados (a través de un axioma de separación). Utilizando el silogismo disyuntivo , el enunciado acaba siendo equivalente a la igualdad extensional de los dos conjuntos. Y la declaración intermedia excluida es equivalente a la existencia de alguna función de elección en . Ambos pasan siempre que puedan usarse en un principio de separación establecido. ${\displaystyle P}$ ${\displaystyle \{U,V\}}$ ${\displaystyle P}$

En teorías que sólo tienen formas restringidas de separación, los tipos de proposiciones para las cuales el tercero excluido está implícito en la elección también están restringidos. En particular, en el esquema axiomático de separación predicativa sólo se pueden utilizar oraciones con cuantificadores ligados establecidos. Esta forma restringida de intermediario excluido todavía no es aceptable constructivamente. Por ejemplo, cuando la aritmética tiene un modelo (cuando, de manera relevante, la colección infinita de números naturales forma un conjunto sobre el que se puede cuantificar), entonces se pueden expresar proposiciones limitadas por conjuntos pero indecidibles. ${\displaystyle P}$

Otros marcos

En la teoría de tipos constructiva , o en la aritmética de Heyting ampliada con tipos finitos, normalmente no existe ningún principio de separación: los subconjuntos de un tipo reciben tratamientos diferentes. Allí, una forma del axioma de elección es un teorema, pero el tercero excluido no lo es.

en topoi

En el artículo original de Diaconescu, el teorema se presenta en términos de modelos topos de teoría constructiva de conjuntos.

Notas

1. Diaconescu, Radu (1975). "Axioma de elección y complementación". Actas de la Sociedad Matemática Estadounidense . 51 (1): 176-178. doi : 10.1090/S0002-9939-1975-0373893-X . SEÑOR  0373893.
2. Goodman, Dakota del Norte; Myhill, J. (1978). "La elección implica un medio excluido". Zeitschrift für Mathematische Logik und Grundlagen der Mathematik . 24 : 461. doi : 10.1002/malq.19780242514.
3. E. Bishop, Fundamentos del análisis constructivo , McGraw-Hill (1967)