Content deleted Content added
Joel Brennan (talk | contribs) |
Joel Brennan (talk | contribs) →Functions: explained more clearly that a function does not determine its codomain |
||
Line 92:
== Functions ==
A '''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 relation <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 the value 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.
Outside of formal set theory, we usually specify a function in terms of its ___domain and codomain, as in the phrase "Let <math>f: A \to B</math> be a function". The ___domain of a function is just its ___domain as a relation, but we have not yet defined the codomain of a function. To do this we introduce the terminology that a function is '''from <math>A</math> to <math>B</math>''' if its ___domain equals <math>A</math> and its range ''is contained in'' <math>B</math>. In this way, every function is a function from its ___domain to its range, and a function <math>f</math> from <math>A</math> to <math>B</math> is also a function from <math>A</math> to <math>C</math> for any set <math>C</math> containing <math>B</math>.
Indeed, no matter which set we consider to be the codomain of a function, the function does not change as a set since by definition it is just a set of ordered pairs. That is, a function does not determine its codomain by our definition. If one finds this unappealing then one can instead define a function as the ordered pair <math>(f, B)</math>, where <math>f</math> is a functional relation and <math>B</math> is its codomain, but we do not take this approach in this article (more elegantly, if one first defines ordered triples - for example as <math>(x, y, z) = (x, (y, z))</math>- then one could define a function as the ordered triple <math>(f, A, B)</math> so as to also include the ___domain). Note that the same issue exists for relations: outside of formal set theory we usually say "Let <math>R \subseteq A \times B</math> be a binary relation", but formally <math>R</math> is a set of ordered pairs such that <math>\text{dom}\,R \subseteq A</math> and <math>\text{ran}\,R \subseteq A</math>.
In 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 [[Axiom 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).
Line 98 ⟶ 102:
=== 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\,|\,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
=== Special kinds of function ===
A function is an '''[[injective]]''' (also called '''[[bijection|one-to-one]]''') if it has an inverse function.
* '''[[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.
Defining functions as ordered pairs <math>(f, B)</math> or ordered triples <math>(f, A, B)</math> has the advantages that we do not have to introduce the terminology of being a function "from <math>A</math> to <math>B</math>", and that we can speak of "being surjective" outright as opposed to only being able to speak of "being surjective onto <math>B</math>".
== Size of sets ==
| |||