Commit 450bcdcb authored by Miriam Polzer's avatar Miriam Polzer

working on presentation

parent ca47dc2d
\documentclass{beamer}
\sloppy
\usepackage{times}
\usepackage{microtype}
\usepackage[final, babel]{microtype}
\usepackage[T1]{fontenc}
\usepackage{graphicx,xspace}
\usepackage{tikz}
\usepackage{amsmath}
\usepackage{url}
\usepackage{ulem}
\usepackage[utf8]{inputenc}
\renewcommand{\baselinestretch}{.99}
\renewcommand{\baselinestretch}{1.12}
\everymath{\displaystyle}
\usepackage{lmodern}
\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{\kuroda}[1]{\Box \dneg #1 \rightarrow \dneg \Box #1}
\newcommand{\dneg}{{\neg\neg}}
\usetheme{Madrid}
%\usefonttheme{structuresmallcapsserif}
\title[DNegMod]{Double-Negation Translation of Intuitionistic Modal Logics in Coq}
\author{Miriam Polzer \& Ulrich Rabenstein}
......@@ -38,8 +43,8 @@
\begin{frame}{Intuitionistic Modal Logic $\KIbox \oplus Z$}
$\phi ::= \top \ |\ \bot\ |\ n\ |\ \phi_1 \rightarrow \phi_2\ |\ \phi_1 \lor \phi_2\ |\
\phi_1 \land \phi_2\ |\ \Box \phi $ \hfill $n \in Vars$
$\phi ::= \top \ |\ \bot\ |\ a\ |\ \phi_1 \rightarrow \phi_2\ |\ \phi_1 \lor \phi_2\ |\
\phi_1 \land \phi_2\ |\ \Box \phi $ \hfill $a \in Vars$
\vspace{2cm}
......@@ -63,17 +68,69 @@
\end{frame}
\begin{frame}
IM Tautologien (impl, and, or)
\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}
\begin{frame}
Motivation der translations (man braucht mehr als dneg) \\
kol, ggr, kur (triangle) and dneg-closed \\
def von adequatness (als Ziel) \\
äquivalenz von adeq. (mit Bild?)
\begin{frame}{Double Negation Tautologies}
Most important:
\begin{itemize}
\item $\KIbox \vdash \dneg (\dneg A \land \dneg B) \leftrightarrow \dneg (A \land B)$
\item $\KIbox \vdash \dneg (\dneg A \lor \dneg B) \leftrightarrow \dneg (A \lor B)$
\item $\KIbox \vdash \dneg (\dneg A \rightarrow \dneg B) \leftrightarrow (\dneg A \rightarrow \dneg B)$
\item \dots
\end{itemize}
\end{frame}
\begin{frame}{Glivenko'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
\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}
\node (a) {a};
\node (b) [below of = a] {b};
\node (c) [right of = b] {c};
\path
(a) edge [->] (b)
(a) edge [->] (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{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)
\end{description}
\end{block}
TODO triangle picture including glv as well
TODO adequateness equivalent
\end{frame}
%\begin{frame}
% Motivation der translations (man braucht mehr als dneg) \\
% kol, ggr, kur (triangle) and dneg-closed \\
% def von adequatness (als Ziel) \\
% äquivalenz von adeq. (mit Bild?)
%\end{frame}
\begin{frame}{Reductiontheorem}
\begin{theorem}[Reductiontheorem]
For $t$ in the triangle \\
......
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