Esta función crece realmente rápido: ¡no hay ninguna función computable que lo limite!
Para ver esto, observe que si tuviéramos un límite computable para $f$ podemos saber si una frase $\sigma$ es coherente con $\mathsf{ZFC}$ (basta con buscar en todas las pruebas de longitud $<f(\vert\sigma\vert+1)$ para un $\mathsf{ZFC}$ -prueba de $\neg\sigma$ ). Pero a partir de esta información podríamos a su vez construir una extensión consistente completa computable de $\mathsf{ZFC}$ :
-
Fijar una enumeración adecuada $(\sigma_i)_{i\in\mathbb{N}}$ de las sentencias en el lenguaje de la teoría de conjuntos.
-
Definir una nueva secuencia $(\tau_i)_{i\in\mathbb{N}}$ de sentencias por recursión como sigue:
-
$\tau_0=\sigma_0$ si $\sigma_0$ es coherente con $\mathsf{ZFC}$ y $\tau_0=\neg\sigma_0$ de lo contrario.
-
$\tau_{i+1}=\sigma_{i+1}$ si $\sigma_{i+1}\wedge\bigwedge_{j\le i}\tau_i$ es coherente con $\mathsf{ZFC}$ y $\tau_{i+1}=\neg\sigma_{i+1}$ de lo contrario.
-
El conjunto $\{\tau_i:i\in\mathbb{N}\}$ es entonces una teoría completa computable y consistente que contiene $\mathsf{ZFC}$ (nota que cuando $\sigma_i$ es un axioma de $\mathsf{ZFC}$ tendremos $\tau_i=\sigma_i$ ).
Sin embargo, esto contradice el primer teorema de incompletitud. (O el teorema de Church, si quieres - básicamente lo anterior es la prueba del teorema de Church a partir del primer teorema de incompletitud).
Tenga en cuenta que realmente utilizamos muy poco sobre $\mathsf{ZFC}$ aquí. El primer teorema de incompletitud se aplica a un enorme gama de teorías, que van desde mucho más débiles que $\mathsf{ZFC}$ a mucho más fuerte que $\mathsf{ZFC}$ En resumen, cualquier teoría axiomatizable computacionalmente que satisfaga una "condición de fuerza" técnica muy suave (básicamente: al menos tan potente como Robinson's $Q$ ) está sujeta a este fenómeno. Véase la sección $4$ de este documento de Beklemishev para más detalles sobre este punto.
_Para ser precisos, la forma del primer teorema de incompletitud que estoy utilizando es: "Toda teoría consistente computablemente axiomatizable que interpreta el $\mathsf{Q}$ está incompleta". Tenga en cuenta que no necesitamos un $\omega$ -La suposición de consistencia aquí; aunque está presente en la prueba original de Godel, fue posteriormente eliminado por Rosser ._
6 votos
Parece que me han superado :P Pero voy a comentar aquí lo que habría puesto al final de mi respuesta: la función que describes está relacionada con el función de castor ocupado Y como los castores ocupados se enseñan en muchas clases de ciencias de la computación, probablemente tendrás más suerte buscando en Google, aunque no sea lo que te interesa.