logo

Substitution Axiom Form 📂Set Theory

Substitution Axiom Form

Axiom

X(xX!y(p(x,y))    YxXyY(p(x,y))) \forall X \left( \forall x \in X \exists ! y \left( p(x,y) \right) \implies \exists Y \forall x \in X \exists y \in Y \left( p(x,y) \right) \right) The range exists for all functions.


Explanation

Although propositional function p(x,y)p(x,y) is a function, strictly speaking, it has not yet been defined as a function, and even if it were defined as a function, it is not the function itself mentioned in the axiom above. What logical expression p(x,y)p(x,y) conveys is that when xXx \in X is given, yYy \in Y exists:

  • For instance, pp can be given as p(x,y):y=2xp(x,y): y = 2x, and in this case, the function that has a range is f(x)=2xf(x) = 2x, not p(x,y)p(x,y). It is the image Y=f[0,1]=[0,2]Y = f [ 0 ,1] = [0,2] of X=[0,1]X = [0,1] for the function ff that exists according to the substitution axiom form.

The reason why it is called an axiom form rather than an axiom is because this axiom exists innumerably for innumerably many p(x,y)p(x,y). If there are two different propositional functions, p1(x,y):y=sinxp_{1}(x,y): y = \sin x and p2(x,y):y=2xp_{2}(x,y): y = 2x, the existence of Y=f2[0,1]=[0,2]Y = f_{2} [ 0,1] = [0,2] is guaranteed not by the ‘substitution axiom for p1(x,y)p_{1}(x,y)’ but by the ‘substitution axiom for p2(x,y)p_{2}(x,y)’.