¿Qué tipo de fundamentos utilizan los matemáticos para demostrar los metateoremas?

Question

La teoría de conjuntos de Zermelo-Fraenkel (con elección) se acepta comúnmente como el fundamento estándar de las matemáticas. Se trata de una teoría de conjuntos material. Para cada dos objetos/conjuntos $a,b$ cabe preguntarse si $a=b$ o no. Además, siempre se puede preguntar si $a\in b$ es cierto o no. Así que $\in$ es un relación global de elementos .

Como fundamento alternativo para la teoría de conjuntos, Shulman propuso SEAR . Es un teoría estructural de conjuntos . Es decir, los elementos no tienen estructura interna, es decir, son sólo "puntos abstractos". Se tiene una declaración de tipo $a\colon A$ por decir que $a$ es un elemento de $A$ . Pero esto no se puede negar, así que $\colon$ no es relación . Pero si $A$ es un conjunto (¿debería decir "conjunto abstracto" para enfatizar el punto de que quiero decir "conjunto en una teoría estructural de conjuntos"?), entonces se tiene un relación de elemento local $\in_A$ para cada elemento $a$ en $A$ y cada subconjunto $B$ de $A$ (= función $A\to 2:=\{0,1\}$ ), la declaración $a\in_A B:\iff B(a)=1$ es verdadero o falso.

En la página de SEAR que he enlazado antes, hay una prueba (supongo que debida a Shulman) que demuestra que SEAR y ZF son básicamente equivalentes: a partir de un modelo de ZF se puede construir un modelo de SEAR y viceversa. Se trata de un teorema meta. Pero, ¿en qué fundamento tiene lugar la demostración de tal metateorema? ¿Es este metafundamento una teoría de conjuntos estructural o material?

Answer 1

Su pregunta es mucho más concreta de lo que sugiere su título. En cuanto a la pregunta en sí, mi respuesta es que no importa. La prueba se da en matemáticas, no en ningún sistema formal. Una base matemática, para serlo, debe ser capaz de formalizar la mayoría de los argumentos matemáticos ordinarios. Por lo tanto, cualquier fundamento de las matemáticas podría utilizarse para formalizar un metateorema de este tipo.

Dicho esto, algunas personas se preguntan si los metateoremas de este tipo pueden formalizarse en teorías muy débiles. No hay nada malo en ello, pero no es algo a lo que yo dedique mi tiempo, y en particular no pensé en ello cuando escribí la prueba a la que te refieres. Lo más cerca que llegué fue a señalar que, en lugar de una "construcción de un modelo", la prueba puede considerarse equivalentemente como una traducción de fórmulas de primer orden. Si estás interesado en este tipo de cuestiones, la respuesta de Nik me parece razonable, pero no estoy familiarizado con los detalles de este tipo de cosas.

Answer 2

Una dirección podría ser la siguiente. Deje que ${\rm ZFC}^+$ sea la teoría en el lenguaje de la teoría de conjuntos aumentada por un símbolo constante ${\bf M}$ con los axiomas

$\bullet$ cada axioma de ${\rm ZFC}$

$\bullet$ " ${\bf M}$ es contable y transitivo"

$\bullet$ la relativización de todo axioma de ${\rm ZFC}$ a ${\bf M}$ .

Entonces se puede demostrar ${\rm Con}({\rm ZFC}) \Rightarrow {\rm Con}({\rm ZFC}^+)$ en aritmética Peano, y basándonos en la página que has enlazado, parece que se puede demostrar directamente la consistencia de cualquier fragmento finito de ${\rm SEAR}$ en ${\rm ZFC}^+$ . Por lo tanto, se puede demostrar ${\rm Con}({\rm ZFC}) \Rightarrow {\rm Con}({\rm SEAR})$ en aritmética Peano. (Si ${\rm SEAR}$ no fueran consistentes entonces algún fragmento finito ${\rm SEAR}_0$ sería incoherente, y este hecho sería verificable en ${\rm ZFC}^+$ de modo que ${\rm ZFC}^+$ demostraría tanto ${\rm Con}({\rm SEAR}_0)$ y $\neg{\rm Con}({\rm SEAR}_0)$ y, por tanto, ser incoherente). Para más detalles, véase el capítulo 7 de mi libro .

Imagino que un argumento similar funcionaría en sentido inverso para demostrar ${\rm Con}({\rm SEAR}) \Rightarrow {\rm Con}({\rm ZFC})$ en aritmética Peano, pero no estoy familiarizado con ${\rm SEAR}$ así que no puedo asegurarlo.