¿Son los conjuntos y los símbolos los componentes básicos de las matemáticas?

Las cosas que realmente escribes en el papel o en algún otro medio no se pueden definir como ningún tipo de objetos matemáticos. Las estructuras matemáticas se pueden usar como máximo para modelar (o aproximar) las estructuras del mundo real. Por ejemplo, podríamos decir que podemos tener cadenas de símbolos de longitud arbitraria, pero en el mundo real nos quedaríamos sin papel, tinta, átomos o lo que sea que usemos para almacenar nuestras representaciones físicas de cadenas.

Entonces, veamos qué podemos construir de forma no circular y en qué orden.

Lenguaje natural

En última instancia, todo se reduce al lenguaje natural. Simplemente no podemos definir todo antes de usarlo. Por ejemplo, no podemos definir "definir"... Sin embargo, lo que esperamos hacer es usar la menor cantidad posible de conceptos intuitivos (descritos en lenguaje natural) para iniciar sistemas formales que sean más "poderosos". Vamos a empezar.

Números naturales y cadenas

Simplemente asumimos las propiedades habituales de los números naturales (aritmética y orden) y las cadenas (extracción de símbolos, longitud y concatenación). Si ni siquiera asumimos esto, no podemos manipular cadenas y no podemos definir ninguna sintaxis en absoluto. Es conveniente suponer que cada número natural es una cadena (por ejemplo, usando codificación binaria).

Especificación del programa

Elija cualquier lenguaje de programación razonable. Un programa es una cadena que especifica una secuencia de acciones , cada una de las cuales es un paso básico de manipulación de cadenas o un salto condicional . En un paso básico de manipulación de cadenas, podemos referirnos a cualquier cadena por su nombre . Inicialmente, todas las cadenas nombradas en el programa están vacías, excepto la cadena nombrada$input$, que contiene la entrada al programa. Un salto condicional nos permite probar si alguna condición básica es verdadera (digamos que un número es distinto de cero) y saltar a otro paso en el programa si es así. Fácilmente podemos implementar un$k$-doble iteración de una secuencia de acciones mediante el uso de un contador de números naturales que se establece en$k$antes de esa secuencia y se reduce en$1$después de la secuencia, y saltando al comienzo de la secuencia siempre que$k$es distinto de cero. La ejecución de un programa en una entrada es simplemente seguir el programa (con$input$que contiene la entrada al principio) hasta que lleguemos al final, momento en el que se dice que el programa se detiene , y lo que sea que esté almacenado en la cadena denominada$output$se tomará como la salida del programa. (Es posible que el programa nunca llegue al final, en cuyo caso no se detiene. Tenga en cuenta que en este punto no queremos (todavía) afirmar que la ejecución de cada programa se detiene o no se detiene. En casos especiales, podríamos ser capaces de observar que no se detendrá, pero si no podemos saberlo, simplemente diremos "No sabemos". por ahora).

Una clase especial de programas son aquellos en los que los saltos condicionales solo se utilizan para realizar la iteración (de la manera descrita anteriormente). Estos programas siempre terminan en cada entrada, por lo que en cierto sentido son los más primitivos. De hecho, se les llama primitivos recursivos. También son los más aceptables en el sentido de que puede 'ver claramente' que siempre se detienen y, por lo tanto, está muy 'bien definido' hablar sobre la colección de cadenas que aceptan (la salida no es la cadena vacía), ya que siempre se detienen y aceptan o no aceptan. Llamamos a tales colecciones primitivas recursivas también. (Como nota al margen, hay programas que siempre se detienen pero no son recursivos primitivos).

Especificación formal del sistema

Ahora podemos usar programas para representar un sistema formal. Específicamente un sistema formal útil$T$tiene un idioma $L$, que es una colección recursiva primitiva de cadenas, aquí llamadas oraciones sobre$T$, algunos de los cuales se dice que son demostrables sobre$T$. A menudo$T$viene con un sistema deductivo , que consiste en reglas que rigen qué oraciones puedes probar dadas las oraciones que ya has probado. Podríamos expresar cada regla en la forma "$φ_1,φ_2,...,φ_k \vdash ψ$", que dice que si ya has probado$φ_1,φ_2,...,φ_k$entonces puedes probar$ψ$. Incluso puede haber infinitas reglas, pero la característica clave de un útil$T$es que hay un solo programa recursivo primitivo que se puede usar para verificar un solo paso deductivo , es decir, una sola aplicación de cualquiera de las reglas. En concreto, para tal$T$hay un programa recursivo primitivo$P$que acepta una cadena$x$si y si$x$codifica una secuencia de oraciones$φ_1,φ_2,...,φ_k,ψ$tal que$φ_1,φ_2,...,φ_k \vdash ψ$.

