Схемой преобразования [множеств] (Axiom schema of replacement) называется следующее высказывание теории множеств :
∀
x
∃
{
1
}
y
(
ϕ
[
x
,
y
]
)
→
∀
a
∃
d
∀
c
(
c
∈
d
↔
∃
b
(
b
∈
a
∧
ϕ
[
b
,
c
]
)
)
{\displaystyle \forall x\exists ^{\{1\}}y\ (\phi [x,y])\to \forall a\exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in a\ \land \ \phi [b,c])\ )}
∀
x
∃
{
1
}
y
(
ϕ
[
x
,
y
]
)
⇔
∀
x
∃
!
y
(
ϕ
[
x
,
y
]
)
⇔
∀
x
∃
y
∀
y
′
(
ϕ
[
x
,
y
]
↔
y
=
y
′
)
{\displaystyle \forall x\exists ^{\{1\}}y\ (\phi [x,y])\Leftrightarrow \forall x\exists !y\ (\phi [x,y])\Leftrightarrow \forall x\exists y\forall y'(\phi [x,y]\leftrightarrow y=y')}
Схему преобразования можно сформулировать по-русски, а именно: "Любое множество можно преобразовать в [то же самое или другое] множество
d
{\displaystyle d}
ϕ
{\displaystyle \phi }
b
{\displaystyle b}
a
{\displaystyle a}
Пример В следующем примере функциональное суждение
y
=
x
{\displaystyle y=x}
a
{\displaystyle a}
ϕ
[
x
,
y
]
↔
y
=
x
⇒
∀
a
∃
d
∀
c
(
c
∈
d
↔
∃
b
(
b
∈
a
∧
c
=
b
)
)
⇔
∀
a
∃
d
∀
c
(
c
∈
d
↔
c
∈
a
)
{\displaystyle \phi [x,y]\leftrightarrow y=x\quad \Rightarrow \quad \forall a\exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in a\ \land \ c=b))\quad \Leftrightarrow \quad \forall a\exists d\forall c\ (c\in d\leftrightarrow c\in a)}
Другие формулировки схемы преобразования
править
Схему преобразования записывают также в следующем виде:
∀
a
(
∀
b
(
b
∈
a
→
∃
{
1
}
y
(
ϕ
[
b
,
y
]
)
)
→
∃
d
∀
c
(
c
∈
d
↔
∃
b
(
b
∈
a
∧
ϕ
[
b
,
c
]
)
)
)
{\displaystyle \forall a\ (\ \forall b\ (b\in a\to \exists ^{\{1\}}y\ (\phi [b,y])\ )\quad \to \quad \exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in a\ \land \ \phi [b,c])\ ))}
Примеры 1. В следующем примере функциональное суждение
y
=
2
b
′
{\displaystyle y=2b'}
N
{\displaystyle \mathbb {N} }
{
0
,
2
,
4
,
.
.
.
}
{\displaystyle \{0,2,4,...\}}
a
=
N
∧
(
ϕ
[
b
′
,
y
]
↔
y
=
2
b
′
)
⇒
∃
d
∀
c
(
c
∈
d
↔
∃
b
(
b
∈
N
∧
c
=
2
b
)
)
⇔
∃
d
∀
c
(
c
∈
d
↔
c
∈
{
0
,
2
,
4
,
.
.
.
}
)
{\displaystyle {\begin{aligned}a=\mathbb {N} \ \land \ (\phi [b',y]\leftrightarrow y=2b')\quad \Rightarrow \quad \exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in \mathbb {N} \ \land \ c=2b))\\\ \Leftrightarrow \exists d\forall c\ (c\in d\leftrightarrow c\in \{0,2,4,...\})\end{aligned}}}
2. В следующем примере функциональное суждение
(
b
′
=
0
→
y
=
a
1
)
∧
(
b
′
≠
0
→
y
=
a
2
)
{\displaystyle (b'=0\to y=a_{1})\ \land \ (b'\neq 0\to y=a_{2})}
R
{\displaystyle \mathbb {R} }
{
a
1
,
a
2
}
{\displaystyle \{a_{1},\ a_{2}\}}
a
=
R
∧
(
ϕ
[
b
′
,
y
]
↔
(
b
′
=
0
→
y
=
a
1
)
∧
(
b
′
≠
0
→
y
=
a
2
)
)
⇒
∃
d
∀
c
(
c
∈
d
↔
∃
b
(
b
∈
R
∧
(
b
=
0
→
c
=
a
1
)
∧
(
b
≠
0
→
c
=
a
2
)
)
)
⇔
∃
d
∀
c
(
c
∈
d
↔
c
=
a
1
∨
c
=
a
2
)
{\displaystyle {\begin{aligned}a=\mathbb {R} \quad \land \quad (\phi [b',y]\leftrightarrow (b'=0\to y=a_{1})\ \land \ (b'\neq 0\to y=a_{2}))\quad \Rightarrow \\\ \exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in \mathbb {R} \ \land \ (b=0\to c=a_{1})\land (b\neq 0\to c=a_{2})\ ))\\\ \Leftrightarrow \exists d\forall c\ (c\in d\leftrightarrow c=a_{1}\ \lor \ c=a_{2})\end{aligned}}}
3. В следующем примере функциональное суждение
(
0
≤
b
′
≤
1
→
y
=
b
′
)
∧
(
¬
(
0
≤
b
′
≤
1
)
→
y
=
1
)
{\displaystyle (0\leq b'\leq 1\to y=b')\ \land \ (\neg (0\leq b'\leq 1)\to y=1)}
Z
{\displaystyle \mathbb {Z} }
{
n
:
n
∈
N
∧
n
<
2
}
{\displaystyle \{n:\ n\in \mathbb {N} \ \land \ n<2\}}
a
=
Z
∧
(
ϕ
[
b
′
,
y
]
↔
(
0
≤
b
′
≤
1
→
y
=
b
′
)
∧
(
¬
(
0
≤
b
′
≤
1
)
→
y
=
1
)
)
⇒
∃
d
∀
c
(
c
∈
d
↔
∃
b
(
b
∈
Z
∧
(
0
≤
b
≤
1
→
c
=
b
)
∧
(
b
<
0
∨
b
>
1
→
c
=
1
)
)
)
⇔
∃
d
∀
c
(
c
∈
d
↔
c
∈
{
n
:
n
∈
N
∧
n
<
2
}
)
{\displaystyle {\begin{aligned}a=\mathbb {Z} \quad \land \quad (\phi [b',y]\leftrightarrow (0\leq b'\leq 1\to y=b')\land (\neg (0\leq b'\leq 1)\to y=1))\quad \Rightarrow \\\ \exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in \mathbb {Z} \land (0\leq b\leq 1\to c=b)\land (b<0\lor b>1\to c=1)))\\\ \Leftrightarrow \exists d\forall c\ (c\in d\leftrightarrow c\in \{n:\ n\in \mathbb {N} \ \land \ n<2\}\ )\end{aligned}}}
Схему преобразования записывают также в следующем виде:
∀
a
(
∀
b
(
b
∈
a
→
∃
{
0
,
1
}
y
(
ϕ
[
b
,
y
]
)
)
→
∃
d
∀
c
(
c
∈
d
↔
∃
b
(
b
∈
a
∧
ϕ
[
b
,
c
]
)
)
)
{\displaystyle \forall a\ (\ \forall b\ (b\in a\to \exists ^{\{0,1\}}y\ (\phi [b,y]))\quad \to \quad \exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in a\ \land \ \phi [b,c])\ ))}
∃
{
0
,
1
}
y
(
ϕ
[
b
,
y
]
)
⇔
∀
y
∀
y
′
(
ϕ
[
b
,
y
]
∧
ϕ
[
b
,
y
′
]
→
y
=
y
′
)
{\displaystyle \exists ^{\{0,1\}}y\ (\phi [b,y])\Leftrightarrow \forall y\forall y'\ (\phi [b,y]\ \land \ \phi [b,y']\to y=y')}
Фон Нейман доказал, что данная аксиома следует из аксиомы ограничения размера . Аксиома схемы преобразований может быть выражена как: если F является функцией, а A является множеством, то F (A ) - это множество.
1. Связь между схемой преобразования и аксиомой пары выражается следующим высказыванием:
∀
a
1
∀
a
2
(
a
=
P
(
P
(
∅
)
)
∧
(
ϕ
[
b
′
,
y
]
↔
(
b
′
=
∅
→
y
=
a
1
)
∧
(
b
′
≠
∅
→
y
=
a
2
)
)
→
(
∃
d
∀
c
(
c
∈
d
↔
∃
b
(
b
∈
a
∧
ϕ
[
b
,
c
]
)
)
→
∃
c
∀
b
(
b
∈
c
↔
b
=
a
1
∨
b
=
a
2
)
)
)
,
{\displaystyle {\begin{aligned}\forall a_{1}\forall a_{2}\ (a={\mathcal {P}}({\mathcal {P}}(\varnothing ))\quad \land \quad (\phi [b',y]\ \leftrightarrow \ (b'=\varnothing \to y=a_{1})\land (b'\neq \varnothing \to y=a_{2})\ )\\\ \rightarrow \quad (\exists d\forall c\ (c\in d\ \leftrightarrow \ \exists b\ (b\in a\land \phi [b,c]))\ \rightarrow \ \exists c\forall b\ (b\in c\leftrightarrow b=a_{1}\lor b=a_{2})\ )),\end{aligned}}}
где
P
(
P
(
∅
)
)
{\displaystyle {\mathcal {P}}({\mathcal {P}}(\varnothing ))}
булеан булеана пустого множества. 2. Связь между схемой преобразования и схемой выделения выражается следующим высказыванием:
∀
a
(
x
∈
{
b
:
b
∈
a
∧
Φ
[
b
]
}
∧
(
ϕ
[
b
′
,
y
]
↔
(
Φ
[
b
′
]
→
y
=
b
′
)
∧
(
¬
Φ
[
b
′
]
→
y
=
x
)
)
→
(
∃
d
∀
c
(
c
∈
d
↔
∃
b
(
b
∈
a
∧
ϕ
[
b
,
c
]
)
)
↔
∃
c
∀
b
(
b
∈
c
↔
b
∈
a
∧
Φ
[
b
]
)
)
)
{\displaystyle {\begin{aligned}\forall a\ (\ x\in \{b:b\in a\land \Phi [b]\}\quad \land \quad (\phi [b',y]\ \leftrightarrow \ (\Phi [b']\to y=b')\land (\neg \Phi [b']\to y=x)\ )\\\ \to \quad (\exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in a\land \phi [b,c]))\ \leftrightarrow \ \exists c\forall b\ (b\in c\leftrightarrow b\in a\land \Phi [b]))\ )\end{aligned}}}
Историческая справка
править
![{\displaystyle \forall x\exists ^{\{1\}}y\ (\phi [x,y])\to \forall a\exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in a\ \land \ \phi [b,c])\ )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d6d99111e6dfacf23d1bd36efc8a06eca82891f5)
![{\displaystyle \forall x\exists ^{\{1\}}y\ (\phi [x,y])\Leftrightarrow \forall x\exists !y\ (\phi [x,y])\Leftrightarrow \forall x\exists y\forall y'(\phi [x,y]\leftrightarrow y=y')}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1c0effd6518671747750df776979e0d447d8cecf)
![{\displaystyle \phi [x,y]\leftrightarrow y=x\quad \Rightarrow \quad \forall a\exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in a\ \land \ c=b))\quad \Leftrightarrow \quad \forall a\exists d\forall c\ (c\in d\leftrightarrow c\in a)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/87ad526219eb846bd217de2e3629f01cd1c9d41d)
![{\displaystyle \forall a\ (\ \forall b\ (b\in a\to \exists ^{\{1\}}y\ (\phi [b,y])\ )\quad \to \quad \exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in a\ \land \ \phi [b,c])\ ))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e221b8cfa9d98bad98683d272dab78c6bcd3d3f4)
![{\displaystyle {\begin{aligned}a=\mathbb {N} \ \land \ (\phi [b',y]\leftrightarrow y=2b')\quad \Rightarrow \quad \exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in \mathbb {N} \ \land \ c=2b))\\\ \Leftrightarrow \exists d\forall c\ (c\in d\leftrightarrow c\in \{0,2,4,...\})\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ac0e63ee288d0d4aac68b496224ce77597bb453a)
![{\displaystyle {\begin{aligned}a=\mathbb {R} \quad \land \quad (\phi [b',y]\leftrightarrow (b'=0\to y=a_{1})\ \land \ (b'\neq 0\to y=a_{2}))\quad \Rightarrow \\\ \exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in \mathbb {R} \ \land \ (b=0\to c=a_{1})\land (b\neq 0\to c=a_{2})\ ))\\\ \Leftrightarrow \exists d\forall c\ (c\in d\leftrightarrow c=a_{1}\ \lor \ c=a_{2})\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/562294cf3a7036c3f4b0588d9f0247e1d9535e5a)
![{\displaystyle {\begin{aligned}a=\mathbb {Z} \quad \land \quad (\phi [b',y]\leftrightarrow (0\leq b'\leq 1\to y=b')\land (\neg (0\leq b'\leq 1)\to y=1))\quad \Rightarrow \\\ \exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in \mathbb {Z} \land (0\leq b\leq 1\to c=b)\land (b<0\lor b>1\to c=1)))\\\ \Leftrightarrow \exists d\forall c\ (c\in d\leftrightarrow c\in \{n:\ n\in \mathbb {N} \ \land \ n<2\}\ )\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f445dafb78f598388851fca2cb6ceeca52232124)
![{\displaystyle \forall a\ (\ \forall b\ (b\in a\to \exists ^{\{0,1\}}y\ (\phi [b,y]))\quad \to \quad \exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in a\ \land \ \phi [b,c])\ ))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e4f7f709637f54fb1788ce624d609d71d96fe25c)
![{\displaystyle \exists ^{\{0,1\}}y\ (\phi [b,y])\Leftrightarrow \forall y\forall y'\ (\phi [b,y]\ \land \ \phi [b,y']\to y=y')}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6f11c89ab2a6e6d3076ae199208d44bffe1d207d)
![{\displaystyle {\begin{aligned}\forall a_{1}\forall a_{2}\ (a={\mathcal {P}}({\mathcal {P}}(\varnothing ))\quad \land \quad (\phi [b',y]\ \leftrightarrow \ (b'=\varnothing \to y=a_{1})\land (b'\neq \varnothing \to y=a_{2})\ )\\\ \rightarrow \quad (\exists d\forall c\ (c\in d\ \leftrightarrow \ \exists b\ (b\in a\land \phi [b,c]))\ \rightarrow \ \exists c\forall b\ (b\in c\leftrightarrow b=a_{1}\lor b=a_{2})\ )),\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d7d8cc95fb9192ed314de121d2af4c9c78dba338)
![{\displaystyle {\begin{aligned}\forall a\ (\ x\in \{b:b\in a\land \Phi [b]\}\quad \land \quad (\phi [b',y]\ \leftrightarrow \ (\Phi [b']\to y=b')\land (\neg \Phi [b']\to y=x)\ )\\\ \to \quad (\exists d\forall c\ (c\in d\leftrightarrow \exists b\ (b\in a\land \phi [b,c]))\ \leftrightarrow \ \exists c\forall b\ (b\in c\leftrightarrow b\in a\land \Phi [b]))\ )\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d044534bf04a21cdf6bd26c2bec7c195d5df8e43)