Estoy buscando una referencia a la afirmación de que Lawvere's Teoría elemental de la categoría de conjuntos (ETCS) es igual a la aritmética de orden finito en cuanto a fuerza probatoria. La persona que me informó de esto dijo que era bien conocido en ciertos círculos, pero no pudo pensar en una referencia.
En realidad, todo lo que necesito es una referencia a una mitad de la equivalencia: que cualquier cosa demostrable en aritmética de orden finito es demostrable en ETCS. La historia: He estado mirando el documento de Colin McLarty Un fundamento aritmético de orden finito para la cohomología , lo que demuestra que no se necesita nada más fuerte que la aritmética de orden finito en ninguna parte de EGA o SGA. Quiero afirmar que no se necesita nada más fuerte que ETCS en ninguna parte de EGA o SGA. Para respaldar esto con referencias, necesito algo que relacione ETCS con la aritmética de orden finito.
Editar Esta pregunta ha generado muchos debates sobre el documento de McLarty. Estoy realmente interesado en esa discusión, pero también me gustaría enfatizar que es periférica a mi pregunta, que es simplemente una solicitud de referencia: ¿dónde puedo encontrar declarado/probado que ETCS es igual en fuerza a la aritmética de orden finito?
Edición adicional Tal vez pueda hacer esta pregunta más transparente para los expertos en teoría de conjuntos no categóricos. Es bien sabido que ETCS tiene la misma fuerza que la teoría basada en la membresía conocida como "Zermelo acotado con elección" o "Zermelo restringido con elección". (Una referencia: Mac Lane y Moerdijk, Haces en Geometría y Lógica , sección VI.10.) Los axiomas son la extensionalidad, el conjunto vacío, el emparejamiento, la unión, el conjunto potencia, el fundamento, la comprensión restringida, el infinito y la elección. Aquí "comprensión restringida" significa que sólo consideramos fórmulas que están restringidas en el sentido de que todos los cuantificadores son de la forma " $\forall x \in y$ " o " $\exists x \in y$ ".
