1 parent 0381b42 commit 9f12419Copy full SHA for 9f12419
1 file changed
content/proof-theory/natural-deduction/translation-N2i.tex
@@ -11,7 +11,7 @@
11
\olsection{Translating from \Log{N2} to \Log{G2}}
12
13
\begin{prop}\ollabel{prop:N2-to-G2} If $\Log{N2c}\ (\Log{N2i}) \Proves
14
-\Gamma \Sequent !A$ then $\Log{G2c}\(\Log{N2i}) + \Cut \Proves \Gamma'
+\Gamma \Sequent !A$ then $\Log{G2c}\ (\Log{N2i}) + \Cut \Proves \Gamma'
15
\Sequent \Delta$ where $\Gamma'$ is the multiset of !!{formula}s
16
resulting from $\Gamma$ by removing labels, and $\Delta = \{!A\}$ if
17
$!A$ is not~$\lfalse$, and $\Delta = \emptyset$ if it is.
0 commit comments