|
== Functions ==
A [[function (set theory)|functional relation]] is a [[binary predicate]] ''<math>F''</math> such that <math>\forall x, y, z\,\left(x F yxFy \wedge x F zxFz \rightarrowto 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) \mid: x F yxFy\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 \rightarrowto y = z\right)</math>. DefineIt ''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.: (if there<math>x</math> is one)<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). ForTo anysolve setthis ''A''problem, one could define <math>F\left[A\right]</math> as <math>\left\{y \mid: \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) \mid: x \in A\right\}</math>. IfThen, ''if <math>A''</math> is a set and ''<math>F''</math> is any functional relation, 'the '[[axiom of replacement|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 notneither a function (nor a set) in either theory; in ZFC, this is true because itsuch isa set would be too large;, and, in NFU, this is true because its definition iswould unstratifiednot 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>, ''f''<supmath>−1f^\left(-1\right)</supmath>, 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]], but for different reasons.
=== Special kinds of function ===
A function is an '''[[Injective function|injection]]''' and '''[[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>.
If ''<math>f''</math> is a function from ''<math>A''</math> to ''<math>B''</math>, ''<math>f''</math> is a:
* '''[[Injective function|Injection]]''' from ''<math>A''</math> to ''<math>B''</math> if the [[image (mathematics)|image]]s under ''<math>f''</math> of distinct members of ''<math>A''</math> are distinct members of ''<math>B''</math>.
* '''[[Surjection]]''' from ''<math>A''</math> to ''<math>B''</math> if the range of ''<math>f''</math> is ''<math>B''</math>.
* '''[[Bijection]]''' from ''<math>A''</math> to ''<math>B''</math> if ''<math>f''</math> is both an injection and a surjection.
This terminology adjusts for the fact that a function, as defined above, does not determine its codomain.
| 