From 1a6e6a99ab6c6f90dc4f2f31449bdf529a7dd365 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= Date: Tue, 28 Nov 2023 21:01:12 +0100 Subject: [PATCH] typo \Gamma --- class_9.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/class_9.tex b/class_9.tex index c96e732..40f3219 100644 --- 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} \ No newline at end of file +\end{homework}