Commit 2dfa8d25 authored by Ulrich's avatar Ulrich

work in progrss

parent 3b1b5046
*.vo
*.glob
*.sty
*.aux
*.v.d
*.v~
......@@ -11,6 +11,7 @@
\usepackage{url}
\usepackage{bussproofs}
\usepackage{ulem}
\usepackage{verbatim}
\usepackage[utf8]{inputenc}
\renewcommand{\baselinestretch}{1.12}
......@@ -56,7 +57,7 @@
\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$
\item s(Z) for all substitutions s
\end{itemize}}
\only<2>{Kripke-Semantics for $\KIbox \oplus Z$:
......@@ -92,10 +93,10 @@
%permutations
\begin{prooftree}
\AxiomC{$\KIbox \oplus Z \vdash A, G \Rightarrow A$}
\AxiomC{$\KIbox \oplus Z \vdash G \Rightarrow A$}
\LeftLabel{\scriptsize(Perm)}
\RightLabel{\scriptsize $G'$ is permutation of $G$}
\UnaryInfC{$\KIbox \oplus Z \vdash A, G' \Rightarrow A$}
\UnaryInfC{$\KIbox \oplus Z \vdash G' \Rightarrow A$}
\end{prooftree}
%In
......@@ -110,7 +111,7 @@
\AxiomC{}
\LeftLabel{\scriptsize(Ax)}
\RightLabel{\scriptsize s substitution}
\UnaryInfC{$\KIbox \oplus Z \vdash A, G \Rightarrow s(Z)$}
\UnaryInfC{$\KIbox \oplus Z \vdash G \Rightarrow s(Z)$}
\end{prooftree}
%or elimination
......@@ -135,22 +136,14 @@
\LeftLabel{\scriptsize($\Box_{IE}$)}
\BinaryInfC{$\KIbox \oplus Z \vdash G \Rightarrow \Box B$}
\end{prooftree}
Classical counterpart of an intuitionistic modal logic:\\
$\KClbox \oplus Z := \KIbox \oplus Z \land (\dneg a \rightarrow a)$
\end{frame}
\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}
\vspace{2cm}
Classical counterpart of an intuitionistic modal logic:\\
$\KClbox \oplus Z := \KIbox \oplus (Z \land (\dneg a \rightarrow a))$
\end{frame}
\begin{frame}{Glivienko's translation}
$A^{glv} := \dneg A$
\begin{theorem}
......@@ -209,7 +202,7 @@ $A^{glv} := \dneg A$
Translations:
\begin{itemize}
\item Glivenko: $A^t := \dneg A$
\item Glivenko: $A^{glv} := \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}
......@@ -239,7 +232,7 @@ $A^{glv} := \dneg A$
%adequateness equivalent
\begin{block}{}
For any tanslations $t_1, t_2$ in \textit{The Triangle}:
For any translations $t_1, t_2$ in \textit{The Triangle}:
\begin{itemize}
\item $\KIbox \oplus Z \vdash (A^{t_1} \leftrightarrow A^{t_2})$
\end{itemize}
......@@ -247,10 +240,30 @@ $A^{glv} := \dneg A$
\end{block}
\end{frame}
\begin{frame}{Double Negation Tautologies}
\begin{block}{}
For any translations $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}
Most important:
\begin{itemize}
\item $\KIbox \oplus Z \vdash \dneg (\dneg A \land \dneg B) \leftrightarrow \dneg (A \land B)$
\item $\KIbox \oplus Z \vdash \dneg (\dneg A \lor \dneg B) \leftrightarrow \dneg (A \lor B)$
\item $\KIbox \oplus Z \vdash \dneg (\dneg A \rightarrow \dneg B) \leftrightarrow (\dneg A \rightarrow \dneg B)$
\item \dots
\end{itemize}
\end{frame}
%\begin{frame}
% Motivation der translations (man braucht mehr als dneg) \\
% kol, ggr, kur (triangle) and dneg-closed \\
% def von adequatness (als Ziel) \\
% def von adequateness (als Ziel) \\
% äquivalenz von adeq. (mit Bild?)
%\end{frame}
......@@ -259,6 +272,7 @@ $A^{glv} := \dneg A$
For $t$ in the triangle \\
$(\adequate Z t) \Leftrightarrow \KIbox \oplus Z \vdash Z^t $ \\
\end{theorem}
\pause
\begin{proof}
\begin{itemize}
\item [$\Rightarrow$] Obviously $\KClbox \oplus Z \vdash Z$, by the premise $\KIbox \oplus Z \vdash Z^t$.
......@@ -286,7 +300,6 @@ $A^{glv} := \dneg A$
\begin{frame}{Envelopes}
\begin{definition}
\vspace{.3cm}
{\centering
$ \displaystyle
\begin{aligned}
......@@ -309,7 +322,7 @@ $A^{glv} := \dneg A$
\end{frame}
\begin{frame}{Adequatness conditions}
\begin{frame}{Adequateness conditions}
\begin{theorem}
\begin{itemize}
\item Let B be a post-envelope and C be a pre-envelope then
......@@ -320,16 +333,14 @@ $A^{glv} := \dneg A$
\end{theorem}
\begin{Proof}
follows from the definition of envelopes and the reduction of adequatness.
follows from the reduction of adequateness and the definition of envelopes
\end{Proof}
\end{frame}
\begin{frame}{Glivenko-Translation}
\begin{definition}
\begin{itemize}
\item $A^{glv} = \dneg A$
\item Kuroda-axiom $\; \kuroda A$
\end{itemize}
Kuroda-axiom $\; \kuroda A$
\end{definition}
......@@ -348,24 +359,55 @@ $A^{glv} := \dneg A$
\end{frame}
\begin{frame}
Coq \\
Permutations \\
Taktiken früher einbauen \\
Induktionsprämissen und Ziele werden automatisch generiert \\
...
\begin{frame}[fragile]{Our experience with Coq}
\begin{itemize}
\item help for generating goals and premises during inductions
\item proofs by auto with hint databases
\scriptsize
\begin{verbatim}
Lemma weakening: forall A B G Z, KIbox Z G B -> KIbox Z (A :: G) B.
intros. induction H; eauto 3 with KIboxDB.
Qed.
\end{verbatim}
\pause
\begin{verbatim}
Lemma eq_kol_kur : forall Z f, KIbox Z [] ((kol f) <<->> (kur f)).
unfold kur. intros; induction f; simpl.
- apply eq_split; split; apply imp_id.
- eauto with eq_impDB.
- eauto with eq_andDB.
- eauto with eq_orDB.
- apply eq_dneg. eq_dest IHf. eq_split; apply box_imp; assumption.
- apply tt_dneg.
- apply ff_dneg.
Qed.
\end{verbatim}
\normalsize
\only<3>{
\item a framework for permutations was a big help
\item we should have thought of good tactics earlier\dots}
\end{itemize}
\end{frame}
\begin{frame}
Ausblick (siehe Mail)
\end{frame}
\begin{frame}
Wenn noch Zeit ist: Semantik
\begin{frame}{Future Work}
\begin{itemize}
\item extend the signature of the logic, i.e. add diamond or non-unary operators
\item integrate this code with Tadeusz Ruitenburg development and possibly extend it (or reproof it with ND)
\end{itemize}
\end{frame}
\begin{frame}
Quellen
\begin{frame}{References}
\small
\begin{itemize}
\item Ferreira, Gilda, and Oliva, Paulo. ``On various negative translations.'' arXiv preprint arXiv:1101.5442 (2011).
\item Hara, Masaki ``Intuitionistic Propositional Calculus'' https://github.com/qnighy/IPC-Coq
\item Tadeusz Litak's formalization of W. Ruitenburg JSL 1984 paper ``On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus''
\item Litak, Tadeusz. ``Constructive modalities with provability smack.'' Leo Esakia on Duality in Modal and Intuitionistic Logics. Springer Netherlands, 2014. 187-216.
\item Bellin, Gianluigi, Valeria De Paiva, and Eike Ritter. ``Extended Curry-Howard correspondence for a basic constructive modal logic.'' In Proceedings of Methods for Modalities. 2001.
\item Litak, Tadeusz. ``Double Negation and Modality'' ALCOP 2016.
\end{itemize}
\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