¿Cuál es la definición de la función en ZF/ZFC?

Question

En ZF hay axioma esquema de sustitución, que puede ser enunciada como

la imagen de un conjunto bajo cualquier función definibles también caen dentro de un conjunto

Hay una definición del concepto de función en ZF/ZFC? ¿Qué es? Me refiero a set-teóricamente hablando. Es decir, en la ingenua teoría de la función puede ser entendida como un conjunto de pares (triples, etc.), pero, ¿qué acerca de ZF/ZFC?

Answer 1

Hay dos diferentes nociones que son llamados "función". Una función internamente a ZFC es un conjunto de pares, donde el primer elemento del par es entendido para ser asignado a la segunda por la función. Por ejemplo, la función sucesor $S :\mathbb N \to \mathbb N$ es una función internamente en ZFC, y está dada por $$ S = \{(n,m) \in \mathbb N \times \mathbb N \mid m = n + 1\}. $$ Sin embargo, la función del axioma esquema de sustitución se refiere a una función en el universo dada por una fórmula. Ligeramente simplificado, si $\phi(x,y)$ es una fórmula con dos variables que ZFC demuestra que $\forall x \exists y \phi(x,y)$$\forall x \forall y \forall y'(\phi(x,y) \land \phi(x,y') \to y = y')$, entonces no es una instancia del esquema de axioma de reemplazo de la cual los estados $$ \forall X \existe Y(\forall x\forall y(\phi(x,y) \de la tierra x \X \a y \Y)). $$