typo \Gamma

saona-raimundo · Nov 28, 2023 · 1a6e6a9 · 1a6e6a9
1 parent 9f0dc60
commit 1a6e6a9
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/class_9.tex b/class_9.tex
@@ -99,8 +99,8 @@ \subsection{Gentzen}
 \begin{split}
 \frac{\Gamma, \phi[x:=t] \vdash \Delta}{\Gamma, \forall x. \phi \vdash \Gamma} &  \forall-elim \\
 \frac{\Gamma \vdash \Delta, \phi[x:=y]}{\Gamma \vdash \Delta, \forall x. \phi} &  \forall-intro \textit{ y is a new (fresh) variable} \\
-\frac{Gamma, \phi[x:=y]}{\Gamma, \exists x. \phi \vdash \Delta} & \exists-elim \\ 
-\frac{Gamma \vdash \Delta, \phi[x:=t]}{\Gamma \vdash \Delta, \exists x. \phi} & \exists-intro
+\frac{\Gamma, \phi[x:=y]}{\Gamma, \exists x. \phi \vdash \Delta} & \exists-elim \\ 
+\frac{\Gamma \vdash \Delta, \phi[x:=t]}{\Gamma \vdash \Delta, \exists x. \phi} & \exists-intro
 \end{split}
 \]
 
@@ -131,4 +131,4 @@ \subsection{Natural Deduction}
 
 \begin{homework}
 	 Use PCP to show satisfiability of FOL is undecidable. 
-\end{homework}
+\end{homework}