josia-notes/w23-logic-2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

yaref dependencies
Some checks failed
Build latex and deploy / checkout (push) Failing after 15m58s
Details

Browse source
This commit is contained in:
Josia Pietsch 2024-02-16 23:28:14 +01:00
parent ab14be172f
commit 9956de5277
Signed by: josia
GPG key ID: E70B571D66986A2D
11 changed files with 81 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
inputs/lecture_02.tex
View file

@ -40,7 +40,7 @@
\label{lem:closedaccumulation} \label{lem:closedaccumulation}
A set $A \subseteq \R$ is closed iff $A' \subseteq A$. A set $A \subseteq \R$ is closed iff $A' \subseteq A$.
\end{lemma} \end{lemma}
\begin{refproof}{lem:closedaccumulation} \begin{yarefproof}{lem:closedaccumulation}
``$\implies$'' ``$\implies$''
\gist{% \gist{%
Let $A$ be closed. Suppose that $x \in A' \setminus A$. Let $A$ be closed. Suppose that $x \in A' \setminus A$.
@ -75,7 +75,7 @@
there would be some Cauchy-sequence $(x_n)$ there would be some Cauchy-sequence $(x_n)$
in $A$ such that $\lim_{n \to \infty} x_n \not\in A$. in $A$ such that $\lim_{n \to \infty} x_n \not\in A$.
But then $x \in A' \subseteq A \lightning$. But then $x \in A' \subseteq A \lightning$.
\end{refproof} \end{yarefproof}
\begin{definition} \begin{definition}
$P \subseteq \R$ (or, more generally, a subset of any topological space) $P \subseteq \R$ (or, more generally, a subset of any topological space)
is called \vocab{perfect} is called \vocab{perfect}

4
inputs/lecture_03.tex
View file

@ -37,7 +37,7 @@
By the fact we just proved, By the fact we just proved,
all condensation points are accumulation points. all condensation points are accumulation points.
\begin{refproof}{thm:cantorbendixson} \begin{yarefproof}{thm:cantorbendixson}
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$.
@ -109,7 +109,7 @@ all condensation points are accumulation points.
\[ \[
A = \overbrace{P}^{\mathclap{\text{perfect, unless $= \emptyset$}}} \cup \underbrace{(A \setminus P)}_{\mathclap{\text{at most countable}}}. A = \overbrace{P}^{\mathclap{\text{perfect, unless $= \emptyset$}}} \cup \underbrace{(A \setminus P)}_{\mathclap{\text{at most countable}}}.
\] \]
\end{refproof} \end{yarefproof}
\gist{\todo{Alternative proof of Cantor-Bendixson}}{} \gist{\todo{Alternative proof of Cantor-Bendixson}}{}
% \begin{remark} % \begin{remark}

4
inputs/lecture_06.tex
View file

@ -7,7 +7,7 @@
and $ b$ linearly ordered, $b$ has an upper bound. and $ b$ linearly ordered, $b$ has an upper bound.
Then $a$ has a maximal element. Then $a$ has a maximal element.
\end{theorem} \end{theorem}
\begin{refproof}{thm:zorn} \begin{yarefproof}{thm:zorn}
\gist{% \gist{%
Fix $(a, \le )$ as in the hypothesis. Fix $(a, \le )$ as in the hypothesis.
Let $A \coloneqq \{ \{(b,x) : x \in b\} : b \subseteq a, b \neq \emptyset\}$. Let $A \coloneqq \{ \{(b,x) : x \in b\} : b \subseteq a, b \neq \emptyset\}$.
@ -96,7 +96,7 @@
\end{itemize} \end{itemize}
} }
\end{refproof} \end{yarefproof}
\begin{remark} \begin{remark}
Over $\ZF$ the \yaref{ax:c} and \yaref{thm:zorn} Over $\ZF$ the \yaref{ax:c} and \yaref{thm:zorn}

4
inputs/lecture_07.tex
View file

@ -19,7 +19,7 @@
or $\alpha \ni \beta$. or $\alpha \ni \beta$.
\end{enumerate} \end{enumerate}
\end{lemma} \end{lemma}
\begin{refproof}{lem:7:ordinalfacts} \begin{yarefproof}{lem:7:ordinalfacts}
\gist{ \gist{
We have already proved (a) before. We have already proved (a) before.
@ -115,7 +115,7 @@
as $\alpha_0 \in \beta_0 \in \alpha_0$. as $\alpha_0 \in \beta_0 \in \alpha_0$.
\end{subproof} \end{subproof}
}{Long and tedious, but not many ideas.} }{Long and tedious, but not many ideas.}
\end{refproof} \end{yarefproof}
\begin{lemma} \begin{lemma}
Let $X$ be a set of ordinals, Let $X$ be a set of ordinals,

4
inputs/lecture_11.tex
View file

@ -137,7 +137,7 @@ so $|a| = \aleph_\beta$ for some $\beta \le |\alpha|$.
\] \]
}{Then $\aleph_{\beta} \le \aleph_\alpha + \aleph_{\beta} \le \aleph_\alpha \cdot \aleph_\beta \le \aleph_\beta \cdot \aleph_\beta = \aleph_\beta$.} }{Then $\aleph_{\beta} \le \aleph_\alpha + \aleph_{\beta} \le \aleph_\alpha \cdot \aleph_\beta \le \aleph_\beta \cdot \aleph_\beta = \aleph_\beta$.}
\end{proof} \end{proof}
\begin{refproof}{thm:hessenberg} \begin{yarefproof}{thm:hessenberg}
\gist{% \gist{%
Define a well-order $<^\ast$ on $\OR \times \OR$ by setting Define a well-order $<^\ast$ on $\OR \times \OR$ by setting
\[ \[
@ -218,7 +218,7 @@ so $|a| = \aleph_\beta$ for some $\beta \le |\alpha|$.
\end{itemize} \end{itemize}
\end{itemize} \end{itemize}
} }
\end{refproof} \end{yarefproof}
\gist{% \gist{%
However, exponentiation of cardinals is far from trivial: However, exponentiation of cardinals is far from trivial:
\begin{observe} \begin{observe}

8
inputs/lecture_14.tex
View file

@ -37,7 +37,7 @@
Clearly this is club Clearly this is club
but $\bigcap_{\beta < \kappa} C_\beta = \emptyset$. but $\bigcap_{\beta < \kappa} C_\beta = \emptyset$.
\end{warning} \end{warning}
\begin{refproof}{lem:clubintersection} \begin{yarefproof}{lem:clubintersection}
\gist{% \gist{%
First let $\alpha = 2$. First let $\alpha = 2$.
Let $C, D \subseteq \kappa$ Let $C, D \subseteq \kappa$
@ -97,7 +97,7 @@
(we used $\cf(\kappa) > \alpha\cdot \omega$). (we used $\cf(\kappa) > \alpha\cdot \omega$).
\end{itemize} \end{itemize}
} }
\end{refproof} \end{yarefproof}
\begin{definition} \begin{definition}
$F \subseteq \cP(a)$ is a \vocab{filter} $F \subseteq \cP(a)$ is a \vocab{filter}
@ -172,7 +172,7 @@ We have shown (assuming \AxC to choose contained clubs):
then $\diagi_{\beta < \kappa} C_{\beta}$ then $\diagi_{\beta < \kappa} C_{\beta}$
contains a club. contains a club.
\end{lemma} \end{lemma}
\begin{refproof}{lem:diagiclub} \begin{yarefproof}{lem:diagiclub}
% TODO THINK % TODO THINK
\gist{ \gist{
Let us fix $\langle C_{\beta} : \beta < \alpha \rangle$. Let us fix $\langle C_{\beta} : \beta < \alpha \rangle$.
@ -277,7 +277,7 @@ We have shown (assuming \AxC to choose contained clubs):
\end{itemize} \end{itemize}
} }
\end{refproof} \end{yarefproof}
\begin{remark}+ \begin{remark}+
$\diagi_{\beta < \kappa} C_{\beta}$ actually $\diagi_{\beta < \kappa} C_{\beta}$ actually
\emph{is} a club, \emph{is} a club,

12
inputs/lecture_15.tex
View file

@ -105,7 +105,7 @@ to be an elementary substructure of $V_\theta$.
\end{lemma} \end{lemma}
Let's do a second proof of \yaref{thm:fodor}. Let's do a second proof of \yaref{thm:fodor}.
\begin{refproof}{thm:fodor} \begin{yarefproof}{thm:fodor}
\gist{% \gist{%
Fix $\theta > \kappa$ and look at $V_{\theta}$. Fix $\theta > \kappa$ and look at $V_{\theta}$.
@ -151,7 +151,7 @@ Let's do a second proof of \yaref{thm:fodor}.
such that $X_\xi \cap \kappa = \xi$ such that $X_\xi \cap \kappa = \xi$
for all $\xi \in C$. for all $\xi \in C$.
\end{claim} \end{claim}
\begin{refproof}{thm:fodor:p2:c1} \begin{yarefproof}{thm:fodor:p2:c1}
Write $C = \{\xi < \kappa:X_\xi \cap \kappa = \xi\}$. Write $C = \{\xi < \kappa:X_\xi \cap \kappa = \xi\}$.
Trivially $C$ is closed. Trivially $C$ is closed.
Let us show that $C$ is unbounded in $\kappa$. Let us show that $C$ is unbounded in $\kappa$.
@ -171,7 +171,7 @@ Let's do a second proof of \yaref{thm:fodor}.
\label{thm:fodor:p2:c1.1} \label{thm:fodor:p2:c1.1}
$\xi \in C$, i.e.~$X_\xi \cap \kappa = \xi$. $\xi \in C$, i.e.~$X_\xi \cap \kappa = \xi$.
\end{claim} \end{claim}
\begin{refproof}{thm:fodor:p2:c1.1} \begin{yarefproof}{thm:fodor:p2:c1.1}
If $\eta < \xi$, If $\eta < \xi$,
then $\eta < \xi_n$ for some $n$ then $\eta < \xi_n$ for some $n$
and then $\eta \in \xi_n \subseteq X_{\xi_n} \subseteq X_{\xi}$. and then $\eta \in \xi_n \subseteq X_{\xi_n} \subseteq X_{\xi}$.
@ -180,8 +180,8 @@ Let's do a second proof of \yaref{thm:fodor}.
Then $\eta \in X_{\xi_n}$ for some $n < \omega$, Then $\eta \in X_{\xi_n}$ for some $n < \omega$,
so $\eta < \xi_{n+1} < \xi$, so $\eta < \xi_{n+1} < \xi$,
hence $X_{\xi} \cap \kappa \subseteq \xi$. hence $X_{\xi} \cap \kappa \subseteq \xi$.
\end{refproof} \end{yarefproof}
\end{refproof} \end{yarefproof}
Now let $\alpha \in S \cap C$, Now let $\alpha \in S \cap C$,
i.e.~$X_\alpha \prec V_{\theta}$ i.e.~$X_\alpha \prec V_{\theta}$
and $\alpha = X_{\alpha} \cap \kappa$. and $\alpha = X_{\alpha} \cap \kappa$.
@ -280,4 +280,4 @@ Let's do a second proof of \yaref{thm:fodor}.
\end{itemize} \end{itemize}
\end{itemize} \end{itemize}
} }
\end{refproof} \end{yarefproof}

4
inputs/lecture_16.tex
View file

@ -101,7 +101,7 @@ one cofinality.
\begin{refproof}{thm:solovay}% \begin{yarefproof}{thm:solovay}%
\gist{% \gist{%
\footnote{``This is one of the arguments where it is certainly worth it to look at it again.''} \footnote{``This is one of the arguments where it is certainly worth it to look at it again.''}
We will only prove this for $\aleph_1$. We will only prove this for $\aleph_1$.
@ -253,7 +253,7 @@ one cofinality.
\item $S_0 \coloneqq T_0 \cup \left( S \setminus \bigcup_{j > 0} T_j \right)$, $S_i \coloneqq T_i$. \item $S_0 \coloneqq T_0 \cup \left( S \setminus \bigcup_{j > 0} T_j \right)$, $S_i \coloneqq T_i$.
\end{itemize} \end{itemize}
} }
\end{refproof} \end{yarefproof}
\gist{% \gist{%
We now want to do another application of \yaref{thm:fodor}. We now want to do another application of \yaref{thm:fodor}.
Recall that $2^{\kappa} > \kappa$, in fact $\cf(2^{\kappa}) > \kappa$ Recall that $2^{\kappa} > \kappa$, in fact $\cf(2^{\kappa}) > \kappa$

4
inputs/lecture_17.tex
View file

@ -25,7 +25,7 @@ We will only prove
\end{remark} \end{remark}
}{} }{}
\begin{refproof}{thm:silver1} \begin{yarefproof}{thm:silver1}
\gist{% \gist{%
We need to count the number of $X \subseteq \aleph_{\omega_1}.$ We need to count the number of $X \subseteq \aleph_{\omega_1}.$
Let us fix $\langle f_\lambda : \lambda < \kappa \text{ an infinite cardinal} \rangle$ Let us fix $\langle f_\lambda : \lambda < \kappa \text{ an infinite cardinal} \rangle$
@ -274,4 +274,4 @@ We will only prove
\end{itemize} \end{itemize}
} }
\end{refproof} \end{yarefproof}

8
inputs/lecture_23.tex
View file

@ -73,7 +73,7 @@ We shall prove:
\footnote{Being a cardinal is $\Pi_1$, \footnote{Being a cardinal is $\Pi_1$,
so $M[h]$ cardinals are always $M$ cardinals.} so $M[h]$ cardinals are always $M$ cardinals.}
\end{claim} \end{claim}
\begin{refproof}{l23:c:2} \begin{yarefproof}{l23:c:2}
Suppose not. Suppose not.
Let $\kappa$ be minimal such that $M \models \text{``$\kappa$ is a cardinal''}$, Let $\kappa$ be minimal such that $M \models \text{``$\kappa$ is a cardinal''}$,
but $M[h] \models \text{``$\kappa$ is not a cardinal''}$. but $M[h] \models \text{``$\kappa$ is not a cardinal''}$.
@ -119,12 +119,12 @@ We shall prove:
But $|\lambda \times \omega| = |\lambda| = \lambda$, But $|\lambda \times \omega| = |\lambda| = \lambda$,
so in $M$ there is a surjection $F' \colon \lambda \to \kappa$, so in $M$ there is a surjection $F' \colon \lambda \to \kappa$,
but $\kappa$ is a cardinal in $M$ $\lightning$. but $\kappa$ is a cardinal in $M$ $\lightning$.
\end{refproof} \end{yarefproof}
\begin{refproof}{l23:c:1} \begin{yarefproof}{l23:c:1}
Omitted. Omitted.
% TODO combinatorial argument % TODO combinatorial argument
\end{refproof} \end{yarefproof}

54
jrpie-yaref.sty
View file

@ -5,6 +5,48 @@
\RequirePackage{amstext} \RequirePackage{amstext}
\RequirePackage{xspace} \RequirePackage{xspace}
\newwrite\yaref@output
\immediate\openout\yaref@output=\jobname.yaref.json
\write\yaref@output{data = [}
\newcounter{yarefproof@depth}
\setcounter{yarefproof@depth}{0}
\edef\yaref@hastag{\string#}%
\let\yaref@oldlabel\label
\def\publicurl{https://josia-notes.users.abstractnonsen.se/w23-logic-2/logic2.pdf}
\newenvironment{yarefproof}[1]{%
\ifnum\the\value{yarefproof@depth}=0%
\global\def\yarefproof@current{#1}%
\fi%
\addtocounter{yarefproof@depth}{1}%
\begin{refproof}{#1}% Depth: \theyarefproof@depth
}{%
\end{refproof}%
\addtocounter{yarefproof@depth}{-1}%
%\ifnum\yarefproof@depth=0%
% \def\yarefproof@current{nothing}%
%\fi%
%\let\yarefproof@current=\undefined%
\ignorespacesafterend%
}
\newcommand{\yaref@writedependency}[1]{%
\ifnum\the\value{yarefproof@depth}=0%
% not in a proof environment
%\write\yaref@output{EDGE: #1 - \theyarefproof@depth}%
\else%
\ifcsname yarefproof@current\endcsname%
\write\yaref@output{{data: {id:"#1\yarefproof@current", source:"#1", target: "\yarefproof@current"}},}%
\else%
% in a proof env, but no label defined ???
%\write\yaref@output{{#1 - ERROR}}%
\fi%
\fi%
}
\newcommand{\yaref@text@large}[1]{% \newcommand{\yaref@text@large}[1]{%
\ifcsname yaref@longlabel@#1\endcsname% \ifcsname yaref@longlabel@#1\endcsname%
\hyperref[#1]{\csname yaref@longlabel@#1\endcsname\ (\ref*{#1})}% \hyperref[#1]{\csname yaref@longlabel@#1\endcsname\ (\ref*{#1})}%
@ -30,14 +72,16 @@
} }
\newcommand{\yalabel}[3]{% \newcommand{\yalabel}[3]{%
\yaref@oldlabel{#3}%
\write\@auxout{\noexpand\expandafter\noexpand\gdef\noexpand\csname yaref@longlabel@#3\noexpand\endcsname{#1}}% \write\@auxout{\noexpand\expandafter\noexpand\gdef\noexpand\csname yaref@longlabel@#3\noexpand\endcsname{#1}}%
\write\@auxout{\noexpand\expandafter\noexpand\gdef\noexpand\csname yaref@shortlabel@#3\noexpand\endcsname{#2}}% \write\@auxout{\noexpand\expandafter\noexpand\gdef\noexpand\csname yaref@shortlabel@#3\noexpand\endcsname{#2}}%
\write\yaref@output{{data: {id: "#3", label: "#1", short: "#2", href: "\publicurl\yaref@hastag\getrefbykeydefault{#3}{anchor}{}"}},}%
\expandafter\gdef\csname yaref@longlabel@#3\endcsname{#1}% \expandafter\gdef\csname yaref@longlabel@#3\endcsname{#1}%
\expandafter\gdef\csname yaref@shortlabel@#3\endcsname{#2}% \expandafter\gdef\csname yaref@shortlabel@#3\endcsname{#2}%
\label{#3}%
} }
\newcommand{\yaref}[1]{% \newcommand{\yaref}[1]{%
\yaref@writedependency{#1}%
\relax\ifmmode% \relax\ifmmode%
\mathchoice \mathchoice
{\yaref@math@large{#1}} % display style {\yaref@math@large{#1}} % display style
@ -50,9 +94,17 @@
} }
% Force a small reference % Force a small reference
\newcommand{\yarefs}[1]{% \newcommand{\yarefs}[1]{%
%\yaref@writedependency{#1}%
\relax\ifmmode% \relax\ifmmode%
\yaref@math@verysmall{#1}% scriptscript style \yaref@math@verysmall{#1}% scriptscript style
\else% \else%
\yaref@text@small{#1}\xspace% \yaref@text@small{#1}\xspace%
\fi% \fi%
} }
\renewcommand{\label}[1]{%
\yaref@oldlabel{#1}%
% \getrefbykeydefault{#1}{name}{}
\write\yaref@output{{data: {id: "#1", label: "\getrefnumber{#1}", href: "\publicurl\yaref@hastag\getrefbykeydefault{#1}{anchor}{}"}},}%
}
\AtEndDocument{\write\yaref@output{{}]}}