Схема преобразования
Схемой преобразования [множеств] (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}}}
Схема преобразования не вошла в совокупность аксиом теории множеств, сформулированных немецким математиком Эрнстом Цермело в 1908 году.
Схема преобразования предложена Адольфом Френкелем в 1922 году , чуть позднее и независимо от него схема была предложена норвежским математиком Туральфом Скулемом .
![{\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)