Dado que todos los sistemas formales útiles tienen un programa de este tipo, podemos verificar la afirmación de cualquiera de que una oración$φ$es demostrable$T$, siempre que proporcionen la secuencia completa de pasos deductivos, que es una posible forma de prueba .

Hasta ahora, vemos que todo lo que necesitamos para comprometernos filosóficamente es la capacidad de realizar (un número finito) de manipulaciones de cadenas, y podemos llegar al punto en el que podemos verificar las pruebas sobre cualquier sistema formal útil. Esto incluye los sistemas de primer orden PA y ZFC. En este sentido, claramente podemos hacer cualquier cosa que ZFC pueda hacer, pero si nuestras manipulaciones de cadenas tienen algún significado o no , no se puede responder sin un compromiso ontológico más fuerte.

Teoremas de incompletitud de Gödel

En este punto ya podemos 'obtener' los teoremas de incompletitud de Gödel, tanto en forma externa como interna. En ambos se nos da un sistema formal útil$T$eso también puede probar lo que PA pueda probar (bajo traducción adecuada). Dada cualquier oración$P$encima$T$, podemos construir una oración$Prov_T(P)$encima$T$que pretende decir "$P$es demostrable$T$Entonces dejamos$Con(T) = ¬Prov_T(\bot)$. Para 'obtener' la forma externa (si$T$prueba$Con(T)$entonces$T$prueba$\bot$), podemos escribir explícitamente un programa que da como entrada cualquier prueba de$Con(T)$encima$T$produce como salida una prueba de$\bot$encima$T$. Y para 'obtener' la forma interna podemos escribir explícitamente una prueba sobre$T$de la frase "$Con(T) \rightarrow \neg Prov_T(Con(T))$". (Vea esto para declaraciones más precisas de este tipo de resultado).

El problema es que la oración "$Prov_T(P)$"no tiene ningún sentido a menos que tengamos alguna noción de interpretación de una oración sobre$T$, que hemos evitado por completo hasta ahora para que todo sea puramente sintáctico. Llegaremos a una forma básica de significado en la siguiente sección.

Teoría básica del modelo

Digamos que queremos poder afirmar que cualquier programa dado en una entrada dada se detiene o no se detiene. Podemos hacerlo si aceptamos LEM (la ley del tercero excluido) . Con esto ahora podemos expresar propiedades básicas sobre$T$, por ejemplo, si es consistente (no prueba tanto una oración como su negación), y si es completo (siempre prueba una oración o su negación). Esto da sentido a los teoremas de incompletud de Gödel. De la forma externa, si$T$es realmente consistente entonces no puede probar$Con(T)$a pesar de$Con(T)$corresponde a través de la traducción a una afirmación sobre los números naturales que es verdadera iff$T$es consistente.

Pero si además queremos poder hablar sobre la colección de cadenas aceptadas por un programa (no solo las recursivas primitivas), esencialmente estamos pidiendo un axioma de comprensión de conjuntos más fuerte, en este caso$Σ^0_1$-comprensión (no sólo$Δ^0_0$-comprensión). El área de Matemática inversa incluye el estudio de la distinción entre axiomas de teoría de conjuntos tan débiles, y el artículo de Wikipedia vinculado menciona estos conceptos y otros de los que hablaré más adelante, pero una referencia mucho mejor es este breve documento de Henry Towsner . Con$Σ^0_1$-comprensión podemos hablar de la colección de todas las oraciones que son demostrables sobre$T$, mientras que antes podíamos hablar de una de esas oraciones pero no de toda la colección como un solo objeto.

Ahora, para probar el teorema de compacidad , incluso para la lógica proposicional (clásica), necesitamos aún más, a saber, WKL (lema de Konig débil) . Y dado que el teorema de compacidad es una consecuencia trivial del teorema de completitud (por ejemplo, para la deducción natural), también se requiere WKL para probar el teorema de completitud. Lo mismo ocurre con la lógica de primer orden.

Saltos de Turing

Ahora bien, realmente no tiene sentido desde un punto de vista filosófico tener sólo$Σ^0_1$-comprensión. Después de todo, eso es en cierto sentido equivalente a tener un oráculo para el problema de la detención (para los programas ordinarios), que es el primer salto de Turing . El problema de la detención es indecidible , lo que significa que no hay ningún programa que siempre se detenga en cualquier entrada.$(P,x)$y acepta si y si$P$se detiene en$x$. Al permitir$Σ^0_1$-comprensión estamos en cierto sentido obteniendo acceso a tal oráculo. Pero entonces, si consideramos los programas aumentados a los que se les permite usar el primer salto de Turing (obtendrá la respuesta en un solo paso), el problema de la detención de estos programas volverá a ser indecidible para cualquiera de ellos, pero podemos concebir un oráculo. por eso también, que es el segundo salto de Turing. Dado que permitimos el primero, no hay una buena razón para prohibir el segundo. Etcétera.

