Commit 7066bd5c authored by Miriam's avatar Miriam

changed a view formulations

parent cde7218a
......@@ -71,11 +71,10 @@
\only<1>{The intuitionistic modal logic $\ikop Z$:
\begin{itemize}
\item All intuitionistic tautologies
\item All intuitionistic tautologies and axiom Z
\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 s(Z) for all substitutions s
\end{itemize}}
\only<2>{Kripke-Semantics for $\ikop Z$:
......@@ -145,7 +144,7 @@
\end{frame}
\begin{frame}{Natural Deduction for $\ikop Z$}
The only rule for box:
The only rule for box, as proposed by Bellin, De Paiva and Ritter:
%(forall f, In f F -> KIbox Z G (|[]| f)) -> KIbox Z F h -> KIbox Z G (|[]| h)
\begin{prooftree}
......@@ -220,7 +219,7 @@
\item[adequateness] $\adequate{Z}{t}$ {\scriptsize(..for a certain class of axioms)}
\end{description}
\end{block}
\end{block}\pause
Translations:
\begin{itemize}
......@@ -271,7 +270,7 @@
$\Rightarrow$ sufficient to show adequateness for one translation
\end{block}
Most important:
Technical work:
\begin{itemize}
\item $\ikop Z \vdash \dneg (\dneg A \land \dneg B) \leftrightarrow \dneg (A \land B)$
\item $\ikop Z \vdash \dneg (\dneg A \lor \dneg B) \leftrightarrow \dneg (A \lor B)$
......
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