Difference between revisions of "Axiom schema of replacement"
From Maths
(A lot of work is required but its a start) |
m (Just added version without underbraces) |
||
| Line 16: | Line 16: | ||
-->\limplies}} {{M|\Big(<!-- | -->\limplies}} {{M|\Big(<!-- | ||
-->\underbrace{\forall X\exists Y\forall y\big[y\in Y\liff\exists x[x\in X\wedge\varphi(x,y,p)]\big]}_{y\in Y\iff\text{the 'image' of }x\text{ under the 'function' is }y }<!-- | -->\underbrace{\forall X\exists Y\forall y\big[y\in Y\liff\exists x[x\in X\wedge\varphi(x,y,p)]\big]}_{y\in Y\iff\text{the 'image' of }x\text{ under the 'function' is }y }<!-- | ||
| − | -->\Big)}} | + | -->\Big)}}<ref group="Note">Here it is without the underbraces: |
| + | * {{M|\Big(<!-- | ||
| + | -->\forall x\forall y\forall z\big[\big(\varphi(x,y,p)\wedge\varphi(x,z,p)\big)\limplies y\eq z\big]<!-- | ||
| + | -->\Big)}} {{M|<!-- | ||
| + | -->\limplies}} {{M|\Big(<!-- | ||
| + | -->\forall X\exists Y\forall y\big[y\in Y\liff\exists x[x\in X\wedge\varphi(x,y,p)]\big]\Big) }}</ref> | ||
** By ''[[rewriting for-all and exists within set theory]]'' we can make a small change to the {{M|\exists x}} part: | ** By ''[[rewriting for-all and exists within set theory]]'' we can make a small change to the {{M|\exists x}} part: | ||
*** {{M|\Big(<!-- | *** {{M|\Big(<!-- | ||
Latest revision as of 15:28, 5 April 2017
Provisional page grade: A*
This page is provisional
This page is provisional and the information it contains may change before this notice is removed (in a backwards incompatible way). This usually means the content is from one source and that source isn't the most formal, or there are many other forms floating around. It is on a to-do list for being expanded.The message provided is:
Needs:
- Infobox
- Apart of what set theories?
- Anything it requires as a precursor?
- Corollaries / use
[ilmath]\newcommand{\limplies}[0]{\rightarrow} \newcommand{\liff}[0]{\leftrightarrow} [/ilmath]
Contents
Definition
Let [ilmath]\varphi(a,b,p)[/ilmath] be a formula where [ilmath]a[/ilmath] and [ilmath]b[/ilmath] are free variables but [ilmath]p[/ilmath] is a parameter (or a parameter pack) and describes a function between classes.
The axiom schema of replacement posits that if [ilmath]F[/ilmath] is some class function then for all sets [ilmath]X[/ilmath], [ilmath]F(X)[/ilmath] - the image of [ilmath]X[/ilmath] under [ilmath]F[/ilmath] - denoted [ilmath]F(X)[/ilmath] is also a set[1].
We state it formally as follows:
- [ilmath]\Big(\underbrace{\forall x\forall y\forall z\big[\big(\varphi(x,y,p)\wedge\varphi(x,z,p)\big)\limplies y\eq z\big]}_{\text{if }(a,b)\in f\iff\varphi(a,b,p)\text{ then }f\text{ acts like a function relation} }\Big)[/ilmath] [ilmath]\limplies[/ilmath] [ilmath]\Big(\underbrace{\forall X\exists Y\forall y\big[y\in Y\liff\exists x[x\in X\wedge\varphi(x,y,p)]\big]}_{y\in Y\iff\text{the 'image' of }x\text{ under the 'function' is }y }\Big)[/ilmath][Note 1]
- By rewriting for-all and exists within set theory we can make a small change to the [ilmath]\exists x[/ilmath] part:
- [ilmath]\Big(\forall x\forall y\forall z\big[\big(\varphi(x,y,p)\wedge\varphi(x,z,p)\big)\limplies y\eq z\big]\Big)[/ilmath] [ilmath]\limplies[/ilmath] [ilmath]\Big(\forall X\exists Y\forall y\big[y\in Y\liff\exists x\in X[\varphi(x,y,p)]\big]\Big)[/ilmath]
- By rewriting for-all and exists within set theory we can make a small change to the [ilmath]\exists x[/ilmath] part:
Notes
- ↑ Here it is without the underbraces:
- [ilmath]\Big(\forall x\forall y\forall z\big[\big(\varphi(x,y,p)\wedge\varphi(x,z,p)\big)\limplies y\eq z\big]\Big)[/ilmath] [ilmath]\limplies[/ilmath] [ilmath]\Big(\forall X\exists Y\forall y\big[y\in Y\liff\exists x[x\in X\wedge\varphi(x,y,p)]\big]\Big) [/ilmath]
