¿Cómo afectaría a la investigación de la teoría de conjuntos el uso de ETCS en lugar de ZFC?

Question

En "Rethinking Set Theory", Tom Leinster argumenta a favor de la enseñanza de la teoría axiomática de conjuntos a través de la Teoría Elemental de la Categoría de Conjuntos de Lawvere con 10 axiomas (pero formulada de forma que no requiere conocimientos de teoría de categorías) que utiliza conjuntos y funciones como elementos primitivos en comparación con ZFC que utiliza conjuntos y elementos como primitivos. (aunque si realmente se insiste se pueden reintroducir los elementos como primitivos a costa de más cláusulas). Es más débil que ZFC pero puede hacerse equivalente a ZFC (o equiconsistente según François G. Dorais) con la adición de un axioma 11 que casi nunca se necesita.

http://golem.ph.utexas.edu/category/2012/12/rethinking_set_theory.html

¿Cómo afectaría a la investigación de la teoría de conjuntos el uso de ETCS en lugar de ZFC?

¿Es el ETCS menos engorroso que el ZFC o más, o no importa? ¿Hace las pruebas más largas/cortas o más fáciles/difíciles?

¿Funcionarán mejor los demostradores automatizados de teoremas con ETCS?

Para aclarar, la pregunta no es sobre la fuerza de ETCS: asuma lo que sea necesario para que ETCS esté a la altura de ZFC. La pregunta es sobre los aspectos prácticos de trabajar con los axiomas de ETCS. Supongo que la mayoría de los matemáticos no trabajan directamente con los axiomas de la teoría de conjuntos en absoluto. Así que la pregunta es: si su trabajo implica trabajar directamente con dichos axiomas, entonces qué diferencia (si es que hay alguna) supone para usted, como investigador de la teoría de conjuntos, utilizar un conjunto diferente de axiomas que tengan la misma fuerza. Si he entendido bien, el objetivo del artículo de Tom Leinster era reflejar la práctica matemática real (no teórica de conjuntos), pero mi pregunta se refiere a lo que harían los teóricos de conjuntos si utilizaran estos axiomas. Supongamos también que, a los efectos de esta pregunta, ETCS se refiere específicamente a la reformulación utilizada en este artículo, que está libre de la terminología de categorías y topos. Tal vez esta reformulación debería llamarse ETS. Añadiendo la sustitución se obtendría el nombre ETSR.

Answer 1

Me gusta que hayas hecho esta pregunta, pero me preocupa un poco que se considere "subjetiva y argumentativa".

En cuanto a la segunda pregunta, creo que muchos teóricos de conjuntos (formados desde la infancia en la ZFC) han dejado constancia de que no les resulta fácil trabajar con ETCS o que no es fácil de usar, y me parece bastante comprensible. Hay que superar un obstáculo crítico de lemas al principio cuando se trabaja con ETCS, porque a diferencia de ZFC o alguna variante de ella, no hay un esquema de comprensión ya hecho en ETCS (al menos como se presenta normalmente). Más bien, hay que probar una serie de instancias de comprensión (en las que uno construye una "lógica interna" a mano, por así decirlo) antes de estar listo para volar. Pero después de un cierto punto, con suficientes lemas iniciales en el cinturón, el desarrollo de las matemáticas, digamos del currículo básico de pregrado que implica resultados básicos de análisis real, álgebra, topología, etc., procede más o menos de la misma manera a la que uno está acostumbrado. Así que, en ese sentido, yo diría que "no importa" para las necesidades de los matemáticos en activo.

Al desarrollar su nueva teoría de conjuntos SEAR (Sets, Elements, And Relations), Mike Shulman reconoció este aspecto engorroso de ETCS, citando una analogía que hice una vez sobre ETCS en el ahora moribundo "blog de Todd y Vishal":

[Trimble] "con el ZFC es más bien como si te subieras al coche y te fueras; con el ETCS construyes el motor del coche a partir de piezas más pequeñas con tus propias manos, pero en el proceso te conviertes en un mecánico experto, y no estás tan rígidamente atado a una marca y un modelo concretos".

