Si realmente queremos considerar conjuntos finitos, queremos no sólo que sean finitos, sino también que sus elementos sean finitos, y los elementos de sus elementos sean finitos, y así sucesivamente. En resumen, queremos que el cierre transitivo del conjunto sea finito. (Cuando el cierre transitivo de un conjunto $x$ es el conjunto más pequeño $y$ tal que $x\subseteq y$ y $t\in s\in y\rightarrow t\in y$ .)
En un modelo de $\sf ZFC$ podemos definir el conjunto de todos los conjuntos hereditariamente finitos. Esto se denota comúnmente por $V_\omega$ . Es un conjunto contable, y de hecho es exactamente la unión [creciente] de $\mathcal P^n(\varnothing)$ la operación de conjunto de potencia iterada del conjunto vacío.
Para añadir más sobre esto, $V_\omega$ satisface todos los axiomas de $\sf ZFC$ excepto el axioma del infinito, y sí satisface su negación: no hay conjuntos inductivos, y por tanto tampoco hay conjuntos infinitos. Lo mismo ocurre con esta teoría, $\sf ZFC$ ¿con el axioma del infinito sustituido por su negación es suficiente para decidir qué son conjuntos finitos?
En general, parece que sí. Pero como cualquier teoría de primer orden con infinitos modelos, podemos producir modelos de la misma teoría tan grandes como queramos, y eso no es muy bueno. Pero al igual que con los números reales, o con $\sf PA$ podemos pasar a la lógica de segundo orden (con semántica completa) y tener una teoría categórica.
Modificamos ligeramente nuestra teoría, y en lugar del esquema de sustitución para conjuntos definibles, añadimos un axioma de segundo orden completo de $\in$ -inducción:
$$\forall A(\varnothing\in A\land\forall x(\forall y(y\in x\rightarrow y\in A)\rightarrow x\in A)\rightarrow\forall x(x\in A))$$ Cada clase $A$ tal que $\varnothing$ es miembro de $A$ y para cada $x$ siempre que todos los miembros de $x$ están en $y$ entonces $x$ es a su vez un miembro de $A$ entonces $A$ es el universo entero.
Esto debe ser, si no me equivoco, a una formulación de segundo orden del esquema de sustitución, aunque no recuerdo la prueba en este momento.
¿Por qué esto garantiza que sólo hay un modelo? Supongamos que $M$ era un modelo de nuestra teoría modificada, entonces tiene una operación de conjunto de potencia definida naturalmente y un conjunto vacío. Construcción por recursión $V_\omega$ como la unión de las iteraciones finitas de $\mathcal P^n(\varnothing)$ y tenemos una clase que satisface el supuesto de este axioma de inducción. Por lo tanto, ¡debe ser igual a todo el universo!
Nótese que la prueba anterior ocurre en el exterior el modelo $M$ . Muy parecido a la prueba de que sólo hay un modelo de $\sf PA_2$ se produce fuera $\Bbb N$ .
Me parece que esta teoría es razonable para captar lo que es verdaderamente finito en el universo de los conjuntos.
