Considere la posibilidad de la expresión de $g(f(x)).$ Su fácil dibujar esto en un diagrama de árbol; el nodo inferior es $x$, por encima de eso es $f$, y por encima de eso es $g$.
Ahora, considere el $(D(f))(x),$ por ejemplo, imagine que $D$ denota la diferenciación. Si intenta dibujar esto como un árbol, usted conseguirá el "paréntesis" en su árbol. (¡Inténtelo!)
Para evitar estos soportes, la mejor manera es probablemente introducir una "función de evaluación" $\mathrm{eval}(*,*)$ tal que $\mathrm{eval}(f,x) = f(x)$ tan larga como esta expresión se define. Luego tenemos a $$(D(f))(x) = \mathrm{eval}(D(f),x)$$
y podemos sacar esto como un árbol bien. Problema resuelto!
Sin embargo, para formalizar esta en ZFC, que tendría que restringir la definición de $\mathrm{eval}$ a funciones de $f$ que son "internos" a la teoría. En particular, teoremas como $$\mathrm{eval}(\mathrm{eval},(f,x)) = f(x)$$
ni siquiera son gramaticalmente coherente. Esto parece moderadamente despilfarro de lo que parece ser perfectamente legítima (aunque trivial) teorema. Probablemente, no son similares pero menos trivial - teoremas demostrables en un auto-referencial del lenguaje que permite este tipo de cosas.
Por lo tanto, mi pregunta es, hay un simple formalismo en el cual la auto-referencial definiciones como la de arriba se puede hacer con seguridad? Tendría que ser sólo lo suficientemente restrictivo para bloquear Russell-como paradojas, pero no de manera restrictiva, así como para bloquear nuestra capacidad para definir la auto-referencial funciones como $\mathrm{eval}, \mathrm{identity}, \mathrm{domain}, \mathrm{range}, \mathrm{kernel}$ etc.
Discusión. Lo que realmente nos gusta es el de ser capaces de afirmar que el $$\mathrm{eval}(f,x) = f(x)$$
para todas las funciones de $f,$ incluyendo funciones como $\mathrm{eval}, \mathrm{identity}, \mathrm{domain}, \mathrm{range}, \mathrm{kernel}$ etc.
Sin embargo, sólo permitiendo la definición-por-los casos conduce a Russell como paradojas. Por ejemplo, supongamos que existe un no-función, se $3$ para la concreción (vamos a suponer que $3$ no es una Iglesia numeral para este argumento para el trabajo!). Ahora definir una función $g$ por casos como el siguiente.
$$f(f)=f \rightarrow g(f) = 3$$ $$f(f)\neq f \rightarrow g(f) = f.$$
Se trata de evaluar $g(g)$ y obtendrás una contradicción.
En los comentarios, Qiaochu sugirió el uso del cálculo lambda y/o un punto fijo combinador para definir dichas funciones. Estoy un poco inseguro de lo que sería similar y/o cómo proceder. Por ejemplo, supongamos que tenemos un primer orden de la teoría de la $T$, como ZFC, ¿cómo podemos extender este con una función como $\mathrm{eval}$? Desde la lógica de primer orden no tiene soporte para este tipo de cosas, realmente no puedo concebir cómo podría hacer esto.
