¿Podemos demostrar que la teoría de conjuntos es consistente?

Question

Descargo de responsabilidad

Por supuesto, soy consciente del segundo teorema de incompletitud de Gödel. Aun así, hay algo que no me convence, tal vez sea simplemente que mi clase de lógica fue hace mucho tiempo. Por otro lado, podría resultar que estoy simplemente confundido. :-)

Antecedentes

Voy a hablar sobre modelos de teoría de conjuntos; estos son conjuntos por sí mismos, por lo que puede surgir una confusión, ya que el símbolo $\in$, entendido como "pertenece al conjunto" en el sentido usual, puede tener un significado diferente al símbolo $\in$ de la teoría. Entonces, para evitar confusiones, hablaré sobre niveles.

En el primer nivel está la teoría de conjuntos que los matemáticos utilizan a diario. Esta tiene axiomas, pero no es una teoría en el sentido usual de la lógica. De hecho, para hablar de lógica ya necesitamos conjuntos (para definir alfabetos, entre otras cosas). En esta teoría ingenua de conjuntos desarrollamos la lógica, en particular las nociones de teoría y modelo. Llamamos a esta teoría Set1.

En el segundo nivel está la teoría de conjuntos formalizada; esta es una teoría en el sentido de la lógica. Simplemente copiamos los axiomas de la teoría ingenua de conjuntos y tomamos la teoría (formal) que tiene estas cadenas de símbolos como axiomas. Llamamos a esta teoría Set2.

Ahora, el resultado de Gödel nos dice que si Set2 es consistente, no puede probar su propia consistencia. Bueno, aquí necesitamos ser un poco más precisos. La afirmación tal como está planteada es obvia, ya que Set2 no puede probar nada sobre los conjuntos del primer nivel. Ni siquiera sabe que existen.

Entonces repetimos el proceso que nos llevó de Set1 a Set2: definimos en Set2 las nociones usuales de lógica (alfabetos, teorías, modelos...) y usamos estas para definir otra teoría Set3.

Una afirmación correcta del resultado de Gödel es, creo yo, que

si Set2 es consistente, entonces no puede probar la consistencia de Set3.

El problema

Ok, así que tenemos una afirmación clara que parece ser completamente demostrable en Set1, y de hecho lo es. Sin embargo, esto no nos dice que

si Set1 es consistente, entonces no puede probar la consistencia de Set2.

Entonces me queda la duda de que lo que uno pueda hacer "desde afuera" puede ser un poco más de lo que uno puede hacer en la teoría formalizada. Compare esto con el primer teorema de incompletitud de Gödel, donde tenemos una afirmación que es verdadera para números naturales (y podemos demostrarla desde afuera) pero que no es demostrable en PA.

Entonces la pregunta es:

¿hay alguna razón para creer que Set1 no puede probar la consistencia de Set2? ¿O simplemente estoy confundido y lo que dije no tiene sentido?

Por supuesto, uno podría argumentar que Set1, al no estar formalizada, no es susceptible de investigación matemática; el mejor modelo que tenemos es Set2, por lo que debemos confiar en que siempre podemos "trasladar nuestros teoremas un nivel". Pero este argumento no me convence: de hecho, el primer teorema de incompletitud de Gödel muestra que tenemos situaciones donde los teoremas en la teoría formalizada son estrictamente menores de lo que podemos ver desde afuera.

Comentario final

En cierto sentido, es poco intuitivo que la teoría de conjuntos deba tener un modelo. Porque los modelos deben ser conjuntos, ¡y los conjuntos son tan pequeños...

Por supuesto, sé acerca de los universos y cómo se pueden usar para "incrustar" la teoría de clases dentro de la teoría de conjuntos, por lo que los conjuntos pueden ser más grandes de lo que pienso. Pero una vez más, la existencia de universos no es demostrable a partir de los axiomas usuales de la teoría de conjuntos.

Answer 1

Su pregunta ciertamente tiene sentido y es un punto que siento que a menudo se pasa por alto en los libros de texto.

