|
A [[function (set theory)|functional relation]] is a [[binary predicate]] <math>F</math> such that <math>\forall x, y, z\,\left(xFy \wedge xFz \to y = z\right)</math>. Such a [[Relation (mathematics)|relation]] ([[Predicate (logic)|predicate]]) is implemented as a relation (set) exactly as described in the previous section. So the predicate <math>F</math> is implemented by the set <math>\left\{\left(x, y\right) : xFy\right\}</math>. A set of ordered pairs <math>F</math> is a function if and only if <math>\forall x, y, z\,\left(\left(x, y\right) \in F \wedge \left(x, z\right) \in F \to y = z\right)</math>. It is therefore possible to define this function <math>F\!\left(x\right)</math> as the unique object <math>y</math> such that <math>xFy</math> – i.e.: <math>x</math> is <math>F</math>-related to <math>y</math> such that the relation <math>f</math> holds between <math>x</math> and <math>y</math> – or as the unique object <math>y</math> such that <math>\left(x, y\right) \in F</math>. The presence in both theories of functional predicates which are not sets makes it useful to allow the notation <math>F\!\left(x\right)</math> both for sets <math>F</math> and for important functional predicates. As long as one does not quantify over functions in the latter sense, all such uses are in principle eliminable.
In [[New Foundations|NFU]], <math>x</math> has the same type as <math>F\!\left(x\right)</math>, and <math>F</math> is three types higher than <math>F\!\left(x\right)</math> (one type higher, if a type-level ordered pair is used). To solve this problem, one could define <math>F\left[A\right]</math> as <math>\left\{y : \exists x\,\left(x \in A \wedge y = F\!\left(x\right)\right)\right\}</math> for any set <math>A</math>, but this is more conveniently written as <math>\left\{F\!\left(x\right) : x \in A\right\}</math>. Then, if <math>A</math> is a set and <math>F</math> is any functional relation, the '[[axiomAxiom of replacement|Axiom of Replacement]]' assures that <math>F\left[A\right]</math> is a set in [[ZFC]]. In NFU, <math>F\left[A\right]</math> and <math>A</math> now have the same type, and <math>F</math> is two types higher than <math>F\left[A\right]</math> (the same type, if a type-level ordered pair is used).
The function <math>I\!\left(x\right) = x</math> is not a set in [[ZFC]] because it is '"too large".' <math>I\!\left(x\right)</math> is, however, a set in NFU. The function (predicate) <math>S\!\left(x\right) = \left\{x\right\}</math> is neither a function nor a set in either theory; in ZFC, this is true because such a set would be too large, and, in NFU, this is true because its definition would not be [[Stratified formula#In set theory|stratified]]. Moreover, <math>S\!\left(x\right)</math> can be proved not to exist in NFU (see the resolution of [[Cantor's paradox]] in [[New Foundations]].)
=== Operations on functions ===
Let <math>f</math> and <math>g</math> be arbitrary functions. The '''[[function composition|composition]]''' of <math>f</math> and <math>g</math>, <math>g \circ f</math>, is defined as the relative product <math>f \mid ,|\,g</math>, but only if this results in a function such that <math>g \circ f</math> is also a function, with <math>\left(g \circ f\right)\!\left(x\right) = g\!\left(f\!\left(x\right)\right)</math>, if the range of <math>f</math> is a subset of the ___domain of <math>g</math>. The '''[[inverse function|inverse]]''' of <math>f</math>, <math>f^\left(-1\right)</math>, is defined as the [[inverse relation|converse]] of <math>f</math> if this is a function. Given any set <math>A</math>, the identity function <math>i_A</math> is the set <math>\left\{\left(x, x\right) \mid x \in A\right\}</math>, and this is a set in both [[ZFC]] and [[New Foundations|NF]] for different reasons.
=== Special kinds of function ===
A function is an '''[[Injective function|injectioninjective]]''' and(also called '''[[bijection|one-to-one]]''') if it has an inverse function.
If <math>A</math> and <math>B</math> are sets, <math>f</math> is a '''function from <math>A</math> to <math>B</math>''' if <math>f</math> is a function whose ___domain is <math>A</math>, and whose range is included in <math>B</math>.
|
