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
\newcommand{\limplies}[0]{\rightarrow} \newcommand{\liff}[0]{\leftrightarrow}
Contents
[hide]Definition
Let \varphi(a,b,p) be a formula where a and b are free variables but p is a parameter (or a parameter pack) and describes a function between classes.
The axiom schema of replacement posits that if F is some class function then for all sets X, F(X) - the image of X under F - denoted F(X) is also a set[1].
We state it formally as follows:
- \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) \limplies \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)[Note 1]
- By rewriting for-all and exists within set theory we can make a small change to the \exists x part:
- \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) \limplies \Big(\forall X\exists Y\forall y\big[y\in Y\liff\exists x\in X[\varphi(x,y,p)]\big]\Big)
- By rewriting for-all and exists within set theory we can make a small change to the \exists x part:
Notes
- Jump up ↑ Here it is without the underbraces:
- \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) \limplies \Big(\forall X\exists Y\forall y\big[y\in Y\liff\exists x[x\in X\wedge\varphi(x,y,p)]\big]\Big)