Voy a reformular tu pregunta. El segundo teorema de Gödel dice que, asumiendo que un cierto sistema formal (ZFC, por ejemplo) tiene una cierta propiedad que llamamos "consistencia", entonces no hay una prueba formal en ZFC de cierta cadena, comúnmente denotada por "Con(ZFC)". Bien. Pero, ¿por qué diablos debería este teorema decir algo sobre si la consistencia de ZFC puede ser probada matemáticamente? El teorema es solo un teorema sobre cadenas abstractas de símbolos, no sobre lo que los seres humanos pueden o no pueden hacer. La cadena denotada "Con(ZFC)" comúnmente se toma como "decir" que "ZFC es consistente", pero ¿cuál es la justificación para hacerlo? Una cadena es solo una cadena y no "dice" nada. Si elegimos pensar que la cadena "significa" algo, entonces eso es asunto nuestro, pero seguramente ese tipo de actividad social humana no es algo sobre lo que podamos probar teoremas matemáticos ¿verdad?

La respuesta es que, subyacente a las discusiones habituales sobre el segundo teorema de Gödel, existe la siguiente Suposición Clave: Si alguien llegara a presentar una prueba matemática de la consistencia de ZFC, entonces imitando esa prueba, podríamos producir una prueba formal de Con(ZFC) a partir de los axiomas de ZFC. La Suposición Clave es crucial. Sin ella, no podemos realizar el salto desde el segundo teorema de Gödel hacia una afirmación meta-matemática sobre la (im)posibilidad de probar la consistencia de las matemáticas. Y hay que tener en cuenta que la Suposición Clave no es puramente matemática; no puede serlo, porque es una afirmación que vincula algo que no es puramente matemático (es decir, la prueba matemática, que es un producto de la actividad humana) y algo que sí lo es (es decir, ZFC y los teoremas de ZFC). Por lo tanto, la Suposición Clave no es susceptible de ser probada matemáticamente, y las razones que tenemos para aceptarla deben ser en parte filosóficas.

Entonces, ¿cuáles son las razones que tenemos para aceptar la Suposición Clave? La razón principal es que la larga experiencia nos ha enseñado que todas las pruebas matemáticas que los matemáticos idean pueden ser imitadas por pruebas formales en ZFC. Esto puede parecernos obvio hoy en día, pero no es en absoluto una afirmación trivial. Antes de la revolución de la teoría de conjuntos, no era en absoluto obvio que todas las diversas áreas de las matemáticas pudieran formularse en un único lenguaje común (es decir, la teoría de conjuntos) y deducirse de una corta lista de axiomas. Solo a través del arduo trabajo de aquellos que trabajan en los cimientos de las matemáticas ahora damos por sentado que para cualquier afirmación matemática precisa que queramos hacer, existe una oración formal $S$ en el lenguaje de primer orden de la teoría de conjuntos con la propiedad de que cualquier prueba matemáticamente aceptable de la afirmación original puede ser imitada para producir una prueba formal de $S$ a partir de los axiomas de ZFC. Y si tenías alguna duda persistente sobre si esta imitación formal existía solo en teoría y no en la práctica, entonces en años recientes, la llegada de software de demostración de teoremas formales como Mizar, HOL Light, Coq, Isabelle, etc., debería haber barrido esas dudas al demostrar concretamente que grandes áreas de las matemáticas pueden ser imitadas formalmente en la práctica y no solo en teoría.

Finalmente, permítanme mencionar que aunque creo que es muy razonable aceptar la Suposición Clave, es posible rechazarla. Quizás el más notablemente, el filósofo Michael Detlefsen ha desafiado la afirmación estándar de que la cadena Con(ZFC) imita adecuadamente la afirmación "ZFC es consistente" en el sentido de la Suposición Clave, y ha sugerido que el programa de Hilbert para probar la consistencia de las matemáticas aún no ha muerto. Creo que Detlefsen simplemente se equivoca y que no hay nada insatisfactorio en la cadena estándar Con(ZFC), pero al menos tiene razón en que aquí hay algo que verificar, y no es un punto puramente matemático sino parcialmente filosófico.

