Commit 5b9180c4 authored by Ulrich's avatar Ulrich

work in progress

parent b62dbf41
......@@ -3,18 +3,16 @@
\usepackage{times}
\usepackage{microtype}
\usepackage[T1]{fontenc}
\usepackage{graphicx,xspace,relsize}
\usepackage{lipsum}
\usepackage{graphicx,xspace}
\usepackage{tikz}
\usepackage{amsmath}
\usepackage{url}
\usepackage{wrapfig}
\usepackage[utf8]{inputenc}
\renewcommand{\baselinestretch}{.99}
\newcommand{\KIbox}{\text{K}_\Box^{\text{I}}}
\newcommand{\KClbox}{\text{K}_\Box^{\text{Cl}}}
\newcommand{\adequate}[2]{ \forall A, \KClbox \oplus #1 \vdash A \Leftrightarrow \KIbox \oplus #1 \vdash A^{#2}}
\newcommand{\adequate}[2]{\forall A, \KClbox \oplus #1 \vdash A \Leftrightarrow \KIbox \oplus #1 \vdash A^{#2}}
\newcommand{\kuroda}[1]{\Box \dneg #1 \rightarrow \dneg \Box #1}
......@@ -67,36 +65,62 @@
\end{frame}
\begin{frame}
\begin{definition}
A is a pre-envelope iff $\forall Z, \KIbox \oplus Z \vdash \dneg sub_\dneg(A) \rightarrow A^{kol}$ \\
A is a post-envelope iff $\forall Z, \KIbox \oplus Z \vdash A^{kol} \rightarrow \dneg sub_\dneg(A)$ \\
A is a $\dneg$-envelope iff $\forall Z, \KIbox \oplus Z \vdash A^{kol} \leftrightarrow \dneg sub_\dneg(A)$ \\
\end{definition}
%evtl. beispiele von envelopes
\begin{definition}
\vspace{.3cm}
{\centering
$ \displaystyle
\begin{aligned}
& \text{A is a pre-envelope} && \text{iff} &&& \forall Z, \KIbox \oplus Z \vdash \dneg sub_\dneg(A) \rightarrow A^{kol} \\
& \text{A is a post-envelope}&& \text{iff} &&& \forall Z, \KIbox \oplus Z \vdash A^{kol} \rightarrow \dneg sub_\dneg(A) \\
& \text{A is a $\dneg$-envelope} && \text{iff} &&& \forall Z, \KIbox \oplus Z \vdash A^{kol} \leftrightarrow \dneg sub_\dneg(A) \\
& \text{Z is a Kuroda-envelope} && \text{iff} &&& \forall A, \KIbox \oplus Z \vdash A^{kol} \leftrightarrow \dneg sub_\dneg(A)
\end{aligned}
$ \par }
\end{definition}
\begin{example}
\begin{itemize}
\item Box-free formulas are $\dneg$-envelopes.
\item Shallow formulas with no disjunction under box are $\dneg$-envelopes.
\item Implication-free formulas are pre-envelopes.
\item Negations of pre-envelopes are post-envelopes.
\end{itemize}
\end{example}
\begin{theorem}
Let B be a post-envelope and C be a pre-envelope then
$\adequate {(B \rightarrow C)} t$.
\end{theorem}
\begin{Proof}
follows directly from the definition of envelopes
\end{Proof}
\end{frame}
\begin{frame}
\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$.
\end{itemize}
\end{theorem}
\begin{Proof}
follows from the definition of envelopes and the reduction of adequatness.
\end{Proof}
\end{frame}
\begin{frame}
\title{Glivenko-Translation}
\begin{definition}
$A^{glv} = \dneg A$ \\
Kuroda-axiom $\; \kuroda A$
\begin{itemize}
\item $A^{glv} = \dneg A$
\item Kuroda-axiom $\; \kuroda A$
\end{itemize}
\end{definition}
Assuming Kuroda-axiom, $glv$ becomes equivalent to the ones in the triangle.
Assuming Kuroda-axiom, $glv$ becomes equivalent to $kur$,$kol$ and $ggr$.
Therefore:
\begin{theorem}
$\KIbox \oplus Z \vdash \kuroda A \; \Rightarrow $ \\
$\adequate Z {glv}$
$\adequate Z t$
\end{theorem}
\begin{Proof}
Since Kuroda-axiom is a Kuroda-envelope\ldots
\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