Completed model computation

itp-lesson/main.tex

@@ -136,6 +136,8 @@ overlay-beamer-styles}
 
 \section{Logics and proofs: Manipulating truth}
 
+\subsection{What we're dealing with}
+
 \begin{frame}{How can I be right?}
 	When is a proposition true? \onslide<2->
 	When it admits a \alert{\onslide<3->{correct} proof}.
@@ -217,9 +219,9 @@ overlay-beamer-styles}
 		\quad
 		\(\neg P \lor Q\)
 		\quad
-		\(\forall x, R(x,x)\)
+		\(\tapp*{\forall x, {R(x,x)}}\)
 		\quad
-		\(\forall x, \forall y, R(x,y) \to R(y, x)\)
+		\(\tapp*{\forall x, \forall y, {R(x,y) \imp R(y, x)}}\)
 	\end{exampleblock}
 	\begin{exampleblock}{with group theory}
 		\(x * y = y * x\)\quad
@@ -231,6 +233,8 @@ overlay-beamer-styles}
 
 \end{frame}
 
+\subsection{Deriving truth: syntax and semantics}
+
 \begin{frame}{Example: Propositional calculus}
 	\begin{block}{Propositional calculus}
 		\[ f ::= f \imp f \mid f \land f \mid f \lor f \mid \neg f \mid \top \mid \bot \mid
@@ -262,14 +266,19 @@ overlay-beamer-styles}
 
 	\begin{block}{Value of a formula}
 		\begin{itemize}
-			\item \(\val{\mathcal{M}}{\tapp{f, t_1, \dots, t_n}}{e} =
+			\item \(\val{\mathcal{M}}{\tapp{f, t_1, \dots, t_n}}{\xi} =
 				\tapp{%
 					f_{\mathcal{M}},
-					(\val{\mathcal{M}}{t_1}{e}),
+					(\val{\mathcal{M}}{t_1}{\xi}),
 					\dots,
-					(\val{\mathcal{M}}{t_n}{e})
+					(\val{\mathcal{M}}{t_n}{\xi})
 				}
 				\)
+			\item \(\val{\mathcal{M}}{R(t_1, \dots, t_n)}{\xi}
+				= R_{\mathcal{M}}(\val{\mathcal{M}}{t_1}{\xi},
+				\dots,
+				\val{\mathcal{M}}{t_n}{\xi})
+				\)
 			\item \(\val{\mathcal{M}}{x}{\xi} = \xi(x)\)
 		\end{itemize}
 	\end{block}