From a3f036ff8d1b1958c5ded52598e82d41d5c81f1f Mon Sep 17 00:00:00 2001
From: Spencer Killen <sjkillen@ualberta.ca>
Date: Thu, 7 Nov 2024 06:47:25 -0700
Subject: [PATCH] .

---
 glossary.tex |  8 +++++++
 notation.tex |  4 +++-
 note.tex     | 68 +++++++++++++++++++++++++++++++++++++++++++++-------
 3 files changed, 70 insertions(+), 10 deletions(-)

diff --git a/glossary.tex b/glossary.tex
index 5641d24..b04a844 100644
--- a/glossary.tex
+++ b/glossary.tex
@@ -6,8 +6,16 @@
 \newcommand{\Image}{\definitionLink{image}{monotone}}
 \let\imageNoLink\image
 \renewcommand{\image}[1]{\imageNoLink{#1}}
+\let\lubNoLink\lub
+\renewcommand{\lub}{\definitionLink{lubglb}{\lubNoLink}}
+\let\glbNoLink\glb
+\renewcommand{\glb}{\definitionLink{lubglb}{\glbNoLink}}
 \newcommand{\CompleteLattice}{\definitionLink{completelattice}{complete lattice}}
 
+\let\topNoLink\top
+\renewcommand{\top}{\definitionLink{topbot}{\topNoLink}}
+\let\botNoLink\bot
+\renewcommand{\bot}{\definitionLink{topbot}{\botNoLink}}
 
 \let\fixpointsOfNoLink\fixpointsOf{}
 \renewcommand{\fixpointsOf}{\definitionLink{fixpointsOf}{\fixpointsOfNoLink}}
diff --git a/notation.tex b/notation.tex
index 9ad9192..9b82aef 100644
--- a/notation.tex
+++ b/notation.tex
@@ -3,4 +3,6 @@
 \newcommand{\lte}{\preceq}
 \newcommand{\image}[1]{[#1]}
 \newcommand{\define}{\coloneqq}
-\newcommand{\union}{\cup}
\ No newline at end of file
+\newcommand{\union}{\cup}
+\newcommand{\glb}{\bigwedge}
+\newcommand{\lub}{\bigvee}
diff --git a/note.tex b/note.tex
index 6bc17db..d7e492b 100644
--- a/note.tex
+++ b/note.tex
@@ -15,6 +15,9 @@
 \pagestyle{plain}
 
 \newtheorem{theorem}{Theorem}
+\newtheorem{corollary}{Corollary}
+\newtheorem{lemma}{Lemma}
+\newtheorem{proposition}{Proposition}
 
 \begin{document}
 
@@ -22,6 +25,8 @@
 
 \definition{monotone}{define monotone}
 \definition{image}{define set image}
+\definition{lubglb}{define glb and lub}
+\definition{topbot}{define $\top$ and $\bot$}
 \definition{completelattice}{define complete lattice}
 
 Hello world\cite{tarskilatticetheoretical1955}
@@ -30,31 +35,76 @@ First, we generalize Knaster-Tarski Fixpoint Theorem.
 $$\fixpointsOf(S)$$
 
 
-\begin{theorem}[Tarski-Knaster Fixpoint Theorem~\cite{tarskilatticetheoretical1955}]
+\begin{theorem}[Tarski-Knaster Fixpoint Theorem~\cite{tarskilatticetheoretical1955}]\label{tarskitheorem}
     For a \Monotone function $o$ over a \CompleteLattice $\langle \L, \lte \rangle$, we have that $\langle \fixpointsOf(o), \lte \rangle$ is a \CompleteLattice.
 \end{theorem}
 
 \begin{theorem}
+    Trivial attempt using set preimage / image to attain LUB / GLB in image lattice does not work.
+
+    Consider antichain of 2 that map to a chain in image.
+    The antichain's LUB does maps to a third, distinct element which extends the chain to three in the image
+
+    If we attain LUB of preimage, then its not the least element :)
+\end{theorem}
+
+\begin{theorem}\label{imagelattice}
     For a \Monotone function $o$ over a \CompleteLattice $\langle \L, \lte \rangle$, we have that $\langle o\imageNoLink{\L}, \lte \rangle$ is a \CompleteLattice.
 \end{theorem}
 \begin{proof}
-    Consider $\langle \L', \lte' \rangle$ where
+    Consider $\langle \L', \lte \rangle$ where
     \begin{align*}
         \L' \define \{ x' ~|~ x \in \L \} \\
-        x' \lte' y' \iff x \lte y \textrm{ where } x, y \in \L
+        x' \lte y' \iff x \lte y \textrm{ where } x, y \in \L
     \end{align*}
     Clearly, $\langle \L', \lte' \rangle$ is a \CompleteLattice.
-    Combining $\L$ and $\L'$
+    Combining $\L$ and $\L'$, we formulate $\L^*$:
     \begin{align*}
-        \L^* \define \{ \top^*, \bot^* \} \union \L \union \L' \\
-        \forall x^*, y^* \in \L^*, x^* \lte y^* \iff \begin{cases}
-            (x^* = \bot^*) \lor (y^* = \top^*) \\
-            two \\ 
-            three
+        \L^* &\define \{ \top^*, \bot^* \} \union \L \union \L' \\
+        \forall x^*, y^* \in \L^*, x^* \lte y^* &\iff \begin{cases}
+            (x^* = \bot^*) \lor (y^* = \top^*), \\
+            \textrm{or } x, y \in \L, \\ 
+            \textrm{or } x', y' \in \L'
         \end{cases}
     \end{align*}
+    It is easy to show that $\langle \L^*, \lte \rangle$ is a \CompleteLattice.
+    Consider the operator $o^*$ that maps elements from $\L$ to $\L'$ and every element in $\L'$ to itself.
+    \begin{align*}
+        o^*(x) \define \begin{cases}
+            o(x)' & \textrm{if } x \in \L \\
+            x & \textrm{otherwise}
+        \end{cases}
+    \end{align*}
+    We have $o^*\image{\L \union \L'} \subseteq L'$ and $\fixpointsOf(o^*) = o\image{\L}' \union \{ \bot^*, \top^* \}$.
+    By Tarski-Knaster Fixpoint Theorem (Theorem \ref{tarskitheorem}), $\fixpointsOf(o^*)$ is a \CompleteLattice.
+    Thus, $o\image{\L} \union \{ \bot^*, \top^* \}$ is a \CompleteLattice. For any $S \subseteq \L$, we have $\glb S \not\in \{ \bot^*, \top^* \}$ and $\lub S \not\in \{ \bot^*, \top^* \}$, thus $\langle o\image{\L}, \preceq \rangle$ is a \CompleteLattice.
 \end{proof}
 
+The following follows directly from the contrapositive of Theorem \ref{imagelattice}.
+\begin{corollary}
+    If $\langle o\image{\L}, \lte \rangle$ is not a \CompleteLattice, then $o$ is not \Monotone.
+\end{corollary}
+
+
+\begin{definition}
+    An approximator set $H$ captures a nondeterministic approximator $o$ if for each consistent pair $(x, y)$
+    \begin{align*}
+        (H\image{(x, y)}_1, H\image{(x, y)}_2) = o(x, y)
+    \end{align*}
+\end{definition}
+
+\begin{theorem}
+    A nondeterministic approximator $o$ has a set of 
+\end{theorem}
+
+\begin{theorem}
+    For any nondeterministic approximator $o$, there exists an approximator set $H$ s.t.\ gamma stable models correspond to n-stable models
+\end{theorem}
+\begin{proof}
+    foo
+\end{proof}
+
+
 \bibliographystyle{plain}
 \bibliography{references}