Answer 2

¿Aceptarías si Set1 simplemente demostrara la existencia de un modelo para Set2 (de la misma manera que Set1 demuestra la consistencia de la aritmética formalizada de Peano al proporcionar un modelo de ella)?

Si es así, y si aceptas en Set1 que hay un cardinal inaccesible κ, entonces el conjunto V_κ es un modelo de ZFC, demostrable en Set1. La mayoría de los teóricos de conjuntos hoy parecen creer que hay cardinales inaccesibles y "grandes cardinales" mucho más grandes en el universo de conjuntos. Así que cuentan esto como una prueba de la consistencia de ZFC, al igual que cuentan la existencia de los números naturales estándar como una prueba de la aritmética de Peano.

No necesitas ni siquiera asumir que Set1 tiene un cardinal inaccesible. Por ejemplo, podrías asumir que Set1 contiene toda la teoría de conjuntos de Morse-Kelley y Set2 consta de ZFC, y luego Set1 demostraría la consistencia de Set2.

Lo que no puedes hacer es demostrar la consistencia de Set2 dentro de Set1 utilizando solo técnicas que puedan ser formalizadas dentro de Set2. Esto no es diferente a la aritmética de Peano: podemos demostrar formalmente que la aritmética de Peano es consistente, pero no utilizando métodos que puedan ser formalizados en la propia aritmética de Peano. El hecho de que te interese la teoría de conjuntos solo hace que el problema parezca más complicado; el fenómeno subyacente no es muy diferente.

Answer 3

¿Hay alguna razón para creer que Set1 no puede probar la consistencia de Set2? ¿O simplemente estoy confundido y lo que dije no tiene sentido?

Lo que estás preguntando sí tiene sentido, pero existen buenas razones informales pero rigurosas para creer que Set1 (matemáticas informales) no puede probar la consistencia de Set2 (una formalización de "todo lo que queremos" de las matemáticas informales).

La razón es que podemos reformular el resultado de incompletitud de Gödel en términos del Problema de Detención, de modo que poder dar una prueba informal de consistencia equivale a dar algún método físico para decidir si los programas de máquinas de Turing arbitrarias se detienen. La existencia de tal método implicaría que la hipótesis de Church-Turing es falsa, lo cual es una afirmación sobre el mundo físico que actualmente parece muy improbable que sea verdadera.

Answer 4

Tu pregunta plantea dos cuestiones interesantes: una de formalización, otra de externalización/reflexión. El primer contiene un problema real, pero más filosófico que matemático; el segundo es donde creo que radica el contenido matemático de tu pregunta, y tiene una respuesta positiva.

---

Das en el clavo en el primer punto cuando señalas: "por supuesto, uno podría argumentar simplemente que Conjunto1, al no estar formalizado, no es susceptible a investigación matemática," y no creo que tu siguiente punto responda completamente esa pregunta: discutes los problemas de externalización del teorema de Gödel, pero eso es separado de la cuestión de formalización. Pides una razón para creer que Conjunto1 no prueba algo - ¿cómo podríamos esperar dar eso sin discutir Conjunto1 como un objeto preciso en alguna meta-teoría?

Afortunadamente, no necesitamos postular un Conjunto0 para esto y terminar con el mismo problema una tortuga más abajo. Para formalizar los fundamentos de la teoría de la prueba, solo necesitamos poder hablar sobre la manipulación de cadenas de símbolos, por lo que una teoría de los números naturales (por ejemplo, PA o incluso HA) es más que suficiente. Por otro lado, sí debemos suponer alguna meta-teoría dada (como la llamarían la mayoría de los lógicos tradicionales) o marco lógico (como lo harían muchos informáticos) para poder avanzar, y en realidad tenemos el problema de que no podemos hablar sobre ella como un objeto en sí sin pasar a una meta-meta-teoría. Este es un problema real, pero más filosófico que matemático: simplemente debemos aceptar una regresión infinita potencial, o dar un salto de fe de que los hechos probados dentro de nuestra meta-teoría, sobre alguna versión interna de ella, se aplicarán a la meta-teoría misma (ya sea que se trate de un objeto platónico, un sistema computacional físico, o cualquier otra cosa).

