Commit 157bddff authored by litak's avatar litak

some more suggested modifications

parent ba49ddb0
......@@ -126,9 +126,9 @@
%Ax
\begin{prooftree}
\AxiomC{}
\AxiomC{}
\LeftLabel{\scriptsize(Ax)}
\RightLabel{\scriptsize s is a substitution}
\RightLabel{\scriptsize $s$ is a substitution}
\UnaryInfC{$\ikop Z \vdash G \Rightarrow s(Z)$}
\end{prooftree}
......@@ -149,10 +149,11 @@
%(forall f, In f F -> KIbox Z G (|[]| f)) -> KIbox Z F h -> KIbox Z G (|[]| h)
\begin{prooftree}
\AxiomC{$\forall A_i. \ikop Z \vdash G \Rightarrow \Box A_i$}
\AxiomC{$\ikop Z \vdash A_1 \dots A_n \Rightarrow B $}
\AxiomC{\scriptsize $\ikop Z \vdash G \Rightarrow \Box A_1 \quad \dots$}
\AxiomC{\scriptsize $\ikop Z \vdash G \Rightarrow \Box A_n$}
\AxiomC{$\ikop Z \vdash A_1 \dots A_n \Rightarrow B$}
\LeftLabel{\scriptsize($\Box_{IE}$)}
\BinaryInfC{$\ikop Z \vdash G \Rightarrow \Box B$}
\TrinaryInfC{$\ikop Z \vdash G \Rightarrow \Box B$}
\end{prooftree}
\bigskip
......@@ -165,7 +166,6 @@
\end{frame}
\begin{frame}{Glivenko's translation}
$A^{glv} := \dneg A$
\begin{theorem}
......
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