Commit b62dbf41 authored by Ulrich Rabenstein's avatar Ulrich Rabenstein

added some definitions / theorems

parent f60b52c3
......@@ -12,6 +12,14 @@
\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}
\title[DNegMod]{Double-Negation Translation of Intuitionistic Modal Logics in Coq}
\author{Miriam Polzer \& Ulrich Rabenstein}
......@@ -48,17 +56,48 @@
Ulrich: \\
adequate eq ggr
For $t$ in the triangle: \\
$(\adequate Z t) \Leftrightarrow \KIbox \oplus Z \vdash Z^t $ \\
$\rightarrow$ easy \\
$\leftarrow $ complicated syntactic proof...
envelopes \\
evtl. beispiele \\
theorem 5
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)$ \\
%evtl. beispiele von envelopes
Let B be a post-envelope and C be a pre-envelope then
$\adequate {(B \rightarrow C)} t$.
follows directly from the definition of envelopes
theorem 6
$A^{glv} = \dneg A$ \\
Kuroda-axiom $\; \kuroda A$
Assuming Kuroda-axiom, $glv$ becomes equivalent to the ones in the triangle.
$\KIbox \oplus Z \vdash \kuroda A \; \Rightarrow $ \\
$\adequate Z {glv}$
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