¿Por qué los matemáticos eligieron la teoría de conjuntos de ZFC sobre la teoría de tipos de Russell?

Question

Como resultado de la paradoja de Russell (y tal vez otros problemas que no soy consciente de), la teoría de conjuntos ingenua tuvo que ser sustituido, y Russell mismo propuso tipo de teoría, que (si he entendido bien) sustituye el lenguaje de la teoría de conjuntos con una diferente. (Y he leído que de alguna manera está relacionado con algo que se llama $\lambda$-cálculo).

Sin embargo, Zermelo–Fraenkel de la teoría de conjuntos (ZFC) también se ocupó de la paradoja de Russell, mediante la formulación restrictiva axiomas sobre los conjuntos.

Los matemáticos claramente han favorecido ZFC sobre el tipo de teoría como de la fundación para las matemáticas. y por lo tanto la mayoría de la gente (incluido yo mismo) ya están familiarizados con la teoría de conjuntos, pero no necesariamente con el tipo de teoría.

¿Cuáles son los aspectos negativos del tipo de la teoría de la comparación con la teoría de conjuntos?

¿Cuáles son los beneficios de tipo de teoría sobre la teoría de conjuntos ZFC?

Answer 1

Voy a responder a tu pregunta del título, pero no a las dos preguntas en el cuerpo. Como los comentarios señalan acertadamente, haciendo así que bien podría llenar un libro. Dicho esto, creo que hay un par de técnicas , aspectos que fueron los factores posibles, que voy a hablar, y luego, sin duda, un montón de factores políticos e históricos que no voy a hablar. Estos factores técnicos, mientras que, por supuesto, siendo cierto, no tiene la fuerza de hoy en día que se hizo en los comienzos del siglo 20. La elección de hoy es claramente impulsada por la historia y pedagógico "infraestructura". Mi impresión es que la mayoría de los alumnos de matemática (incluso restringido a estudiantes de posgrado) ni siquiera son conscientes de que existe una cosa que se llama "el tipo de la teoría de la" excepto tal vez vagamente. (Como una nota terminológica, por "la teoría tipo" voy a por lo general significa conceptual descendientes de Russell tipo de teoría, por todas las cuentas que he leído, Russell temprana de la formulación de la teoría tipo era un poco de un desastre.)

Ahora la respuesta real. La primera cosa que debe tener en cuenta si se mira al Granjero de papel, incluso de tan sólo el resumen, es que el tipo de teoría no es una alternativa a la teoría de conjuntos, es una alternativa a la lógica de primer orden (FOL). Un tipo de teoría es otro tipo de lógica; no es una teoría dentro de la lógica de primer orden como la teoría de conjuntos. En otras palabras, el tipo de teoría (como la fundación) es una lógica de base para las construcciones matemáticas, mientras que la teoría de conjuntos se podría llamar, a falta de una mejor palabra¹, un "matemático" de base para las construcciones matemáticas. Esto no es una gran sorpresa. Este es el espíritu del Logicismo. Hay tres cosas que se pueden tomar a partir de esto, y voy a elaborar sobre cada uno de los siguientes. En primer lugar, el tipo de teoría que era una marca nueva lógica. En segundo lugar, desde una filosofía de la matemática de la perspectiva de estos dos enfoques sugieren filosofías muy distintas. Tercero, axiomatizing de la teoría de conjuntos a través de ZFC es una especie de "reducción" de la teoría de conjuntos para la lógica de primer orden.

Mientras que los detalles formales de FOL se desarrollaba alrededor de este tiempo, más o menos equivalente a los sistemas informales había sido utilizado desde la antigüedad. Que yo sepa formalmente la formulación de FOL salió sin problemas. FOL fue ampliamente aceptado, o al menos fácil de aceptar. Tipo de teoría no era nada parecido a esto en el tiempo. Tipo de teoría fue efectivamente la adición de nuevas "reglas de inferencia" sin la satisfacción de base. Presentaciones de tipo de teoría eran complicados y confusos. Uno de los principales problemas con el tipo de teoría, es que efectivamente hizo la noción de "función" o "predicado" de primera clase. Una de las cosas que van para FOL fue la noción de la semántica para ello fue tema de controversia. En términos modernos, por lo general, utilizar la teoría de conjuntos para hablar acerca de la semántica de primer orden de la teoría, pero la semántica no requiere de la noción de powersets o el axioma de infinitud o que los elementos del dominio de sí mismos se establece. Básicamente, todo lo que necesitas es los productos cartesianos y limitada comprensión. La semántica de la teoría tipo requeriría espacios de funciones o powersets. Pero averiguar lo que "funciones" se fue uno de los problemas que precipitó la "crisis de la fundación".

