This is part 3 of my posts about
the irrefutability of AC in ZF.
We define a hierarchy of sets, the
![V](/latex?n=de5a6f78116eca62d7fc5ce159d23ae6b889b365a1739ad2cf36f925a140d0cc)
-
hierarchy.
Furthermore, we have
![V_\alpha\subseteq V_\beta](/latex?n=718a2e02998c28d669666ff21e89152e61611bcc4f624a252278d11dda836412)
for
![\alpha\le\beta](/latex?n=451a1aaf8a1c23708e0c01a24746f5892f4501cefb724fb32bba23826fd9779e)
, which can be shown by a trivial
inductive argument.
Theorem: We have
![V=\bigcup_{\gamma\in On} V_\gamma](/latex?n=b9d6619779fde03092b10d1c8fc4f306760686eae50a25e57a49b5b869a44f91)
.
Proof: Assume there was an
![x\in V](/latex?n=8d5506dfec9b2e6af6eec1e35209e307aeacf41dc24f5df172352c2bd4192df2)
which is not in
![V_\alpha](/latex?n=92becdaca2dd0d191f64bdc3cdcd3a03a128e0e06e793cdc7bfec89f391a87e2)
for some
![\alpha](/latex?n=4893e9df8b5496ebe7a0f1c2cc92a39fb6df03085030e3b97cfcc4d45136db5a)
. Then it cannot be subset of any
![V_\alpha](/latex?n=92becdaca2dd0d191f64bdc3cdcd3a03a128e0e06e793cdc7bfec89f391a87e2)
, since otherwise it would be element of
![V_{\alpha+1}](/latex?n=f85a56f4770bbc2d99bde7c17a95e071c32daccc9fbedbed5f821b234087177a)
. Therefore it must contain an element
![x'](/latex?n=e81b61047eca0739f7270bda88a4eef57926f6e5c6611cce36b88354ff495c6d)
which is not in
![V_\alpha](/latex?n=92becdaca2dd0d191f64bdc3cdcd3a03a128e0e06e793cdc7bfec89f391a87e2)
for every
![\alpha](/latex?n=4893e9df8b5496ebe7a0f1c2cc92a39fb6df03085030e3b97cfcc4d45136db5a)
as well. That is, every set not being in any of the
![V_\alpha](/latex?n=92becdaca2dd0d191f64bdc3cdcd3a03a128e0e06e793cdc7bfec89f391a87e2)
must contain a set not being in any of the
![V_\alpha](/latex?n=92becdaca2dd0d191f64bdc3cdcd3a03a128e0e06e793cdc7bfec89f391a87e2)
, hence, we would get an infinite
![\ni](/latex?n=1f2066890ddef798f0cfbca2810ee6b9ad1ca2894ec83785cc5b1923a348fc8b)
-chain, which contradicts (FUN). □
Definition: The
relativization ![\phi^W](/latex?n=e97ecb453ec704e9ec360e934ddc45cc18e1ffb102b4cbff253cf7727440320c)
of a formula
![\phi](/latex?n=10ce0200b450ea955833553e717821c7721818b8a95cffd7e54b46e08918b512)
regarding a class
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
is defined inductively over the structure on
![\phi](/latex?n=10ce0200b450ea955833553e717821c7721818b8a95cffd7e54b46e08918b512)
by:
Intuitively,
![\phi^W](/latex?n=e97ecb453ec704e9ec360e934ddc45cc18e1ffb102b4cbff253cf7727440320c)
means that
![\phi](/latex?n=10ce0200b450ea955833553e717821c7721818b8a95cffd7e54b46e08918b512)
holds in
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
. We will later write
![W\models\phi](/latex?n=d5de735bcb25bfb2ebe633dcede79305725d86f8793d71e13d7d1f1c6c1f1694)
to denote that
![\phi^W](/latex?n=e97ecb453ec704e9ec360e934ddc45cc18e1ffb102b4cbff253cf7727440320c)
holds, defining yet another additional meaning for
![\models](/latex?n=7997c4f3be17c7ce998bd9f46b9abbeb9a8c4a26e57cd6f8839c029d91c2b550)
.
Definition: A class
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
is called
inner model of ZF, if it satisfies
- for all
we have ![x\subseteq W](/latex?n=e62e5c9e9d9b6fcca9dacd89db7d6909778ef93943b482d2bdd340544590419f)
![On\subseteq W](/latex?n=184bdf53259a2ce979b820a36424055d4ff425fe610d4db7971c3824e939830b)
- for all axioms
of ZF we have ![ZF\models\phi^W](/latex?n=5bf250c3a5dd90de6b46bc4c295512fd5363067089f0ad097a378b174b651545)
Remark: ![V](/latex?n=de5a6f78116eca62d7fc5ce159d23ae6b889b365a1739ad2cf36f925a140d0cc)
is an inner model of ZF, since
![\phi=\phi^V](/latex?n=d2c4856160864a3d1c1f14c094c7b3b73d41ef573369db2d6d0fef065cc14310)
.
Inner models provide a way of getting new models from models of ZF:
Remark: Let
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
be an inner model of ZF, and
![{\mathcal M}](/latex?n=b3eea6f6319248758b2c5fb92e642a01f5348db95bc4dd13049d5bf8184d7a80)
be a model of ZF with domain
![M](/latex?n=08f271887ce94707da822d5263bae19d5519cb3614e0daedc4c7ce5dab7473f1)
and the
![\in](/latex?n=729f2cd8398e996012ccabf10defcacca4f5c7343e72484f631eba1d210bc9ad)
-relation interpreted by a relation
![\epsilon\subseteq M^2](/latex?n=ad449cc11baccb31ba2d74e1ff121713df79d00e76dc9d1b86a0b7cfbbfb6119)
. Let
![N=\{a\in M|{\mathcal M}\models a\in W\}](/latex?n=ea308ebb23251116c87c2f4ad5273e4c958c107c8168c683d5aee4760dfd83c4)
and
![\mathcal N](/latex?n=6e9e0a3f9b6130ca0fa1e9096adc4469c23282c477e9149be4e72825a22ba1fa)
be an interpretation with domain
![N](/latex?n=8ce86a6ae65d3692e7305e2c58ac62eebd97d3d943e093f577da25c36988246b)
and
![\in](/latex?n=729f2cd8398e996012ccabf10defcacca4f5c7343e72484f631eba1d210bc9ad)
-relation
![\epsilon\cap N^2](/latex?n=f5e9bd8739637768e84ffc4bda8e17b5cf616d393ed282eb0def33c6beb86071)
. Then
![{\mathcal N}\models ZF](/latex?n=1bf3edf69d5e83d835a9577a5af3c8b77a82e489d99fea514d5aeefa18c2e150)
.
Therefore, it is sufficient to give an inner model of ZF satisfying AC to show that AC is not refutable: From a model of ZF, we would get a model of ZF satisfying AC. That is what we are going to do. Before we can do this, we have to do some work to give an alternative classification of inner models.
Definition: A formula is called
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-
formula, if every quantifier is
bounded, that is, every universal quantifier is of the form
![\forall_x (x\in y\rightarrow \phi)](/latex?n=5e6c87aa442d1ef6608f1c172dc58434baaf94dac252813da1db7cce6f438965)
, and equivalently, every existential quantifier is of the form
![\exists_x (x\in y \wedge \phi)](/latex?n=16edf9797f585bfbd141252696e0e4a8d49ca4579589aa002f90d5665011e3e2)
. (Recall that our language does not contain existential quantifiers directly, but defines them by universal quantifiers. However, our definition is equivalent to what we would get directly.)
Notice that
![x=y](/latex?n=14bf50d80768f3bcd08b39d302f7e14465ae44bf65e7ef88bb28e83e8a1ae172)
is a
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-formula.
We write
![\forall_{x\in y} \phi](/latex?n=9b2724974bcf2f4894b1b2b1f3cef9faea35296b2b5c5a997d892ab2b8ddc03a)
for
![\forall_x (x\in y\rightarrow \phi)](/latex?n=5e6c87aa442d1ef6608f1c172dc58434baaf94dac252813da1db7cce6f438965)
, and
![\exists_{x\in y} \phi](/latex?n=2ff7dc07ecaec0dbaffcc52851a5a2dd6dd6a5e2417524cc4df2789d036b6767)
for
![\exists_x (x\in y\wedge\phi)](/latex?n=0888adb08d957ee549746ae6acafc800b09b2bef00245a4ea752712b19b1ca73)
. Furthermore, if we want to denote a list of variables, then we use the vector notation
![\vec{x}](/latex?n=6e2c286eac5b03a21414c9618de9038cdda83c58945042b0e34e230a3dc787b9)
, and we will use
![\forall_{\vec{x}}](/latex?n=895a057716e11bee7c9a9e609106cf01ad5ae68e574174ffbb2fb9e2528757ae)
to denote the universal quantification over all of these variables.
Theorem I: Let
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
be a class. Then the following propositions are equivalent:
- a.
is an inner model - b.
satisfies: - (I1) Every element of
is a subset of ![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
- (I2) For every
there is an element
such that ![x\subseteq y](/latex?n=6e0004c78368850f8409fc9a4aad1214c6e90f698d8d35354b61657b86ddf2b7)
- (I3) For every
-formula
we have ![\forall_{\vec{z}\in W}\forall_{u\in W} \{x\in u|\phi(x,\vec{z})\}\in W](/latex?n=2f37fb6366db7a33154285d81fefc4ab50f4c2e326f0ba1b6996e1ca237ae70a)
To proof Theorem I, some additional work needs to be done. Firstly, we will replace the replacement scheme by two other schemes:
-comprehension: For every
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-formula
![\phi(x,\vec{z})](/latex?n=93b7a2c78c3f7f2efa034748e757bdb7e84ee1ceca1b61b94b508467c75f2fdc)
we have
![\forall_{\vec{z}}\forall_u\{x\in u|\phi(x,\vec{z})\}\in V](/latex?n=910573021d86939dd28eef0a4eb1573a7263e468f41499b94ee677015683726b)
.
Limitation: For every ZF-formula
![\phi(x,y,\vec{z})](/latex?n=1f76d554ddf46cd444a40d7da6fb7b070a987e4c3908d5413cb9aacaf6cf6ec7)
we have
![\forall_{\vec{z}}\forall_u\exists_v\forall_{x\in u} ((\exists_y \phi(x,y,\vec{z}))\rightarrow \exists_{y\in v}\phi(x,y,\vec{z}))](/latex?n=aca7bb45e32506366378f193ad4d44edc5b0c7e0f766935d3b4381d2a4b76845)
Theorem: These schemes are derivable from ZF.
Proof: ![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-comprehension follows by general comprehension, which follows by (RPL). For limitation, let
![\phi](/latex?n=10ce0200b450ea955833553e717821c7721818b8a95cffd7e54b46e08918b512)
,
![\vec{z}](/latex?n=2a7db5a6ad77cd08c23d63f4372b815108c268da8e443af4fc268b8fa6f439ed)
and
![u](/latex?n=0bfe935e70c321c7ca3afc75ce0d0ca2f98b5422e008bb31c00c6d7f1f1c0ad6)
be given, and
![a=\{x\in u|\exists_y\phi(x,y,\vec{z})\}](/latex?n=fd7f5c922ad3c9bec4751b110cc234734f1cc41d5659f8823b48bbf27052483d)
. Define a function
![g:a\rightarrow On, g(x)=\min\{\gamma|\exists_{y\in V_\gamma}\phi(x,y,\vec{z})\}](/latex?n=b2af01df7cd8efd18d296e72bcb6a6cc6ebabc1fd58c74971d9e6a7c06023a89)
; this is well-defined, since such a
![\gamma](/latex?n=67610b0632683369b69db194167ac4c38ed7c7cfab252970ced9e152b9b45554)
always exists according to the above theorem. Then the range of
![g](/latex?n=cd0aa9856147b6c5b4ff2b7dfee5da20aa38253099ef1b4a64aced233c9afe29)
is a set of ordinals, and therefore has a supremum
![\alpha](/latex?n=4893e9df8b5496ebe7a0f1c2cc92a39fb6df03085030e3b97cfcc4d45136db5a)
. Now set
![v=V_\alpha](/latex?n=1e2298ae84f4a472448150fb4d3827dc6d9bfef862a2266eb54eee0ea5fcfa94)
. Then
![v](/latex?n=4c94485e0c21ae6c41ce1dfe7b6bfaceea5ab68e40a2476f50208e526f506080)
contains an
![y](/latex?n=a1fce4363854ff888cff4b8e7875d600c2682390412a8cf79b37d0b11148b0fa)
for every
![x](/latex?n=2d711642b726b04401627ca9fbac32f5c8530fb1903cc4db02258717921a4881)
, such that
![\phi(x,y,\vec{z})](/latex?n=1f76d554ddf46cd444a40d7da6fb7b070a987e4c3908d5413cb9aacaf6cf6ec7)
.
□
We now show the converse, these schemes imply replacement.
Lemma: For every ZF-formula
![\phi(\vec{x})](/latex?n=47553b2cb4988df3206c782e16c01684d6ff99f1bed525497fa0c796a007e974)
,
![\forall_{u_1}\ldots\forall_{u_n}\{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}\in V](/latex?n=355ad56a6e9937b85f640c8c91ab8aa0ca4c94c9bec956bf60277dde7b250f50)
can be shown by
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-comprehension and limitation, not using full comprehension.
Proof: Recall that for pairs
![\left<x,y\right>:=\{\{x,y\},\{x\}\}\}](/latex?n=2a433a8ccfeca74e317d01aa115a7a0be18aae298c3b8d345204d78b5d22d2f4)
. We show that from
![u,v\in V](/latex?n=75bd97d3081217c617a76d767ac06f72c6c08d134851fbda768ef86cdf0451c0)
follows
![u\cap v,u\backslash v,u\times v\in V](/latex?n=0026fc98a3850555b1a3ad12a726e4126d29f7b22ad6cb2f7c9ce48eb68ecc1a)
:
![u\cap v=\{x\in u\cup v| x\in u\wedge x\in v\}](/latex?n=a9a819df86ca8488fd4acd6f1fba8767009ea486988f8421c8630ded12c248e3)
,
![u\backslash v = \{x\in u|x\not\in v\}](/latex?n=2a0d92df9800cfd98b9f78080fddb9d3d270312eafd8640ec0312ed325710561)
are sets by
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-comprehension. By limitation, there exists a set
![b](/latex?n=3e23e8160039594a33894f6564e1b1348bbd7a0088d42c4acb73eeaed59c009d)
such that for all
![x\in u](/latex?n=c964ee98ac6b9959c4ea82a71250772ac759aba7767801e030e689f9f9d94eb0)
we have an
![y\in b](/latex?n=ccb94b34a11d8893deed22cf643efad11b072e8e6ef3768ed9993fb745466782)
with
![\forall_{z\in v} \left<x,z\right>\in y](/latex?n=712fd5a14aab73199294ae9cf4e2831ae27c803656be6e5ae83c6f813db388f8)
. That is,
![b](/latex?n=3e23e8160039594a33894f6564e1b1348bbd7a0088d42c4acb73eeaed59c009d)
contains a superset of
![\{x\}\times v](/latex?n=94faae19e49ea828ba090db586348db5a6df7709de5958d37c68355b5a0052dc)
for every
![x\in u](/latex?n=c964ee98ac6b9959c4ea82a71250772ac759aba7767801e030e689f9f9d94eb0)
, that is
![\bigcup_{r\in b}\{r\}](/latex?n=1f1077666d49a2b7d3469cb544bfa8e9951772ed872c49a41f27f4bb53651587)
is a superset of
![u\times v](/latex?n=2534f70220cb07706f48cec3708c1fdb0161d28b56c7997cc4811f1850a7dbe8)
, thus,
![u\times v=\{a \in \bigcup_{r\in b}\{r\}| \exists_{x\in u}\exists_{y\in v} a=\{\{x,y\},\{x\}\}\}](/latex?n=9f74e9c5db3a06d010abf7c0e25e5e752f6dd37726fd47ec9503837d5f7bc1cb)
is a set due to
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-comprehension.
We now use structural induction on
![\phi(\vec{x})](/latex?n=47553b2cb4988df3206c782e16c01684d6ff99f1bed525497fa0c796a007e974)
.
If
![\phi(\vec{x})=\bot](/latex?n=f0956b383770e8b7d5acaf9bccaa069afc14f055bcbdaf929ddb201c9ae8c150)
, then
![\emptyset](/latex?n=8d2cacefc75ba038f020cd92e4b0cf1458ad543ef8d3393b99fc1787330c38b5)
is the desired set.
If
![\phi(\vec{x})](/latex?n=47553b2cb4988df3206c782e16c01684d6ff99f1bed525497fa0c796a007e974)
is of the form
![x_i\in x_j](/latex?n=bcc70cf8f9a0559904fa9359809c0a72f86d405a7ab1a3b8918563a473c0ac85)
, let
![u_1,\ldots,u_n](/latex?n=03ce14c581dbe7453ce13a2c685fece4672b827e631ab9f33205daf2d88ae3c7)
be given and let
![W=\{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}=](/latex?n=8a9a80aae84fda82b7950238cdcfd322bdff05595bf1a904913b394fa7fdea6b)
![\{z\in u_1\times\ldots\times u_n|\exists_{x_1\in u_1}\ldots\exists_{x_n\in u_n} (z=\left<x_1,\ldots,x_n\right>\wedge x_i\in x_j)\}](/latex?n=060b7b3046fabf2b90346656e8e6a0fac946523fa58279c3cf7304c9497bf0ff)
, and
![\exists_{x_1\in u_1}\ldots\exists_{x_n\in u_n} (z=\left<x_1,\ldots,x_n\right>\wedge x_i\in x_j)](/latex?n=03fe68e442ef844190ec8c08be3884ad608a245bfd372708b9c9a408b2a38e1f)
is a
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-formula, which means that
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
is a set by
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-comprehension.
If
![\phi(\vec{x})](/latex?n=47553b2cb4988df3206c782e16c01684d6ff99f1bed525497fa0c796a007e974)
is of the form
![\phi_1(\vec{x})\wedge\phi_2(\vec{x})](/latex?n=ec2cef65b0f24e6c59aecdf62250de93c520b896edb408f9275a83e4eafaa17c)
, then
![\{\left<x_1,\ldots,x_n\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}=](/latex?n=6251bea4cea19fd8aca5ffedbacc9c99a654c1d2c605977ef13944ab4c204a1d)
![\{\left<x_1,\ldots,x_n\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}\cap](/latex?n=d61277817fd98b5b9b04ba5c8c26ae0c8e9ee7e074bd8417bb1860fccb91a32d)
![\{\left<x_1,\ldots,x_n\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}](/latex?n=dc76a94fdd3d8b1f5f95f15c34a31a17b49963357e147810dade3da07b71cc95)
and these are both sets by induction.
For
![\phi(\vec{x})=\phi_1(\vec{x})\rightarrow\phi_2(\vec{x})](/latex?n=003823ade13bfff3e474557bcf7b4b4b4487a051924b976f484485c9c2ba71b3)
notice that
![\phi(\vec{x})\leftrightarrow \lnot (\phi_1(\vec{x})\wedge\lnot\phi_2(\vec{x}))](/latex?n=7c20b8a8e148312a4244a4b0e409bfe0433283fad7813c5ddef08a1ed079b37d)
, therefore it is sufficient to show the induction step for negations. Thus, let
![\phi(\vec{x})=\lnot\phi_3(\vec{x})](/latex?n=4d3d12f470169979ad8ce20ed344deb151c80d32550d8aeff7a196824975adf3)
. Then
![\{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}=u_1\times\ldots\times u_n \backslash \{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\phi_3(\vec{x})\}](/latex?n=f3bc442ef870f53e299f55c005266ccaea4d31c13d757ec521a95a31ce1c60ca)
which is a set by induction.
For
![\phi(\vec{x}) = \forall_y \phi_1(\vec{x},y)](/latex?n=c197fab471559eb83e029ebe1c2bf17c57e4e2f3b6072215d90b64ee4903598d)
, by limitation we have a set
![v\in V](/latex?n=5635dbab273b2a4cbdf6cc7d05103fe160a05899eddedf17dfda463545a8af23)
with
![\forall_{x_1\in u_1}\ldots\forall_{x_n\in u_n}((\exists_y \lnot\phi_1(\vec{x},y))\rightarrow\exists_{y\in v}\lnot\phi_1(\vec{x},y))](/latex?n=5dce6f507a374b457e917f00378aa8851f756a2a175e0ad191df849e223bbd38)
. By induction hypothesis,
![q=\{\left<\vec{x},y\right>\in u_1\times\ldots\times u_n\times v|\phi_1(\vec{x},y)\}\in V](/latex?n=1c59340bf3df54a20d2221c345b2c334257cebcb7342cbe05b97305d49d1085f)
, and therefore
![a=u_1\times\ldots\times u_n\times v-q=](/latex?n=074269b78e0e8063e5f17f11e2e9cf4dae0fa5ab20b7324661d53f16071e7b1e)
![\{\left<\vec{x},y\right>\in u_1\times\ldots\times u_n\times v|\lnot\phi_1(\vec{x},y)\}\in V](/latex?n=87f39659429ec2ab6666303affb0f3c56c4b11a4bf9de6ba4bf008de4501cb3d)
. Therefore, by
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-comprehension,
![b=\{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\exists_x\lnot\phi_1(\vec{x})\}=](/latex?n=1b5b10ee44757e4fcd479f3d7cb619c94030e342951f1cc15e0ecead4b7f9b5c)
![\{z\in u_1\times\ldots\times u_n|\exists_{y\in v}\left<z,y\right>\in a\}\in V](/latex?n=73888244df78d71808efbf2787afa82dc2635b2d6958852ab77b4cb3b554f3d1)
, therefore,
![\{\left<\vec{x}\right>\in u_1\times\ldots\times u_n|\phi(\vec{x})\}=u_1\times\ldots\times u_n-b\in V](/latex?n=3caab1e0c8ccadabde3887ea189ffdce19256d059ba25b147201928758e9dde6)
.
□
Lemma: For
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-formulae
![\phi(\vec{x})](/latex?n=47553b2cb4988df3206c782e16c01684d6ff99f1bed525497fa0c796a007e974)
and classes
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
such that
![x\in W\Rightarrow x\subseteq W](/latex?n=bb41b8c13ad72b1be574c20c1a92d75f6237b12042e85ee948b22b6b0535fdf1)
follows
![\forall_{\vec{x}\in W} (\phi(\vec{x})\leftrightarrow\phi^W(\vec{x}))](/latex?n=245dd8e68953019a8913f399a899278bd953ebe448970b469488f66af4c81ac9)
.
Proof: By structural induction. For everything except quantors, the relativization can be looped through. For quantors, we may assume that we always have an existential quantifier, since
![\forall_x\phi\leftrightarrow\lnot\exists_x\lnot\phi](/latex?n=1f2f509ea97637cd62cec3f94a6760794eaff54ddd509c7b89f82698b57404c8)
. So let
![\phi(\vec{x})=\exists_{z\in y}\psi(z,\vec{x},y)](/latex?n=095a8c83c68efcda41a425189a2896be15f212d44a89e880adb16b12dadc0b01)
. We may assume that
![x\neq y](/latex?n=855e79764b4d5815c2e29aac8d0e95b3ff4a0f14a9b962589d21135864940d8a)
, since otherwise the formula would be equivalent to
![\bot](/latex?n=ff66021ec1d8e804e4720480d98fded1494c488b20aa5fa3d830c073d1ddf62a)
. Let
![\vec{x},y\in W](/latex?n=9c466453893369219d14e4d85641c24af4fda7bdbdc6222bad8829142bad7a0c)
, then by induction hypothesis
![\psi^W(z,\vec{x},y)\rightarrow\psi(z,\vec{x},y)](/latex?n=66af15532bc16253112a21cc6badd68e3edca67e766c1e6791b5dc948aa6ccd6)
, and therefore
![\phi^W(\vec{x},y)\rightarrow\phi(\vec{x},y)](/latex?n=91de0e3768488ef2d478d2691c27fa8b7fa9ef9f5d90ff98353abd8c16e8ebe5)
. For the other direction, assume
![\phi(\vec{x},y)](/latex?n=551c554440cdd77e59aac9e167b698d1f86d374aa630513958db76e9e513e116)
, that is, there is some
![z\in y](/latex?n=08b62aa4bd1e7383b23232e668ba655b5e41230d6a77db54a2060f435c8deed9)
such that
![\psi(z,\vec{x},y)](/latex?n=1c49eb9ae7751bfa1c54f7f54a385a347017f2de0185823287ebdabd7a9579c1)
. Then
![y\in W](/latex?n=6ddac084009398bea3c9336834313e6d7c644e0f66d3d66515c6d83bb077c008)
implies
![y\subseteq W](/latex?n=b3640684e26591de4c5e7453b54d869409dd2dd9ebb99cbe280752e2009a3f2e)
which implies
![z\in W](/latex?n=e3d2de1f8bbb1e7dc4b217ea9a34a0b9587f6f1ba634e4d47e43e14869bc5425)
, so by induction hypothesis,
![\psi^W(z,\vec{x},y)](/latex?n=01b422ec3daf178d7a7c3ea130c04d037448468c6043ee1a7af40c5a3ab99dcd)
, and since
![z\in W](/latex?n=e3d2de1f8bbb1e7dc4b217ea9a34a0b9587f6f1ba634e4d47e43e14869bc5425)
we have
![\exists_{z\in y\cap W}\psi^W(z,\vec{x},y)](/latex?n=0390b4d39b7a5fbd062013be31b69f683bbaff1404886e10a4fb0dc4a99e1e69)
, therefore
![\phi^W(\vec{x})](/latex?n=96446f70d10b7a16b0b4caf8f180a6d5a313980b6b126392af9d4adfb1fbf164)
.
□
Corollary: For
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-formulae
![\psi(\vec{x},\vec{y})](/latex?n=8a89dc0dad6294dfbc6378edb4deb4c4ebcea1a560a9306f748fe0859dcfbcbb)
and classes
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
in which every element is a subset we have
![\forall_{\vec{y}\in W}((\forall_{\vec{x}}\psi(\vec{x},\vec{y}))\rightarrow\forall_{\vec{x}\in W}\psi^W(\vec{x},\vec{y})](/latex?n=654c04ae4acd93d5a6022ee40c3e2504a2c62cf8155f1766a88e548c7079ebef)
and
Theorem: From
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-comprehension and limitation follows replacement.
Proof: Let
![F](/latex?n=f67ab10ad4e4c53121b6a5fe4da9c10ddee905b978d3788d2723d7bfacbe28a9)
be a functor, and
![u\in v](/latex?n=bee40695bd0fa3f8a91bbffc4b6d0f82449b6f6cd0e4a9f3528e80970fdd506d)
. By limitation we get a
![v\in V](/latex?n=5635dbab273b2a4cbdf6cc7d05103fe160a05899eddedf17dfda463545a8af23)
with
![\forall_{x\in u} ((\exists_y F(x)=y)\rightarrow \exists_{y\in v} F(x)=y)](/latex?n=94fba1c189a37d76b77e36ccd056ee71774317c76cfa2d3952bf703c7b031f7a)
. Then
![\{F(x)|x\in u\}=\{y\in v|\exists_{x\in u} F(x)=y\}\in V](/latex?n=72739c40666a2d3e8aeca95e0fe23808313ade03998c14cd90c3adb5dce6a4c1)
by the above Lemma.
□
We finally arrive at...
Proof of Theorem I: "a=>b": (I1) by definition. For (I2), consider the
![V_\alpha](/latex?n=92becdaca2dd0d191f64bdc3cdcd3a03a128e0e06e793cdc7bfec89f391a87e2)
-hierarchy inside
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
, that is, define
![W_\alpha := V_\alpha^W](/latex?n=13756794161c58a7c4a791421e4f9502c9f4d597eb3639c5a5776822cf290039)
. For
![x\in V,x\subseteq W](/latex?n=a398f407529340ca54bbad96ab0419a74a0fc36e1091f6457364656bc3f41a13)
we can find an
![\alpha](/latex?n=4893e9df8b5496ebe7a0f1c2cc92a39fb6df03085030e3b97cfcc4d45136db5a)
such t hat
![x\subseteq W_\alpha](/latex?n=3886e5498b2c9a39b402eea2206134dd618c081ec81288389aa28d322c987108)
, and
![W_\alpha\in W](/latex?n=555a9a1985c6fc7a6f453ac55afd69a868b8d3de27b511e633802f6e6ac10f4c)
. For (I3), let
![\phi(x,\vec{z})](/latex?n=93b7a2c78c3f7f2efa034748e757bdb7e84ee1ceca1b61b94b508467c75f2fdc)
be a
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-formula and let
![\vec{z}\in W](/latex?n=e7854634f397f9cc29d32e7a67c029f486d20bb13f19fdb8ce02462db1d0bba0)
. Because of (I1) we have
![\phi(x,\vec{z})\leftrightarrow\phi^W(x,\vec{z})](/latex?n=86bd3303ad2210a05301e552e4b6d8563b2214e74ea80c9570ebabb98d5df931)
for all
![x\in W](/latex?n=63eed7d965c4ed178c7ceb50206564bacb150dc22db2b981c70fcb9b63e02fba)
according to the above lemma. Therefore, for every
![u\in W](/latex?n=bdb0cd2e9b097a19a40563ac388d675eecb1a9e6d9509defd17d6f2f553665bb)
,
![\{x\in u|\phi(x,\vec{z})\}=\{x\in u\cap W|\phi^W(x,\vec{z})\}](/latex?n=2498aded088c768f19d457b1610ac705b5c56a86903678f96124d07ab2f50248)
, which is in
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
by comprehension.
"b=>a": Trivially,
![On\cap W](/latex?n=572148392114ffcbc9492bc06cb81782bb4b9600387b0d7b258ea6b6985a56ca)
is transitive, and as every transitive set of ordinals is an ordinal, either
![On\cap W\in On](/latex?n=cf97041b06f5de20ebf506fe5025fc5ce167221e8b4a0073433d4593f2741bc9)
or
![On\cap W = On](/latex?n=bedda453b254c9ab8778dcc13f552d47d38a224f92acabaa11632b4c02ae85e3)
. Assume
![On\cap W\in On](/latex?n=cf97041b06f5de20ebf506fe5025fc5ce167221e8b4a0073433d4593f2741bc9)
, then by (I2) we have an
![y\in W](/latex?n=6ddac084009398bea3c9336834313e6d7c644e0f66d3d66515c6d83bb077c008)
such that
![On\cap W\subseteq y](/latex?n=1c3ba19c8841887f5310670d5c8c5c04c3afe3c6894a2bd6789af9eff72fc4da)
. But
![On\cap W = \{x\in y|x\in On\}](/latex?n=3b19595b242352a0a56885567c52628f0fa124f11e4a47de39679806fe066c1d)
which is in
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
by (I3), so
![On\cap W\in On\cap W](/latex?n=cd415a362ad6d5df82e21e52793728962daf8513dd9274fffd0710dec24868e8)
. Contradiction. Therefore,
![On\subseteq W](/latex?n=184bdf53259a2ce979b820a36424055d4ff425fe610d4db7971c3824e939830b)
. We show the ZF-axioms. (EXT) and (FUN) hold because of the above Corollary, (NUL) and (INF) hold since
![\omega,\emptyset\in On\subseteq W](/latex?n=c1df5df9a54b8f52cd7d3a38f0abf0b9b46c2e27c0d29cd925b753faa471ec5c)
. For (UNI), let
![x\in W](/latex?n=63eed7d965c4ed178c7ceb50206564bacb150dc22db2b981c70fcb9b63e02fba)
, then
![x\subseteq W](/latex?n=e62e5c9e9d9b6fcca9dacd89db7d6909778ef93943b482d2bdd340544590419f)
and therefore every
![y\in x](/latex?n=e51268f91ec40cd948035eccdab1d6faa7b34cdb9e9a37f95b498c63022e739b)
is subset of
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
, therefore
![\bigcup_{y\in x}y\in W](/latex?n=0f2b746fd7c93ad8e1926e54ce9750983c8feda2fbedfb297393b1f31b124389)
and according to (I2) we find a superset
![u\in W](/latex?n=bdb0cd2e9b097a19a40563ac388d675eecb1a9e6d9509defd17d6f2f553665bb)
. But then,
![\bigcup_{y\in x}y = \{y\in u|\exists_{z\in x} y\in z\}\in W](/latex?n=0efec0a5aa8467d6f40d0082f4a94c77235589672fe723f84c44379faa265e13)
by (I3). Similar for (PAR). For (POW), let
![x\in W](/latex?n=63eed7d965c4ed178c7ceb50206564bacb150dc22db2b981c70fcb9b63e02fba)
. Then by (I2), since
![\mathbb{P}(x)\cap W\subseteq W](/latex?n=b39e97af98e573de9e2f0d94f6c8cc539d61563af4beb0099ba8e4f112b11191)
, there exists an
![u\in W](/latex?n=bdb0cd2e9b097a19a40563ac388d675eecb1a9e6d9509defd17d6f2f553665bb)
such that
![\mathbb{P}(x)\cap W\subseteq u](/latex?n=4afccaa9e64331d90c4ffee7880bd87072e9b4c8e20ed1e0f0333f02050a2ffc)
. Then by (I3),
![\mathbb{P}(x)\cap W=\{z\in u|z\subseteq x\}\in W](/latex?n=3c2e1a5b6202fb3e55b0e803062667861b702297a82e715083cbfaaaab160311)
.
We have proven that replacement can be replaced by
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-comprehension and limitation, therefore, we show
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-comprehension and limitation in
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
. For
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-comprehension, let
![\phi(x,\vec{z})](/latex?n=93b7a2c78c3f7f2efa034748e757bdb7e84ee1ceca1b61b94b508467c75f2fdc)
be a
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-formula. We have to show that
![\forall_{\vec{z}\in W}\forall_{u\in W}\{x\in u|\phi^W(x,\vec{z})\}\in W](/latex?n=9c523d3c18234c0674e269033d109a25fc057d22785ae3a3c6a9cc3d958970c5)
. But by the above Lemma, this is the same set as
![\{x\in u|\phi^W(x,\vec{z})\}](/latex?n=e39470b747cc23ab22a5949dca010905d4d342a8551ad5dbf53a59659a9e3237)
, which is in
![W](/latex?n=fcb5f40df9be6bae66c1d77a6c15968866a9e6cbd7314ca432b019d17392f6f4)
according to (I3). For limitation, consider again a
![\Sigma_0](/latex?n=59681cd776049191c419cda67a89f5bc98861b66f4c13b1f66ecd86a795c0134)
-formula
![\phi(x,y,\vec{z})](/latex?n=1f76d554ddf46cd444a40d7da6fb7b070a987e4c3908d5413cb9aacaf6cf6ec7)
. Then we have to show
![\forall_{\vec{z}\in W}\forall_{\vec{u}\in W}\exists_{v\in W}\forall_{x\in U}((\exists_{y\in W}\phi^W(x,y,\vec{z}))\rightarrow\exists_{y\in v}\phi^W(x,y,\vec{z}))](/latex?n=ebe20a3c6e0423ac794376ae4c50fc0c6e59b2cfa046dd091ae99080c5235e1c)
. Let
![\vec{z},u\in W](/latex?n=d33c24be3ab933ef62c439ebb5c3af628f7e45848cfb8001dcf4549fb0fab9cd)
, then there exists a
![v'\in V](/latex?n=6c51c9114236f27ab46ea42ef89ad86371802e32a6227441da18881d93e8f81a)
such that
![\forall_{x\in u}((\exists_{y\in W}\phi^W(x,y,\vec{z}))\rightarrow\exists_{y\in v'} (y\in W\wedge \phi^W(x,y,\vec{z})))](/latex?n=18a56dc9e0120b2fb25610f8ed88cceab461134c1a6078914fc35af3eee584f1)
. By (I2) we get a
![v\in W](/latex?n=21ce1635435bf8dcb30926cc927edac9fe405dd5b0a7035db188e046ea7b3e34)
such that
![v'\cap W\subseteq v](/latex?n=19c232fbcd3ff3f1d149a1fcf2aa011e2efdc681f3aa0fed0a767b7b79dc3e2c)
, which trivially satisfies the above formula.
□