Substitution Axiom Form
Axiom
The range exists for all functions.
- The symbol signifies uniqueness.
- Here, is a propositional function in .
Explanation
Although propositional function 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 conveys is that when is given, exists:
- For instance, can be given as , and in this case, the function that has a range is , not . It is the image of for the function 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 . If there are two different propositional functions, and , the existence of is guaranteed not by the ‘substitution axiom for ’ but by the ‘substitution axiom for ’.