[Utilizando esta metáfora, el SEAR puede considerarse como un coche ETCS que viene premontado con un bonito panel de control. O, utilizando una metáfora alternativa, ZFC es como Windows, ETCS es como UNIX y SEAR es como OS X (o quizás Ubuntu). Con SEAR obtienes una interfaz agradable y familiar con la que es fácil hacer cosas estándar, hay menos basura que con ZFC, y detrás de las escenas tienes todo el poder de ETCS (y más). (Por supuesto, si te gustan los productos de Microsoft, entonces esta metáfora probablemente no te atraiga).

Así que SEAR pretende combinar las ventajas de ETCS (como una teoría de conjuntos verdaderamente "estructural", en la que los aspectos de los conjuntos que realmente nos importan son isomorfismo-invariantes, y llevan menos "chatarra") con las ventajas de ZFC (en la que los principios de comprensión, etc. están incorporados directamente; véase su axioma 1). Probablemente, SEAR resultará más familiar a los que estén acostumbrados a la teoría de conjuntos ingenua tradicional; no hay nada de este intimidante asunto de "topos bien punteados con NNO y elección" por el que hay que pasar al principio.

Answer 2

En principio, no se perdería nada trabajando en ETCS+R en lugar de ZFC, ya que las dos teorías son muy bien interpretables entre sí. Sin embargo, después de hablarlo con Mike Shulman (a quien agradezco mucho) aquí Llegué a la conclusión de que se perdería mucho en la práctica.

El problema radica en la noción de fundamento. Recordemos que una relación binaria $R$ en un conjunto $A$ está bien fundada si todo subconjunto no vacío $B$ de $A$ tiene un $R$ -elemento mínimo (un $x \in B$ tal que $y \not\mathrel{R} x$ para todos $y \in B$ ); se trata de un $\Pi_1$ declaración en el Jerarquía de Lévy . En ZFC, una afirmación equivalente es que existe una función de rango de valor ordinal para $R$ en $A$ (una función $r:A \to \mathrm{Ord}$ tal que $x \mathrel{R} y \Rightarrow f(x) \lt f(y)$ para todos $x,y\in A$ ). Este es un $\Sigma_1$ declaración en la jerarquía de Lévy debido a que al ser un ordinal es $\Delta_0$ . En ETCS+R, no hay un equivalente adecuado a los ordinales: dos ordenaciones del mismo tipo son indistinguibles entre sí. Por ello, en ETCS+R, el enunciado de la función de rango equivalente es mucho más complejo, ya que hay que decir explícitamente que el codominio de la función de rango es un pozo de ordenación (para lo que hay que utilizar el $\Pi_1$ definición).

Dado que la solidez es $\Delta_1$ en ZFC, es absoluto para modelos transitivos (de un pequeño fragmento) de ZFC. En otras palabras, las incrustaciones transitivas entre modelos de ZFC preservan la fundamentación. (Una incrustación $f:M \to N$ es transitivo si $f$ mapea los elementos de $x$ en $M$ en los elementos de $f(x)$ en $N$ por cada $x \in M$ por lo que el rango de $f$ es una subestructura transitiva de $N$ isomorfo a $M$ .) Para los modelos de ETCS+R, no hay un equivalente natural a las incrustaciones transitivas, por lo que si se quiere preservar la solidez, hay que exigirlo explícitamente. En la práctica, es muy difícil comprobar que una incrustación preserva el carácter de bien fundada, especialmente si se compara con la comprobación de que una incrustación es transitiva.

Por lo tanto, ETCS+R no tiene un buen dominio de la fundamentación en comparación con ZFC. Dado que el estudio de la solidez es tan importante para la teoría de conjuntos moderna, el marco de ZFC es mucho más apropiado que ETCS+R para que los teóricos de conjuntos trabajen con él. Para reformular una analogía que utilicé en otro lugar, pedir a un teórico de conjuntos que trabaje en ETCS+R en lugar de ZFC es como pedir a un teórico de anillos que trabaje con relaciones ternarias $A(x,y,z)$ para la adición $x+y = z$ y $M(x,y,z)$ para la multiplicación $x \cdot y = z$ En principio, es lo mismo, pero simplemente no es lo correcto.

Answer 3

Gran parte de la investigación en teoría de conjuntos (por ejemplo, un artículo en el que estoy trabajando actualmente, relativo a ciertos ultrafiltros sobre los números naturales) funcionaría perfectamente en ETCS. Pero gran parte de la investigación en teoría de conjuntos utiliza el axioma de sustitución de una forma que no puede imitarse en ETCS. El artículo de Tom Leinster da el ejemplo de la existencia de la unión de $\mathbb N$ su conjunto de energía $\mathcal P(\mathbb N)$ el conjunto de potencias de éste, y así sucesivamente, iterando durante un número contable de pasos. En otras palabras, ETCS no puede demostrar que existe un número cardinal $\kappa$ con infinitos cardenales infinitos por debajo de él. Tal $\kappa$ y otros mucho más grandes están ciertamente involucrados en una gran cantidad de teoría de conjuntos a nivel de investigación, por lo que se necesita una base que tenga la fuerza de ZFC (o incluso más) allí.

Answer 4

Nadie ha abordado realmente la cuestión de los demostradores de teoremas automatizados. Voy a entender que esto se refiere de forma más general a las matemáticas asistidas por ordenador, ya que los demostradores de teoremas totalmente automatizados siguen teniendo una utilidad muy limitada para un matemático. Hay muchos y buenos argumentos para afirmar que el mejor sistema de fundamentación para ellos no es ni ZFC (ni sus parientes) ni ETCS (ni sus parientes), sino alguna variedad de teoría de los tipos .

Esto se debe principalmente a que la teoría de tipos está muy vinculada a la programación y tiene un buen comportamiento computacional, por lo que encaja muy bien con los ordenadores. Como la pregunta no es sobre la teoría de tipos, no diré mucho al respecto; sólo quiero señalar que ETCS se parece más a la teoría de tipos que ZFC. Así que aunque dudo que realmente utilizando ETCS en un asistente de pruebas computacional sería mucho mejor que usar ZFC, aprender a pensar en ETCS y hacer matemáticas en él probablemente te pondrá en mejor posición cuando intentes usar un asistente de pruebas basado en la teoría de tipos.

Answer 5

Hay varios parientes (típicamente: subteorías y superteorías) de ZFC que se utilizan en la investigación teórica de conjuntos. Si alguien quiere hacer teoría de conjuntos basada en ETCS o en una teoría base relacionada, estas teorías tendrían que ser traducidas a esta nueva base (o, en el caso de teorías que no son tan canónicas, como ZFC*, habría que encontrar sustitutos).

Esta traducción parece bastante sencilla en el caso de las superteorías; una buena traducción utilizaría, por supuesto, los modismos de la lengua de llegada.

• Ejemplos de superteorías:
  • ZFC más cardenales grandes
  • ZFC más determinismo definible (por ejemplo, determinismo proyectivo, o algunas consecuencias del mismo - relacionadas con grandes cardinales).
  • ZF más AD, o ZF + $V=L(\mathbb R)$ (sólo la superteoría de ZF)
  • ZF(C) más "V es un determinado modelo interior". Las versiones más débiles incluyen:
    • ZFC más supuestos aritméticos cardinales (GCH, SCH)
    • ZFC más principios combinatorios ( $\diamondsuit$ etc.)
  • ZFC más axiomas de forzamiento (MA, PFA, etc.)
  • otros, incluidas las combinaciones (conjunciones) de los anteriores
• Ejemplos de subteorías
  • KP y teorías relacionadas, que no tienen una comprensión completa. (Creo que se suelen asociar a la teoría de la prueba más que a la teoría de conjuntos)
  • ZFC menos el infinito (esto está más relacionado con la aritmética que con la teoría de conjuntos)
  • ZF, o ZF más versiones débiles de elección
  • ZFC menos el conjunto de potencia (más las instancias del conjunto de potencia). Los modelos típicos son de la forma $H(\chi)$ .
  • ZFC menos la sustitución (más un número finito de casos de sustitución). Los modelos típicos son $V_\delta$ .
  • ZFC*, un subconjunto finito a menudo no especificado de ZFC, utilizado para sortear la "indefinibilidad de la verdad", o para aplicar el teorema de la reflexión. (Moralmente es lo mismo que el punto anterior).
  • ZFC menos Foundation, lo que refleja el hecho de que Foundation apenas se utiliza fuera de la teoría de conjuntos.
  • Otros, incluyendo combinaciones (intersecciones) de los anteriores
• Otros familiares:
  • ZF(C) con átomos, tal vez más cerca de la práctica matemática que la propia ZFC.
  • NBG. La relación entre NBG y ZFC se entiende muy bien, al igual que sus ventajas y desventajas: En el lado positivo, NBG puede hablar naturalmente de clases, y está axiomatizada finitamente (lo que podría hacerla más susceptible de demostración automatizada de teoremas). Por otro lado, el hecho de que no todas las subclases de $\mathbb N$ es un conjunto puede ser inconveniente.
  • MK y otros.
  • NF y NFU, que a veces se afirma que son más naturales que la ZFC. Mientras que ZFC hace que sea incómodo hablar de clases, NFU tiene problemas con la función $x\mapsto \{x\}$ .