¿Es necesario sustituir el argumento del objeto pequeño?

Question

¿Es necesario el axioma de sustitución en el argumento del objeto pequeño y en el construcción transfinita de álgebras libres ?

Mi motivación para la pregunta es que he oído que el axioma de sustitución nunca es necesario en la práctica.

Si la respuesta es "sí", ¿cómo se puede evitar el axioma de sustitución en las aplicaciones prácticas de estos dos teoremas?

Nótese que no se pueden usar ordinales si no se permite el axioma de sustitución (creo).

Answer 1

De la forma en que se suele presentar, ciertamente sí. Como señalas, suele referirse a ordinales regulares posiblemente incontables, lo que normalmente significaría ordinales de von Neumann. Una vez que se tiene el ordinal regular, digamos $\kappa$ Entonces, independientemente de si $\kappa$ es un ordinal de von Neumann o simplemente un conjunto bien ordenado, hay que definir una secuencia de objetos $K_\alpha$ para cada $\alpha < \kappa$ y tomar colimits en cada etapa de límite, y en general al final. Este tipo de argumento parece requerir una sustitución, por lo que veo. Ciertamente es posible definir una secuencia de conjuntos, incluso de longitud $\omega$ cuyo colímite no existe de forma demostrable en la categoría de conjuntos bajo $\mathbf{ZFC}$ menos la sustitución (ya que $V_{\omega + \omega}$ es un modelo de esa teoría, y podemos definir la secuencia $K_n := V_{\omega + n}$ ).

Por otro lado, existen dos versiones alternativas del argumento del objeto pequeño en Swan, Tipos W con reducciones y el argumento del objeto pequeño que no utilizan el reemplazo (y tampoco utilizan definiciones por recursión en universos de tipos pequeños, que es, a grandes rasgos, la versión teórica del reemplazo). La primera puede llevarse a cabo en un topos con objeto de número natural y que satisfaga el principio de elección $\mathbf{WISC}$ que creo que se mantiene para cualquier topos de Grothendieck bajo los supuestos de $\mathbf{ZFC}$ menos la sustitución. La segunda es específica para el caso de cofibraciones generadoras mónicas en topos de preseaf, pero no requiere $\mathbf{WISC}$ por lo que funcionaría en una metateoría de $\mathbf{ZF}$ menos la sustitución. Ambos argumentos son para una definición ligeramente no estándar de cofibrante generado, y tienen un formato diferente a la prueba habitual usando ordinales. En lugar de definir una secuencia de objetos a lo largo de un ordinal, sólo hay dos pasos, primero definir un $W$ -y, a continuación, se cotizan (para el primer argumento) o se extrae un subobjeto (para el segundo).