-
Notifications
You must be signed in to change notification settings - Fork 41
/
lection13.tex
36 lines (31 loc) · 1.81 KB
/
lection13.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
\section{Лекция 13}
\subsection{Теорема Диаконеску}
\begin{theorem}[Диаконеску]
В аксиомах ZF аксиома выбора влечет закон исключенного третьего.
\end{theorem}
\begin{proof}
По аксиоме выделения для любого утверждения $P$ мы можем построить два множества из множества \{0, 1\}:
\[
A = \set{x \in \set{0, 1} \mid \left(x = 0\right) \lor P} \qquad
B = \set{x \in \set{0, 1} \mid \left(x = 1\right) \lor P}
\]
По аксиоме выбора мы знаем, что их декартово произведение непусто.
Иначе говоря, существует функция $f : \set{A, B} \to \set{0, 1}$, что
\[
f(A) \in A \with f(B) \in B
\]
Это, по определению двух множеств, эквивалентно
\[
\left(f(A) = 0 \vee P\right) \with \left(f(B) = 1 \vee P\right)
\]
Из этого следует, что
\begin{gather}
\left(f(A) \neq f(B)\right) \vee P \label{firstOption} \tag{$*$}
\end{gather}
Однако, по принципу объёмности $P \to \left(A=B\right)$. Значит, $P \to \left(f(A) = f(B)\right)$. Значит,
\begin{gather}
\left(f(A) \neq f(B)\right) \to \neg P \label{secondOption} \tag{$**$}
\end{gather}
Из \ref{firstOption} и \ref{secondOption} можно вывести $P \vee \neg P$.
\end{proof}
Важным следствием данной теоремы является то, что мы не можем воспринимать типы как множества, так как системы типов изоморфны интуиционистской логике, в которой нет закона исключенного третьего.