Supongamos que queremos formalizar una proposición (es decir, a partir de la categoría de la teoría o modelo de la teoría) que tiene el "tamaño" de los problemas. Para la concreción, permite llevar la siguiente declaración como bastante típico ejemplo.
La proposición. El functor categoría $[\mathrm{Grp}, \;\mathrm{Set}]$ es completa.
Si nuestro elegido fundacional de la teoría ZFC, entonces podríamos estar tentados a formalizar la anterior proposición de la siguiente manera.
Primera Formalización del pedido. Para cada modelo de $V$ de ZFC, el functor categoría $[\mathrm{Grp}.\!V, \mathrm{Set}.\!V]$ $V$- completa.
(Si el significado de la anterior notación no está claro, por favor deje un comentario.) Sin embargo, hay otra manera de formalizar la proposición de interés, en el que podemos restringir los modelos de segundo orden.
Segundo-la Formalización del pedido. Para cada modelo de $V$ de los de segundo orden ZFC, el functor categoría $[\mathrm{Grp}.\!V, \mathrm{Set}.\!V]$ $V$- completa.
Tenga en cuenta que incluso si usamos algo más fuerte que ZFC, el problema no desaparece. Por ejemplo, supongamos que hemos elegido Tarski-Grothendieck la teoría de conjuntos (TG) como nuestro fundacional de la teoría. Bueno, hay tanto de primer y segundo orden versiones de TG, por lo tanto, hay dos maneras diferentes de formalización de la proposición de interés con respecto a la TG. Por lo tanto, mi pregunta es:
Pregunta. En general, que es la "correcta" de la formalización de la original propuesta? El primer fin de versión, o el segundo fin de versión? Y qué importa siquiera?
Además, si no hay una "tercera vía" que supera a los mencionados enfoques para la formalización de la propuesta, me gustaría saber.
