This commit is contained in:
parent
32c8b3214b
commit
6936663173
4 changed files with 156 additions and 6 deletions
|
@ -111,6 +111,31 @@ Furthermore $F\,''a \coloneqq \{y : \exists x \in a .~(x,y) \in F\}$.
|
|||
\todo{notation: $\emptyset, \cap$}
|
||||
|
||||
|
||||
\todo{the following was actually done in lecture 9}
|
||||
|
||||
$\BGC$ (in German often NBG) is defined to be $\BG$
|
||||
together with the additional axiom:
|
||||
\begin{axiom}[Choice]
|
||||
\[
|
||||
\exists F.~(F \text{ is a function} \land \forall x \neq \emptyset. F(x) \in x).
|
||||
\]
|
||||
\end{axiom}
|
||||
\begin{fact}
|
||||
$\BGC$ is conservative over $\ZFC$,
|
||||
i.e.~for all formulae $\phi$ in the language
|
||||
of set theory (only set variables):
|
||||
if $\BGC \vdash \phi$ then $\ZFC \vdash \phi$.
|
||||
\end{fact}
|
||||
We cannot prove this fact at this point,
|
||||
as the proof requires forcing.
|
||||
The converse is easy however, i.e.~if
|
||||
$\ZFC \vdash \phi$ then $\BGC \vdash \phi$.
|
||||
|
||||
\begin{notation}
|
||||
From now on, objects denoted by capital letters
|
||||
are (potentially proper) classes.
|
||||
\end{notation}
|
||||
|
||||
|
||||
\subsection{Induction and Recursion}
|
||||
|
||||
|
@ -230,9 +255,3 @@ Furthermore $F\,''a \coloneqq \{y : \exists x \in a .~(x,y) \in F\}$.
|
|||
The construction of $g$ in the previous proof was a special case of
|
||||
a construction on the proof of the recursion theorem: % TODO REF
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
128
inputs/lecture_09.tex
Normal file
128
inputs/lecture_09.tex
Normal file
|
@ -0,0 +1,128 @@
|
|||
\lecture{09}{2023-11-16}{}
|
||||
|
||||
|
||||
\begin{definition}
|
||||
Let $R$ be a binary relation.
|
||||
$R$ is called \vocab{well-founded}
|
||||
if for all classes $X$,
|
||||
there is an $R$-least $y$ such that
|
||||
there is no $z \in X$ with $(z,y) \in R$.
|
||||
\end{definition}
|
||||
|
||||
\begin{theorem}[Induction (again, but now with classes)]
|
||||
Suppose that $R$ is a well-founded relation.
|
||||
Let $X$ be a class such that for all sets $x$,
|
||||
\[
|
||||
\{y : (y,x) \in R\} \subseteq X \implies x \in X.
|
||||
\]
|
||||
Then $X$ contains all sets.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
Assume otherwise.
|
||||
Consider $Y = \{x : x \not\in X\} \neq \emptyset$.
|
||||
By hypothesis, there is some
|
||||
$x \in Y$ such that $(y,x) \not\in R$ for all $y \in Y$.
|
||||
In other words, if $(y,x) \not\in R$,
|
||||
then $x \not\in Y$, i.e.~$x \in X$.
|
||||
Thus $\{y: (y,x) \in R\} \subseteq X$.
|
||||
Hence $x \in X \lightning$.
|
||||
\end{proof}
|
||||
|
||||
An alternative way of formulating this is
|
||||
\begin{theorem}
|
||||
Suppose $R$ is a well-founded binary relation on $A$,
|
||||
i.e.~$R \subseteq A \times A$.
|
||||
Suppose for all $\overline{A} \subseteq A$
|
||||
is such that for all $x \in X$,
|
||||
\[
|
||||
\{y \in A: (y,x) \in R\} \subseteq \overline{A} \implies x \in \overline{A}.
|
||||
\]
|
||||
Then $\overline{A} = A$.
|
||||
\end{theorem}
|
||||
|
||||
\begin{definition}
|
||||
Let $R$ be a binary relation.
|
||||
$R$ is called \vocab{set-like}
|
||||
iff for all $x$,
|
||||
$\{y : (y,x) \in R\}$ is a set.
|
||||
\end{definition}
|
||||
|
||||
\begin{theorem}
|
||||
Let $R$ be a well-founded
|
||||
and set-like relation on $A$ (i.e.~$R \subseteq A \times A$).
|
||||
|
||||
Let $D$ be a class of triples
|
||||
such that for all $u,x$ there is exactly
|
||||
one $y$ with $(u,x,y) \in D$
|
||||
(basicalls $(u,x) \mapsto y$ is a function).
|
||||
|
||||
Then there is a unique function $f$ on $A$
|
||||
such that for all $x \in A$,
|
||||
\[
|
||||
(F\defon{ \{y \in A : (y,x) \in R\}}, x, F(x)) \in D.
|
||||
\]
|
||||
I.e.~$F(x)$ is computed from $F\defon{\{y \in A: (y,x) \in R\}}$.
|
||||
\end{theorem}
|
||||
\begin{proof}
|
||||
Uniqueness:
|
||||
|
||||
Let $F, F'$ be two such functions.
|
||||
Suppose that $\overline{A} = \{ x \in A : F(x) \neq F'(x)\} \neq \emptyset$.
|
||||
As $R$ is well-founded,
|
||||
there is some $x \in \overline{A}$
|
||||
such that $y \not\in \overline{A}$
|
||||
for all $y \in A, (y,x) \in R$.
|
||||
I.e. $F(y) = F'(y)$
|
||||
for all $y \in A$, $(y,x) \in R$.
|
||||
|
||||
But then $F(x)$
|
||||
is the unique $y$
|
||||
with $(F\defon{\{z\colon (z,x) \in R\}}, x, y) \in D$,
|
||||
in particular it is the same as $F'(x) \lightning$
|
||||
|
||||
|
||||
Existence:
|
||||
|
||||
Let us call a (set) function $f$
|
||||
\emph{good},
|
||||
if
|
||||
\begin{itemize}
|
||||
\item $\dom(f) \subseteq A$,
|
||||
\item if $x \in \dom(f)$ and $y \in A, (y,x) \in R$,
|
||||
then $y \in \dom(f)$ and
|
||||
\item for all $x \in \dom(f)$ :
|
||||
\[
|
||||
(f\defon{\{y \in A: (y,x) \in R\}}, x, f(x)) \in D.
|
||||
\]
|
||||
\end{itemize}
|
||||
|
||||
|
||||
By the proof of uniqueness,
|
||||
we have that all good functions are coherent,
|
||||
i.e.~$f(x) = f'(x)$ for good functions
|
||||
$f,f'$ and all $x \in \dom(f) \cap \dom(f')$.
|
||||
We may now let $F = \bigcup \{f: f \text{ is good}\}$,
|
||||
this exists by comprehension.
|
||||
|
||||
If $x \in \dom(F)$ and $y \in A$ with $(y,x) \in R$,
|
||||
then $y \in \dom(F)$
|
||||
and $(F\defon{\{y : (y,x) \in R\}}, x,F(x)) \in D$.
|
||||
|
||||
We need to show that $\dom(F) = A$.
|
||||
This holds by induction:
|
||||
Suppose for a contradiction that $A \setminus \dom(F) \neq \emptyset$.
|
||||
Then there exists an $R$-least element $x$ in this set,
|
||||
i.e.$x \not\in \dom(F)$,
|
||||
but $y \in \dom(F)$ for all $(y,x) \in R$.
|
||||
For each $y \in A$ with $(y,x) \in R$,
|
||||
pick some good function $f_y$ with $y \in \dom(f_y)$
|
||||
Since $R$ is set-like,
|
||||
we have that $f = \bigcup_y f_y$ is a good function.
|
||||
But then $f \cup (x,z)$,
|
||||
where $z$ is unique such that $(f\defon{\{y : (y,x) \in R\}}, x, z) \in D$,
|
||||
is good $\lightning$.
|
||||
\end{proof}
|
||||
|
||||
|
||||
|
||||
|
|
@ -110,6 +110,8 @@
|
|||
\DeclareMathOperator{\Zermelo}{Z}
|
||||
\DeclareSimpleMathOperator{ZF}
|
||||
\DeclareSimpleMathOperator{ZFC}
|
||||
\DeclareSimpleMathOperator{BG}
|
||||
\DeclareSimpleMathOperator{BGC}
|
||||
\DeclareSimpleMathOperator{HOD}
|
||||
\DeclareSimpleMathOperator{OD}
|
||||
\DeclareSimpleMathOperator{AC}
|
||||
|
|
|
@ -32,6 +32,7 @@
|
|||
\input{inputs/lecture_06}
|
||||
\input{inputs/lecture_07}
|
||||
\input{inputs/lecture_08}
|
||||
\input{inputs/lecture_09}
|
||||
|
||||
|
||||
\cleardoublepage
|
||||
|
|
Loading…
Reference in a new issue