Tipo de teoría, sin embargo, no estaba destinado a ser utilizado como FOL. FOL es como un lenguaje de especificación. Un primer orden de la teoría es como una especificación, y estamos interesados principalmente en los modelos de la teoría, es decir, cosas que se ajustan a la especificación. Esto se presta a un Platónico de la lectura: las cosas existen y FOL nos permite hablar acerca de ellos. Desde este punto de vista, la teoría de conjuntos ZFC es una forma de hablar de los "conjuntos" que "intuitivamente existe". La fundamental salto de fe es que ZFC tiene un modelo. Tipo de teoría es más parecido a un lenguaje de programación. No hay necesidad de preocuparse acerca de los modelos (aunque este es un rico y poderoso campo hoy en día), ya que puedes construir lo que quieras en el tipo de teoría en sí misma, fuera de la "lógica pura", por así decirlo. Sin embargo, la gente todavía quiere saber lo que "funciones" y "predicados" y hay dos respuestas. En primer lugar, la respuesta abstracta "es algo que podemos aplicar a un argumento" y, en general cumple las reglas correspondientes. Esto lleva a la gente a preguntarse si existen tales cosas y esto nos lleva de nuevo a la semántica. La segunda respuesta es "nada se puede escribir del tipo adecuado". Este está mucho más cerca de un Formalista de la filosofía. Este dice que una función, y todo lo demás, es pura sintaxis. Esta línea de pensamiento, ¿y dio lugar a la ciencia de la computación. El enfoque anterior no parece realmente ayudar en la solución del problema de las fundaciones; el segundo enfoque fue mal entendido en el tiempo y a medida que pasaba el tiempo se hacía cada vez más claro, que lo llevó a un lugar diferente de las matemáticas.

Otra perspectiva sobre lo que la teoría de conjuntos es es que es una "aplicación" de (sin tipo) de orden superior de la lógica en términos de primer orden de la lógica. FOL es como un bajo nivel de lenguaje de programación y ZFC es como una "máquina de programa" en ese idioma, mientras que el tipo de teoría es como un lenguaje de alto nivel. (Nota de nuevo cómo el tipo de la teoría y de la teoría de conjuntos son diferentes tipos de cosas.) Desde una perspectiva de uso, esto hace que ZFC engorroso. A partir de una de las fundaciones perspectiva, sin embargo, esto es exactamente lo que usted desea. Podría decirse que ZFC hace razonablemente bien en comparación con el tipo de teorías, que minimiza la complejidad necesaria para la formalización de un lenguaje que se puede manejar razonablemente en todos los de matemáticas, ver Es ZFC un Hack?. (Este documento incluye el costo de la formalización de FOL, así que la imagen es aún más atractivo para ZFC si usted toma FOL como un dado.)

En última instancia, parece que por el tipo de tiempo de los teóricos consiguió su acto juntos los matemáticos estaban ya a sentirse cómodo con la teoría de conjuntos y ya no se preocupa por las fundaciones. En lugar de ello, científicos de la computación recogido tipo de teoría. Hoy en día lo inesperado, pero profundas conexiones entre la teoría tipo y categoría de teoría, además de la que se esperaba, pero aún profundas conexiones entre la teoría tipo y ciencias de la computación han llevado a un creciente renacimiento de la teoría tipo en matemáticas. Los constructivistas también han puesto un montón de trabajo de campo en demostrar que usted realmente puede hacer un montón de matemáticas "sintácticamente", y la categoría de la teoría ha demostrado que incluso si no eres un constructivista, esto es extremadamente rentable. El tipo de teoría que ha madurado en los últimos cien años.

¹ tal vez alguien puede darme una palabra mejor...

Answer 2

Uno de los problemas con tu pregunta es que muchos de estos términos han cambiado a lo largo del tiempo. He estudiado la hipótesis continua durante los últimos treinta años, con la convicción de que la independencia de la pregunta se encuentra con un problema con la forma lógica se dirige. En la búsqueda de esta convicción me ha remontado a ciertas preguntas a través de las traducciones de las fuentes originales de todo el camino de vuelta a Aristóteles.

La expresión "tipo de teoría" es ahora vaga. Lo que Russell introdujo para evitar lo que él creía ser el origen de la contradicción es la que mejor se llama "predicativo de las matemáticas". En Zermelo-Fraenkel de la teoría de conjuntos se implementa mediante el axioma de fundación. Los conjuntos obtenidos en el acumulado de jerarquía se dice "bien fundada". Por lo tanto, uno tiene individuos, grupos de individuos, los conjuntos de conjuntos de individuos, y así sucesivamente. Este es el predicativo estructura que Russell introdujo con "tipos". En la moderna Zermelo-Fraenkel de la teoría de conjuntos, esto está restringido de alguna manera desde su interpretación habitual es el de una teoría de la pura conjuntos. Es decir, este predicativo jerarquía se genera a partir de un solo individuo llamado el conjunto vacío.