---

La segunda cuestión es la reflexión, y tiene una resolución más satisfactoria. (Mantendré la meta-teoría informal, pero HA sería más que suficiente para formalizar esto, creo.) Digamos que tenemos algunos axiomas para Conjunto1, lo suficientemente fuertes como para contener una "copia interna" de los números naturales y por lo tanto poder hablar sobre teoría básica de la prueba; entonces definimos Conjunto2 como la "versión interna" de la misma teoría en Conjunto1, y así sucesivamente. Ahora podemos probar:

Lema. (Una instancia de un principio de reflexión para demostrabilidad.) Si Conjunto1 prueba "Conjunto2 es consistente", entonces también prueba "Conjunto2 prueba 'Conjunto3 es consistente'".

(Este es un buen ejercicio de internalización; esencialmente proviene del hecho de que "ser una prueba" es una propiedad muy directa, y por lo tanto robusta bajo la internalización.)

Ahora, si Conjunto1 es capaz de probar el teorema de Gödel para Conjunto2 (en la forma en que lo planteas, es decir, "si Conjunto2 prueba la consistencia de Conjunto3, entonces Conjunto2 es inconsistente"), podemos deducir el teorema de Gödel para Conjunto1 de la siguiente manera:

Supongamos que Conjunto1 prueba Conjunto2. Por la proposición anterior, Conjunto1 también prueba "Conjunto2 prueba Conjunto3". Ahora, por el teorema de Gödel para Conjunto2, podemos deducir (todavía en Conjunto1) el teorema "Conjunto2 es inconsistente". Pero ahora tenemos pruebas en Conjunto1 tanto de Con(Conjunto2) como de su negación; por lo que Conjunto1 es inconsistente. QED

Así que tu pregunta tiene una respuesta positiva: si se nos permite razonar matemáticamente sobre Conjunto1 en absoluto, entonces sí, tenemos razones para creer que no prueba la consistencia de Conjunto2.

Answer 5

Creo que estás describiendo un proceso que es una descripción bastante precisa de cómo los teóricos de conjuntos suelen pensar en cuestiones de consistencia, donde Set1 es la explicación informal de la jerarquía acumulativa, tal como se ilustra en nuestras otras investigaciones formales, Set2 es ZFC y Set3 no es uno, sino una familia de teorías de conjuntos más fuertes obtenidas mediante algo similar a tu proceso de reflexión de vuelta en Set1, a la cual llamaré Set3*.

La principal diferencia es que los lógicos no hablarán de que Set1 pruebe algo, porque no tiene ningún tipo de teoría de la prueba, como otros han indicado en tu respuesta. En cambio, Set1 "justificará" los axiomas de Set2, y "fundamentará" o "sugerirá" axiomas propuestos para Set3*.

Así que lo que entiendo de tu discusión sobre la aplicación de la incompletitud es (i) una indicación adicional de que Set1 no tiene teoría de la prueba, ya que es una fuente abundante y falible de nueva fuerza probatoria, (ii) que la jerarquía Gödeliana de fuerza probatoria debe ser una guía cuando investigamos las teorías en Set3*, y (iii) realmente no hay ningún indicio de un modelo, aparte de los que obtenemos de las axiomatizaciones cortesía del teorema de completitud.

Creo que es esclarecedor contrastar el estado de la consistencia de la teoría de conjuntos con la de la aritmética, donde Gentzen dio una prueba teórico-pragmática de consistencia directamente fundamentada en la intuición combinatoria. Allí, Arith1, nuestra intuición aritmética, desempeña un papel más directo para apuntalar Arith2, la Aritmética de Peano, y donde el análisis de la jerarquía Gödeliana muestra que la consistencia de la teoría es equivalente en fuerza a la verdad del principio combinatorio elemental. Desafortunadamente, no sabemos cómo construir tales principios combinatorios lo suficientemente fuertes como para demostrar la consistencia de ZFC.