Commit 3b1b5046 authored by Miriam's avatar Miriam

presentation draft finished

parent a90c51a8
......@@ -5,6 +5,8 @@
\usepackage[T1]{fontenc}
\usepackage{graphicx,xspace}
\usepackage{tikz}
\usetikzlibrary{arrows,shapes,positioning}
\usetikzlibrary{calc,decorations.markings}
\usepackage{amsmath}
\usepackage{url}
\usepackage{bussproofs}
......@@ -22,7 +24,7 @@
\newcommand{\dneg}{{\neg\neg}}
\usetheme{Madrid}
%\usefonttheme{structuresmallcapsserif}
\usefonttheme{structuresmallcapsserif}
\title[DNegMod]{Double-Negation Translation of Intuitionistic Modal Logics in Coq}
\author{Miriam Polzer \& Ulrich Rabenstein}
......@@ -48,14 +50,34 @@
\vspace{2cm}
Now we need a proof system satisfying exactly:
\only<1>{The intuitionistic modal logic $\KIbox \oplus Z$:
\begin{itemize}
\item All intuitionistic tautologies
\item Closure under substitution and MP
\item Closure under MP and substitution
\item Closure under generalization: If $A$ valid, then $\Box A$ valid.
\item $\Box (A \rightarrow B) \rightarrow (\Box A \rightarrow \Box B)$
\item Axiom $Z$
\end{itemize}
\end{itemize}}
\only<2>{Kripke-Semantics for $\KIbox \oplus Z$:
\begin{itemize}
\item Nonempty set of worlds
\item Two relations: \\
\scalebox{1}{\begin{tikzpicture}
\draw[->]
(current bounding box.south west)
++(0, -2em) -- ++(2em, 0)
node[right] {Intuitionistic relation $R_i$, preorder};
\draw[->, dashed]
(current bounding box.south west)
++(0, -1em) -- ++(2em, 0)
node[right] {Modal relation $R_m$};
\end{tikzpicture}}
\item A \textit{frame condition}, e.g.
$\forall w_1 w_2, (\exists w_3, w_1 R_i w_3 \land w_3 R_m w_2) \Rightarrow
(\exists w_3, w_1 R_m w_3 \land w_3 R_i w_2)$
\end{itemize}}
\end{frame}
......@@ -114,11 +136,6 @@
\BinaryInfC{$\KIbox \oplus Z \vdash G \Rightarrow \Box B$}
\end{prooftree}
TODO explanaition?
\end{frame}
\begin{frame}{Natural Deduction for $\KClbox \oplus Z$}
Classical counterpart of an intuitionistic modal logic:\\
$\KClbox \oplus Z := \KIbox \oplus Z \land (\dneg a \rightarrow a)$
\end{frame}
......@@ -134,44 +151,100 @@
\end{frame}
\begin{frame}{Glivenko's translation}
$A^{glv} := \dneg A$
\begin{frame}{Glivienko's translation}
$A^{glv} := \dneg A$
\begin{theorem}
\it Formula $A$ is a classical tautology if and only if $A^{glv}$ is an intuitionistic tautology.
\end{theorem}
\only<1>{$\KIbox \oplus Z \vdash \dneg A \Leftrightarrow \KClbox \oplus Z \vdash A$ ?} \pause
$\KIbox \oplus Z \vdash A^{glv} \Leftrightarrow \KClbox \oplus Z \vdash A$ ?
\end{frame}
\begin{frame}{Glivenko's translation}
\sout{$\KIbox \oplus Z \vdash A^{glv} \Leftrightarrow \KClbox \oplus Z \vdash A$}
\begin{example}
$\Box (\dneg p \rightarrow p) \in \KClbox$ but $\dneg \Box (\dneg p \rightarrow p) \not \in \KIbox$\\
\begin{tikzpicture}
\vspace{2em}
\begin{tabular}{l|r}
\scalebox{1.6}{\begin{tikzpicture}
\node (a) {a};
\node (b) [below of = a] {b};
\node (c) [right of = b] {c};
\node (c) [right of = b] {c};
\path
(a) edge [->] (b)
(a) edge [->] (c)
(a) edge [dashed, ->] (b)
(a) edge [dashed, ->] (c)
(b) edge [->] (c);
\end{tikzpicture}
TODO:
a->c and a->b are modal. b->c is intuitionistic.
c satisfies p, b does not. then b satisfies $\dneg$ p, but not p
\end{tikzpicture}}
&
\scalebox{1}{\begin{tikzpicture}
\node (1) {$V(p) = \{c\}$};
\draw[->]
(current bounding box.south west)
++(0, -2em) -- ++(2em, 0)
node[right] {Intuitionistic Relation};
\draw[->, dashed]
(current bounding box.south west)
++(0, -1em) -- ++(2em, 0)
node[right] {Modal Relation};
\end{tikzpicture}}
\end{tabular}
%a->c and a->b are modal. b->c is intuitionistic.
%2c satisfies p, b does not. then b satisfies $\dneg$ p, but not p
\end{example}
\end{frame}
\begin{frame}{The translation triangle}
\begin{block}{Translation Properties}
\begin{description}
\item[$\dneg$-characterization]
$\KIbox \vdash \dneg A \leftrightarrow A^t$
\item[adequateness] $\adequate{Z}{t}$ \scriptsize(..for a certain class of axioms)
\item[characterization]
$\KClbox \vdash A \leftrightarrow A^t$
\item[adequateness] $\adequate{Z}{t}$ {\scriptsize(..for a certain class of axioms)}
\end{description}
\end{block}
Translations:
\begin{itemize}
\item Glivenko: $A^t := \dneg A$
\item Kolmogorov: $\dneg$ in front of \textsc{every} subformula
\item Refined Gödel-Gentzen: simplfy Kolmogorov from the \textsc{outside}
\item Kuroda: simplify Kolmogorov from the \textsc{inside}
\end{itemize}
TODO triangle picture including glv as well
TODO adequateness equivalent
\end{frame}
\begin{frame}{The translation triangle}
\center
\scalebox{1}{\begin{tikzpicture}[node distance = 2cm]
\node (ggr) {ggr};
\node (kol) [below right of= ggr] {kol};
\node (kur) [below left of= ggr] {kur};
\node (inv) [below of= ggr] {};
\draw (0,-1) circle (2cm) node[label={[label distance=2cm]\textit{The Triangle}}] (circ) {};
\node (glv) [left = 3cm of circ] {glv};
\path
(ggr) edge [<->, double] (kol)
(kol) edge [<->, double] (kur)
(kur) edge [<->, double] (ggr)
(glv) edge [->, double] ++(1.3cm,0) (circ.west);
\end{tikzpicture}}
%adequateness equivalent
\begin{block}{}
For any tanslations $t_1, t_2$ in \textit{The Triangle}:
\begin{itemize}
\item $\KIbox \oplus Z \vdash (A^{t_1} \leftrightarrow A^{t_2})$
\end{itemize}
$\Rightarrow$ sufficient to show adequateness for one translation
\end{block}
\end{frame}
%\begin{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