Una razón por la que los matemáticos seguido de Zermelo-Fraenkel de la teoría de conjuntos es, probablemente, el simple hecho de que la reputación de Hilbert de la escuela. Pero, Russell enfoque tenido ciertos problemas más allá de la complejidad de escrito las fórmulas que la disminución de su capacidad para influir en las matemáticas de la comunidad. Uno de estos había sido el axioma de reducibilidad. Este había sido el axioma que Skolem se opuso. El otro había sido la incapacidad para eliminar un axioma de infinitud. Esto es lo que Goedel ridiculizado (muy buen hombre, que con su edificable universo. Y, dentro de la filosofía de la comunidad, Russell uso de descripciones definidas se había encontrado objetable. Estas descripciones constituyen un "epistémica " orden" para los usos de la identidad. Normalmente, esto se llama el principio de identidad de los indiscernibles. El filosóficas objeción es que uno no puede "definir" una existente. Esta crítica, sin embargo, ignora lo que Russell escribió en su papel "En la que denota".

Cuando te preguntan acerca de los beneficios de tipo de teoría en el contexto de Russell trabajo, usted probablemente necesita mirar Quine Nuevas Fundaciones y los autores que lo han estudiado. Quine la teoría simplifica la complejidad de trabajar con escrito de fórmulas. Pero, el sentido en el que se tiene una ventaja de más de Zermelo-Fraenkel de la teoría de conjuntos es que es compatible con lo que se llama Fregean número de clases. Logicismo tiene dos sentidos. Uno es el desarrollo histórico de British matemáticas después de la disputa entre Newton y Leibniz. Newton había establecido un estándar con el cálculo infinitesimal. Así, la búsqueda de una lógica de cálculo había sido una mayor prioridad en el Británico de matemáticas. El trabajo de pavo real y de Morgan, es a veces visto como anticipando modelo moderno de la teoría en virtud de este relato de la historia. Pero, logicismo, en el sentido de Frege se había basado en la idea de que los números naturales se puede definir con respecto a la lógica de la noción de una "clase". Para Quine del trabajo es un desarrollo natural de las ideas de Frege a través de Russell tipo de teoría.

Debido a que el Quinean noción de un individuo se desarrolla con respecto a las ideas del cálculo lambda, existe una relación. Sin embargo, no creo que el trabajo de la Iglesia se origina a partir de las ideas de Russell del tipo de la teoría directa. Por lo que puedo ver en la literatura de la computación, la Iglesia había introducido el cálculo lambda en la búsqueda de una noción de efectivo de la computación.

En la matemática moderna y la computación, la noción de tipo no está obligado a Russell noción de predicativo matemáticas. Un desarrollo separado llamado la categoría de teoría, comenzó a hablar de los objetos con morfismos entre ellos. Dentro de una categoría, los objetos están siempre asociados con una identidad de morfismos. Las nociones modernas de tipo se parece más a la noción Aristotélica de la clase en la que la identidad es un concepto local a un tipo. A su vez, esto se parece más a la categoría de teoría.

Habrá quienes no estén de acuerdo con lo que he dicho. Pero, he tratado de responder a sus preguntas lo mejor que puedo. Espero te sirva de ayuda.

Answer 3

@noé

Tengo que responder de esta manera ya no soy un miembro.

En primer lugar, quiero pedir disculpas a usted y a la comunidad. Hay una gran cantidad de desagradable insinuaciones en las fuentes originales de las fundacional de la literatura. Un ejemplo famoso es "de Russell un trabajo honrado" comentario. Estos tipos de comentarios son algo que me gusta. Pero, es tan fácil de hacer que me encuentro a mí mismo por haber cometido la misma. Y, en Internet, que a menudo conduce a pandemonium.

Iba a escribir algo más largo de la justificación de mi mal paso. Es posible que haya sido informativo. Pero, habría sido una más de la descortesía.

La cita que me molesta con la forma Goedel visto Russell trabajo puede ser encontrado en Goedel obras completas. Es también en Kanamori. Lee,

"... no fue un obstáculo que realmente la hacía prácticamente imposible para los constructivistas para descubrir mi consistencia de la prueba. Es el hecho de que la jerarquía ramificada, que había sido inventado expresamente para fines constructivos, había de ser utilizados en un completamente manera no constructiva."

Una razón que no me gusta de esta cita es que Zermelo-Fraenkel de la teoría de conjuntos se establece expresamente que la teoría no tiene ningún adecuado de las clases. Y, Zermelo había sido claramente siguientes Fregean puntos de vista de la lógica en el modo a través del cual se especifica su dominio. Después de haber leído Frege, sé que su semántica se correspondía con lo que ahora conocemos como libre negativo de la lógica. Si usted visita la página de la SEP en la libre lógica y comparar la semántica de libre positivo de la lógica y libre negativo de la lógica, usted encontrará que Goedelian metatheory es positivo libre de la lógica.

Es romper las reglas. Por supuesto, los defensores de la lógica de primer orden como la lógica matemática de la vista a través de la lente de "progreso".