stringtranslate.com

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 del medio excluido o formas 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 sobre la lógica clásica, donde se supone la ley del tercero excluido. Por lo tanto, la prueba que sigue se da utilizando los medios de una teoría de conjuntos constructiva . Es evidente a partir de la prueba cómo el teorema se basa en el axioma de emparejamiento, así como en un axioma de separación , de los cuales hay 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.

Terminología de fijación para la prueba: Llamar a un conjunto finito si existe una biyección con un número natural , es decir, un ordinal de von Neumann finito . En particular, escribir , y . Por ejemplo, un conjunto es finito con cardinalidad uno (un singleton habitado) si y solo si existe probadamente una función biyectiva fuera del conjunto . La prueba a continuación es sencilla en el sentido de que no requiere distinciones patológicas relativas al conjunto vacío. Para que un conjunto tenga elección significará que si todos sus miembros están habitados , es el dominio de una función de elección . Por último, para habitado , denote por la proposición que sobreyecta sobre .

La estrategia de la prueba consiste en 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 completa. 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:

La ley del tercero excluido es equivalente a la elección en todos los conjuntos habitados .

Una vez que la dirección hacia atrás de esta equivalencia es dada, entonces el axioma de elección , en particular al conceder una función de elección en todos los conjuntos de esta forma, implica un tercero 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 clásica de conjuntos los conjuntos que se consideran aquí son demostrablemente todos finitos (con exactamente la cardinalidad uno o dos), queda así establecida la dirección hacia delante 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, sea

y

Tanto y están habitados, como lo atestiguan y . Si la proposición puede probarse, entonces ambos conjuntos son iguales a . 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 .

El resto de la prueba se refiere al par , un conjunto de conjuntos habitados. (De hecho, está habitado en sí mismo e incluso valida , lo que significa que está indexado finitamente . Sin embargo, tenga en cuenta que cuando no se supone un medio excluido, no necesita ser demostrablemente finito, en el sentido de biyección).

Una función de elección por definición tiene que mapearse en la unión general y cumplir

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

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 la disyunción . Esto concluye la prueba del lema.

Discusión

Como se ha señalado, implica que ambos conjuntos definidos son iguales a . En ese caso, el par es igual al conjunto singleton y hay dos posibles funciones de elección en ese dominio, escogiendo o bien . Si, en cambio, puede rechazarse, es decir, si se cumple, entonces y . Así que en ese caso , y en el par adecuado sólo hay una posible función de elección, escogiendo al único habitante de cada conjunto singleton. Esta última asignación " y " no es viable si se cumple, ya que entonces las dos entradas son en realidad las mismas. De forma similar, las dos asignaciones anteriores no son viables si se cumple, ya que entonces 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 una (posiblemente la misma función) que elige entre .

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 tercio excluido, en la teoría clásica de conjuntos demostrar que estos conjuntos constituyen funciones de elección . Un conjunto de este tipo representa una asignación condicionada a si se cumple o no. Si se puede decidir si es verdadero o falso, entonces dicho conjunto se simplifica explícitamente a uno de los tres candidatos anteriores.

Pero, en cualquier caso, ni ni ni se pueden establecer necesariamente. 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 lo tanto, no es una función en el sentido de la palabra que podría evaluarse explícitamente en su codominio de valores distinguibles.

Finitud

En una teoría que no asume la disyunción o cualquier principio que la implique, ni siquiera se puede probar que una disyunción de los enunciados de igualdad de conjuntos anteriores debe ser el caso. 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 y , en los que no se pueden inyectar. Como acotación al margen, es coherente también con la teoría clásica que existen conjuntos que no son ni infinitos de Dedekind ni finitos).

A su vez, el emparejamiento también es elusivo. 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 valor explícitas para ambos y , o incluso cuántas asignaciones diferentes tendrían que especificarse. Por lo tanto, generalmente no hay una definición (de conjunto) tal que una teoría constructiva pruebe que la asignación conjunta (conjunto) sea una función de elección con dominio . Nótese que tal situación no surge con el dominio de funciones de elección otorgadas por los principios más débiles de elección contable y dependiente , ya que en estos casos el dominio es siempre solo , el primer cardinal infinito trivialmente contable.

La adopción del axioma de elección completo o de la lógica clásica implica formalmente que la cardinalidad de es o bien o bien , lo que a su vez implica que es finito. Pero un postulado como este mero axioma de existencia de funciones 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.

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 pertenencia (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 pertenencia está relacionada con los predicados (a través de un axioma de separación). Usando el silogismo disyuntivo , el enunciado termina siendo equivalente a la igualdad extensional de los dos conjuntos. Y el enunciado del tercero excluido para ello es equivalente a la existencia de alguna función de elección en . Ambos pasan por siempre que se puede usar en un principio de separación de conjuntos.

En teorías con formas de separación restringidas, los tipos de proposiciones para las que se implica el término medio excluido por 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 acotados por conjuntos. Sin embargo, la forma restringida del término medio excluido demostrable en ese contexto sigue sin ser aceptable de manera constructiva. 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 acotadas por conjuntos pero indecidibles.

Otros marcos

En la teoría de tipos constructivos , o en la aritmética de Heyting extendida con tipos finitos, normalmente no existe ningún principio de separación: los subconjuntos de un tipo reciben tratamientos diferentes. En este caso, una forma del axioma de elección es un teorema, pero el término medio excluido no lo es. [ cita requerida ]

En topoi

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

Notas

  1. ^ Diaconescu, Radu (1975). "Axioma de elección y complementación". Actas de la American Mathematical Society . 51 (1): 176–178. doi : 10.1090/S0002-9939-1975-0373893-X . MR  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 (25–30): 461. doi :10.1002/malq.19780242514.
  3. ^ E. Bishop, Fundamentos del análisis constructivo , McGraw-Hill (1967)