¿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

Pues bien, sólo habría que añadir una instancia de sustitución lo suficientemente fuerte, o la consecuencia que realmente se necesita, a los supuestos del teorema que se está demostrando. Por ejemplo, se podría tomar la existencia de $\aleph_\omega$ como una suposición (como un gran cardenal) en lugar de demostrar que existe. Hay modelos de ETCS en los que existe y en los que no. En este caso, sólo se está rebajando el nivel en el que se considera un cardinal "grande".

Me recuerda el reciente trabajo de McLarty sobre las teorías de conjuntos débiles, y hacer geometría algebraica en ellas. Uno puede demostrar resultados fuertes sobre la cohomología, pero no puede demostrar la existencia de un anillo incontable como $\mathbb{R}$ o $\mathbb{C}$ . Dice que simplemente se puede plantear la existencia de tal cosa sobre la teoría de conjuntos débiles, y entonces todos los teoremas pasan.

Por supuesto, en la teoría de conjuntos hay toda una pila de resultados que dependen de la fuerza de la ZFC más allá de la ETCS, y supondría todo un esfuerzo matemático inverso averiguar cuál es en realidad necesario para las franjas de teoría, que muchos dirían que es más fácil asumir lo que ZFC te da. Pero no es estrictamente necesario, pero mucho más fácil.