El resultado final es que también podríamos aceptar la comprensión aritmética completa (podemos construir cualquier conjunto de cadenas o números naturales definibles por una fórmula donde todos los cuantificadores están sobre cadenas o números naturales). Y desde una perspectiva metalógica, también deberíamos tener el esquema de inducción de segundo orden completo , porque ya asumimos que solo hemos estado aceptando suposiciones que se cumplen para los números naturales estándar, es decir, aquellos que son expresables en la forma "$1+1+\cdots+1$".

Tenga en cuenta que todo hasta este punto puede considerarse predicativo , en el sentido de que en ningún momento construimos ningún objeto cuya definición dependa del valor de verdad de alguna afirmación que lo involucre (como a través de algún cuantificador cuyo rango incluye el objeto a construir). ). Por lo tanto, la mayoría de los lógicos inclinados constructivamente son perfectamente felices hasta aquí.

Teoría del modelo superior

Si solo acepta conjuntos predicativos contables como justificados ontológicamente, conjuntos de cadenas específicamente predicativos (o subconjuntos equivalentes de los números naturales), entonces lo anterior es prácticamente todo lo que necesita. Tenga en cuenta que desde el principio hemos asumido implícitamente un alfabeto finito para todas las cadenas. Esto implica que solo tenemos un número incontable de cadenas y, por lo tanto, no podemos tener cosas como sistemas formales con un número incontable de símbolos. Estos ocurren con frecuencia en la teoría de modelos superiores, por lo que si queremos poder construir algo incontable, necesitaríamos mucho más, como ZFC.

Un ejemplo del uso del poder de ZFC está en la construcción de modelos no estándar a través de ultrapoderes , que requieren el uso de un tipo débil del axioma de elección . Lo bueno de esta construcción es que es elegante y, por ejemplo, se puede ver que el modelo no estándar resultante de los reales captura muy bien la idea de usar secuencias de reales módulo alguna relación de equivalencia como modelo para el primer orden. teoría de los números reales, donde tener un comportamiento eventualmente consistente implica que se cumple la propiedad correspondiente. El ultrafiltro no constructivo es necesario para especificar si la propiedad se mantiene en el caso sin un comportamiento eventualmente consistente.

Espero haber demostrado de manera convincente que aunque necesitamos muy poco para comenzar a definir y usar un sistema formal, incluso ZFC, todo el empuje de símbolos carece de significado a menos que asumamos más, y cuanto más significado queramos expresar o probar , suposiciones más fuertes necesitamos. ZFC (excluyendo el axioma de fundación) es históricamente el primer sistema suficientemente fuerte que puede hacer todo lo que los matemáticos han estado haciendo, por lo que no sorprende que también se use como un metasistema para estudiar lógica. Pero no podrá justificar ontológicamente ZFC, si eso es lo que está buscando.

Conjuntos en teorías de conjuntos

Finalmente, su pregunta podría estar basada en un concepto erróneo común de que en ZFC tiene una noción de "conjunto". No precisamente. ZFC es solo otro sistema formal y no tiene ningún símbolo que represente "conjunto". Es simplemente que los axiomas de ZFC se hicieron para que parezca razonable suponer que se cumplen para alguna noción vaga de "conjuntos" en lenguaje natural. Dentro de ZFC, cada cuantificador cubre todo el dominio, por lo que no se puede hablar de conjuntos como si hubiera otros tipos de objetos. Si usamos un meta-sistema que no tiene conjuntos, entonces un modelo de ZFC podría no tener ningún 'conjunto' en absoluto, ¡cualquiera que sea el significado de "conjunto"!

En ZFC, no se puede hablar del "conjunto de Russell", ya que el axioma de comprensión no nos permite construir tal colección. En la teoría de conjuntos MK (Morse-Kelley), hay una noción interna de conjuntos, y uno puede construir cualquier clase de conjuntos definible por alguna fórmula, pero uno no puede construir nada que se asemeje a una "clase de clases" por la misma razón que la de Russell. paradoja.

En la NFU de la teoría de conjuntos no convencional, uno tiene tanto conjuntos como urelements (la extensionalidad solo se aplica a los conjuntos), por lo que puede tener sentido hablar de conjuntos aquí. Pero NFU no es un sistema muy fácil de usar de todos modos.

Y aquí es también donde mi respuesta se detendrá.