Commit 77cbb5d4 authored by Ulrich Rabenstein's avatar Ulrich Rabenstein

minor

parent 5b9180c4
......@@ -52,19 +52,37 @@
äquivalenz von adeq. (mit Bild?)
\end{frame}
\begin{frame}
Ulrich: \\
\begin{theorem}
For $t$ in the triangle: \\
\begin{frame}{Reductiontheorem}
\begin{theorem}[Reductiontheorem]
For $t$ in the triangle \\
$(\adequate Z t) \Leftrightarrow \KIbox \oplus Z \vdash Z^t $ \\
\end{theorem}
\begin{proof}
$\rightarrow$ easy \\
$\leftarrow $ complicated syntactic proof...
\begin{itemize}
\item [$\Rightarrow$] Obviously $\KClbox \oplus Z \vdash Z$, by the premise $\KIbox \oplus Z \vdash Z^t$.
\item [$\Leftarrow$]
Let $\KIbox \oplus Z \vdash Z^t$.
\begin{itemize}
\item [$\leftarrow$]
Let $\KIbox \oplus Z \vdash A^t$, then
$\KClbox \oplus Z \vdash A^t$ and thus $\KClbox \oplus Z \vdash A$.
\item [$\rightarrow$]
Induction on $\KClbox \oplus Z \vdash A$. \\
On the blackboard...
%Box-case: Premises: \\
% $\forall A \in F, \KIbox \oplus Z \vdash G^t \Rightarrow \dneg \Box A^t$ and \\
% $\KIbox \oplus Z \vdash F^t \Rightarrow h^t$. \\
%From the first one: $\forall A \in F^t, \KIbox \oplus Z \vdash G^t \Rightarrow \dneg \Box A$. \\
%By the premises and a modified box-rule, we get $\KIbox \oplus Z \vdash G^t \Rightarrow \dneg \Box B^t$.
\end{itemize}
\end{itemize}
\end{proof}
\end{frame}
\begin{frame}
\begin{frame}{Envelopes}
\begin{definition}
\vspace{.3cm}
{\centering
......@@ -89,12 +107,12 @@
\end{frame}
\begin{frame}
\begin{frame}{Adequatness conditions}
\begin{theorem}
\begin{itemize}
\item Let B be a post-envelope and C be a pre-envelope then
$\adequate {(B \rightarrow C)} t$.
\item Let A be a $\dneg$-envelope or Z be a Kuroda-envelope, then $\adequate Z t$.
\item Let Z be a $\dneg$-envelope or a Kuroda-envelope, then $\adequate Z t$.
\end{itemize}
......@@ -104,22 +122,26 @@
\end{Proof}
\end{frame}
\begin{frame}
\title{Glivenko-Translation}
\begin{frame}{Glivenko-Translation}
\begin{definition}
\begin{itemize}
\item $A^{glv} = \dneg A$
\item Kuroda-axiom $\; \kuroda A$
\end{itemize}
\end{definition}
Assuming Kuroda-axiom, $glv$ becomes equivalent to $kur$,$kol$ and $ggr$.
\begin{theorem}
$\KIbox \oplus Z \vdash \kuroda A \; \Rightarrow $ \\
$\adequate Z t$
\begin{itemize}
\item [1] Assuming Kuroda-axiom, $glv$ becomes equivalent to $kur$,$kol$ and $ggr$.
\item [2] $\KIbox \oplus Z \vdash \kuroda A \; \Rightarrow $\\$ (\adequate Z t)$
\end{itemize}
\end{theorem}
\begin{Proof}
Since Kuroda-axiom is a Kuroda-envelope\ldots
\begin{itemize}
\item [1] by straightforward induction
\item [2] since Kuroda-axiom is a Kuroda-envelope\ldots
\end{itemize}
\end{Proof}
\end{frame}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment