¿Cuál es incorrecto con ZFC?

Question

¿Por qué hay aparentemente para muchos de los que quieren utilizar ETCS, o HoTT, o similar, como un fundamento de las matemáticas? Soy consciente de que HoTT tiene un buen par de buenos aspectos, pero eso no completamente explicar el fuerte deseo de encontrar algo distinto de ZFC a usar, así que me pregunto:

Lo que está mal, en realidad, con ZFC que las unidades de este deseo?

He escuchado un par de argumentos ya, aunque eran un poco vago - voy a enumerar a continuación.

1. Como todos los objetos de ZFC son conjuntos, en ZFC preguntas tales como "es $\pi \in 3$" se les puede pedir, y por alguna razón, sólo por el hecho de que puede pedir es un problema...pero realmente no veo el problema. Usted no necesita hacer esas preguntas, así que donde iban a causar un problema?

2. Otro argumento es que ZFC tiene mucha "equipaje" causado por la jerarquía acumulativa - no queremos tener que preocuparse de la configuración de los aspectos teóricos de los elementos de los números reales, por ejemplo. Esto, de nuevo, se pierde en mí - ¿alguien puede dar un ejemplo de hasta donde realmente alguna vez sentimos la necesidad de decir nada en absoluto acerca de dichos aspectos? Seguramente una vez que tienes tu definiciones y tiene un par de propiedades que usted desea, puede proceder a deducir utilizando únicamente las propiedades y puede ignorar aquellos que no quieren pensar?

Usted nunca va a conseguir un falso teorema de ignorar un axioma - cuando uno prueba algo acerca de los grupos en general no importa lo extraño de las propiedades individuales de los grupos que siguen el grupo de axiomas así que la conclusión es válida. Del mismo modo sabemos cuáles son las propiedades que queremos que los números reales que tienen, por lo que seguramente podemos deducir de aquellos sin ningún problema real una vez que tenemos un objeto con aquellos (aunque posiblemente otros) propiedades?

3. El último problema aparente que voy a mencionar es categorías. Al parecer ZFC (supongamos que con Universos) es un dolor de cabeza para la categoría teóricos. Algo acerca de ZFC hace que la categoría de la teoría de la más difícil de lo que sería, digamos, homotopy tipo teórico de las fundaciones. Hasta el momento todas las que he visto es el de la mano saludando - ¿alguien puede dar un ejemplo de donde ZFC(+U) realmente hace la vida mucho más difícil para los teóricos de la categoría? ¿Cuál es el problema?

Sé que este es un poste negativo, preguntando lo que está mal con ZFC en lugar de lo que es derecho sobre HoTT, ETC, etc, es sólo que he visto muchas referencias vagas de los descontentos con la teoría de conjuntos, pero que aún no se concreta quejas.

Como con muchas de mis preguntas inusuales, las etiquetas son conjeturas.

Answer 1

Como muchos de los comentaristas han dicho, no hay nada "malo" en ZFC en un nivel práctico; es solo que las otras teorías tienen ciertas ventajas. No estoy seguro de lo que se está refiriendo a "el fuerte deseo de encontrar algo distinto de ZFC usar" — para la mayor parte sólo he visto a la gente señalando ventajas de particular otras teorías, en lugar de quejarse de que ZFC es roto por su propia cuenta.

Los dos primeros inconvenientes que se señalan son, como usted dice, no de la práctica de importancia para el uso de ZFC como una base para las matemáticas. Pero no son de valor observaciones. Si nada más, son importantes filosófica observaciones que hay formas en las que ZFC no coincide con la práctica cotidiana de los matemáticos, por lo que debe ser de interés filosófico que hay otras fundaciones que hacer coincidir mejor.

También hay una pedagógico punto a tener en cuenta: el trabajo matemático puede tener ningún problema en ignorar un axioma, pero solamente un alumno al aprendizaje de las matemáticas puede obtener la impresión errónea acerca de cómo los conjuntos se utilizan en las matemáticas de una ZFC orientado a la introducción. (De hecho, pedagógico consideraciones fueron lo primero que vamos a Lawvere inventar ETCS.)

Y también hay una cuestión de extensibilidad: cuando tratamos de interpretar fundacional de la teoría de "no estándar" de los modelos (pongo la palabra entre comillas porque tiene un no deseado connotación negativa), es mucho más fácil si utilizamos fundacional de la teoría de que se parece más a los modelos que nos interesan en la medida que surgen naturalmente — es decir, como categorías, no acumulativa jerarquías. Uno puede, con un poco de esfuerzo, construir una jerarquía acumulativa de una categoría, pero no siempre capturar exactamente lo que uno quiere, y por qué la fuerza de uno mismo para ir a través del dolor cuando hay otras muy buenas fundamental de las teorías que podríamos utilizar en lugar de ZFC?

Como categoría de la teoría, hay al menos dos razones por las que una categoría teórico podría estar insatisfecho con la teoría de conjuntos. Uno es el torpe tratamiento de universos utilizados para lidiar con las "grandes categorías", pero la alternativa a las fundaciones que usted menciona (ETCS, HoTT) realmente no hacen nada para resolver el problema. (Hay otra alternativa fundaciones, tales como los propuestos por Feferman, que hacen el intento de abordar esa pregunta, pero yo no sé mucho acerca de ellos.)

Otro problema con la teoría de conjuntos para la categoría de la teoría es que cualquiera de los dos objetos en la teoría de conjuntos puede ser igual, mientras que en la categoría de teoría por lo general sólo desee considerar objetos de hasta isomorfismo, o de las categorías de equivalencia, y así sucesivamente en dimensiones superiores. Usted podría pensar que esto es como la pregunta de tonterías declaraciones de $3\in \pi$, ya que usted puede simplemente ignorar la noción de igualdad y el uso de isomorfismo. Sin embargo, técnicamente, usted, a continuación, incurrir en la obligación de demostrar que todos los teoremas y construcciones respecto isomorfismo (o equivalencia). Nadie realmente no esta en matemáticas diarias, siendo considerado como obvio; pero cuando se inicia la formalización de las matemáticas en una computadora, se hace necesario y tedioso. ETCS y HoTT tienen algunas ventajas aquí: en ETCS formulados adecuadamente, uno puede demostrar que una metatheorem que todo lo transporta a través de isomorfismo; mientras que en HoTT este transportabilidad es parte de la teoría básica (la univalence axioma).

Para ser justos, debo señalar que ZFC en sí tiene algunas ventajas sobre otros fundacional teorías. En particular, está muy bien adaptado para lo que los matemáticos que se llaman a sí mismos "conjunto de los teóricos de la" utilizar, es decir, el estudio de la bien fundada de las relaciones. La mayoría de los resultados de la moderna teoría de conjuntos podría ser formulado y probado en la alternativa de las fundaciones, pero a menudo se vuelven mucho más torpe.