This commit is contained in:
parent
883ee88516
commit
0771440511
4 changed files with 28 additions and 26 deletions
|
@ -41,7 +41,8 @@ all condensation points are accumulation points.
|
||||||
Fix $A \subseteq \R$ closed.
|
Fix $A \subseteq \R$ closed.
|
||||||
We want to see that $A$ is at most countable
|
We want to see that $A$ is at most countable
|
||||||
or there is some perfect $P \subseteq A$.
|
or there is some perfect $P \subseteq A$.
|
||||||
Let $P \coloneqq \{x \in \R | x \text{ is a condensation point of $A$}\}$.
|
Let
|
||||||
|
\[P \coloneqq \{x \in \R | x \text{ is a condensation point of $A$}\}.\]
|
||||||
Since $A $ is closed, $P \subseteq A$.
|
Since $A $ is closed, $P \subseteq A$.
|
||||||
|
|
||||||
\begin{claim}
|
\begin{claim}
|
||||||
|
|
|
@ -9,7 +9,7 @@
|
||||||
$\ZFC$ stands for
|
$\ZFC$ stands for
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item \textsc{Zermelo}’s axioms (1905), % crises around 19000
|
\item \textsc{Zermelo}’s axioms (1905), % crises around 19000
|
||||||
\item \vocab{Fraenkel}'s axioms,
|
\item \textsc{Fraenkel}'s axioms,
|
||||||
\item the axiom of choice.
|
\item the axiom of choice.
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
\begin{notation}
|
\begin{notation}
|
||||||
|
|
|
@ -18,74 +18,74 @@ has the following axioms:
|
||||||
\begin{axiom}[Extensionality]
|
\begin{axiom}[Extensionality]
|
||||||
\yalabel{Axiom of Extensionality}{(Ext)}{ax:bg:ext}
|
\yalabel{Axiom of Extensionality}{(Ext)}{ax:bg:ext}
|
||||||
\[
|
\[
|
||||||
\forall x, y. \left( x = y \iff \left( \forall z.~(z \in x \iff z \in y \right) \right).
|
\forall x.~\forall y.~ \left( x = y \iff \left( \forall z.~(z \in x \iff z \in y \right) \right).
|
||||||
\]
|
\]
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
\begin{axiom}[Foundation]
|
\begin{axiom}[Foundation]
|
||||||
\yalabel{Axiom of Foundation}{(Fund)}{ax:bg:fund}
|
\yalabel{Axiom of Foundation}{(Fund)}{ax:bg:fund}
|
||||||
\[
|
\[
|
||||||
\forall x .(x \neq \emptyset \implies \exists y \in x . y \cap x = \emptyset).
|
\forall x .~(x \neq \emptyset \implies \exists y \in x .~ y \cap x = \emptyset).
|
||||||
\]
|
\]
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
|
|
||||||
\begin{axiom}[Pairing]
|
\begin{axiom}[Pairing]
|
||||||
\yalabel{Axiom of Pairing}{(Pair)}{ax:bg:pair}
|
\yalabel{Axiom of Pairing}{(Pair)}{ax:bg:pair}
|
||||||
\[
|
\[
|
||||||
\forall x \forall y \exists z . z = \{x,y\}.
|
\forall x.~\forall y . ~\exists z .~ z = \{x,y\}.
|
||||||
\]
|
\]
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
|
|
||||||
\begin{axiom}[Union]
|
\begin{axiom}[Union]
|
||||||
\yalabel{Axiom of Union}{(Union)}{ax:bg:union}
|
\yalabel{Axiom of Union}{(Union)}{ax:bg:union}
|
||||||
\[
|
\[
|
||||||
\forall x \exists y .~ y = \bigcup x.
|
\forall x .~\exists y .~ y = \bigcup x.
|
||||||
\]
|
\]
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
\begin{axiom}[Power]
|
\begin{axiom}[Power]
|
||||||
\yalabel{Powerset Axiom}{(Pow)}{ax:bg:pow}
|
\yalabel{Powerset Axiom}{(Pow)}{ax:bg:pow}
|
||||||
\[
|
\[
|
||||||
\forall x \exists y .~ y = \cP(x).
|
\forall x .~\exists y .~ y = \cP(x).
|
||||||
\]
|
\]
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
|
|
||||||
\begin{axiom}[Infinity]
|
\begin{axiom}[Infinity]
|
||||||
\yalabel{Axiom of Infinity}{(Infinity)}{ax:bg:inf}
|
\yalabel{Axiom of Infinity}{(Infinity)}{ax:bg:inf}
|
||||||
\[
|
\[
|
||||||
\exists x . ~(\emptyset \in x \land \left( \forall y \in x .~y \cup \{y\} \in x \right)).
|
\exists x .~(\emptyset \in x \land \left( \forall y \in x .~y \cup \{y\} \in x \right)).
|
||||||
\]
|
\]
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
|
|
||||||
Together with the following axioms for classes:
|
Together with the following axioms for classes:
|
||||||
|
|
||||||
\begin{axiom}[Extensionality for classes]
|
\begin{axiom}[Extensionality for classes]
|
||||||
\[
|
\[
|
||||||
\forall X \forall Y \left( \forall x(x \in X \iff y \in X) \implies X = Y).
|
\forall X .~\forall Y.~ \left( \forall x.~(x \in X \iff x \in Y) \implies X = Y\right).
|
||||||
\]
|
\]
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
|
|
||||||
\begin{axiom}
|
\begin{axiom}
|
||||||
Every set is a class:
|
Every set is a class:
|
||||||
\[
|
\[
|
||||||
\forall x \exists X. x = X.
|
\forall x.~ \exists X.~ x = X.
|
||||||
\]
|
\]
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
\begin{axiom}
|
\begin{axiom}
|
||||||
Every element of a class is a set:
|
Every element of a class is a set:
|
||||||
\[
|
\[
|
||||||
\forall X \exists Y.~(X \in Y \to \exists x.~x = X).
|
\forall X .~\exists Y.~(X \in Y \to \exists x.~x = X).
|
||||||
\]
|
\]
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
\begin{axiom}[Replacement]
|
\begin{axiom}[Replacement]
|
||||||
\yalabel{Axiom of Replacement}{(Rep)}{ax:bg:rep}
|
\yalabel{Axiom of Replacement}{(Rep)}{ax:bg:rep}
|
||||||
|
|
||||||
If $F$ is a function and inf $a $ is a set,
|
If $F$ is a function and $a$ is a set,
|
||||||
then $F"a$ is a set.
|
then $F\,''a$ is a set.
|
||||||
\end{axiom}
|
\end{axiom}
|
||||||
Here a \vocab[Class function]{(class) function} is a class
|
Here a \vocab[Class function]{(class) function} is a class
|
||||||
consisting of pairs $(x,y)$,
|
consisting of pairs $(x,y)$,
|
||||||
such that for every $x$ there is at most one $y$
|
such that for every $x$ there is at most one $y$
|
||||||
with $(x,y) \in F$.
|
with $(x,y) \in F$.
|
||||||
Furthermore $F"a \coloneqq \{y : \exists x \in a .~(x,y) \in F\}$.
|
Furthermore $F\,''a \coloneqq \{y : \exists x \in a .~(x,y) \in F\}$.
|
||||||
|
|
||||||
\begin{remark}
|
\begin{remark}
|
||||||
Note that we didn't need to use an axiom schema,
|
Note that we didn't need to use an axiom schema,
|
||||||
|
@ -94,10 +94,9 @@ Furthermore $F"a \coloneqq \{y : \exists x \in a .~(x,y) \in F\}$.
|
||||||
|
|
||||||
\begin{axiom}[Comprehension]
|
\begin{axiom}[Comprehension]
|
||||||
\yalabel{Axiom of Comprehension}{(Comp)}{ax:bg:comp}
|
\yalabel{Axiom of Comprehension}{(Comp)}{ax:bg:comp}
|
||||||
|
|
||||||
\[
|
\[
|
||||||
\forall X_1 \ldots \forall X_k .~\exists Y ( \forall x .~x \in Y \iff \phi(x,X_1,\ldots, X_k))
|
\forall X_1 .~\ldots \forall X_k .~\exists Y.~ ( \forall x .~x \in Y \iff \phi(x,X_1,\ldots, X_k))
|
||||||
\]
|
\]
|
||||||
where $\phi(x, X_1, \ldots, X_k)$
|
where $\phi(x, X_1, \ldots, X_k)$
|
||||||
is a formula which contains exactly $X_1, \ldots, X_k, x$
|
is a formula which contains exactly $X_1, \ldots, X_k, x$
|
||||||
as free variables,
|
as free variables,
|
||||||
|
|
|
@ -113,6 +113,8 @@
|
||||||
\DeclareSimpleMathOperator{HOD}
|
\DeclareSimpleMathOperator{HOD}
|
||||||
\DeclareSimpleMathOperator{OD}
|
\DeclareSimpleMathOperator{OD}
|
||||||
\DeclareSimpleMathOperator{AC}
|
\DeclareSimpleMathOperator{AC}
|
||||||
|
\newcommand{\AxC}{\yarefs{ax:c}}
|
||||||
|
\newcommand{\AxSep}{\yarefs{ax:sep}} % Separation
|
||||||
\newcommand{\Choice}{\yarefs{ax:c}}
|
\newcommand{\Choice}{\yarefs{ax:c}}
|
||||||
% \DeclareSimpleMathOperator{Choice}
|
% \DeclareSimpleMathOperator{Choice}
|
||||||
% \DeclareSimpleMathOperator{Fund}
|
% \DeclareSimpleMathOperator{Fund}
|
||||||
|
|
Loading…
Reference in a new issue