Start sectoin 3

itp-lesson/main.tex

@@ -724,93 +724,16 @@ ghci> \textcolor{emph2}{let} p \textcolor{emph2}{::} P\textcolor{emph2}{;} p = \
 %%     encode the existential quantification in the universal
 %%     quantification
 
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% REMOVED in favour of BHK interpretation
-%
-%\begin{frame}{Writing proofs}
-%	\begin{tikzpicture}
-%		\node (A) {%
-%				\begin{prooftree}
-%					\infer0[top-i]{\vdash \top}
-%					\infer0[top-i]{\vdash \top}
-%					\infer2[and-i]{\vdash \top \land \top}
-%				\end{prooftree}
-%			};
-%
-%		\pause
-%		\node[right = 2cm of A] (B) {%
-%				\begin{prooftree}
-%					\infer0{\text{top-i}}
-%					\infer0{\text{top-i}}
-%					\infer2{\text{and-i}}
-%				\end{prooftree}
-%			};
-%		\draw[->] (A) -- (B);
-%		\pause
-%		\node[right=2cm of B] (C) {%
-%				\(\text{and-i}(\text{top-i}, \text{top-i})\)
-%			};
-%		\draw[->] (B) -- (C);
-%	\end{tikzpicture}
-%
-%	\vfill
-%
-%	\uncover<4->{%
-%		What about contexts?
-%		\qquad
-%		\begin{tikzpicture}
-%			\node (A) {%
-%					\begin{prooftree}
-%						\infer0[ax]{P, Q \vdash P}
-%						\infer0[ax]{P, Q \vdash Q}
-%						\infer2[and-i]{P, Q \vdash P \land Q}
-%					\end{prooftree}
-%				};
-%			\only<5->{%
-%				\node[right = 2cm of A] (B) { ? };
-%				\draw[->] (A) -- (B);
-%			}
-%		\end{tikzpicture}
-%	}
-%	% Contexts are missing: there's not enough information to build the deduced
-%	% sequent from the proof
-%	% But: with natural deduction, we may use contexts only for the axiom rule
-%\end{frame}
-%
-%\begin{frame}{Writing proofs: contexts}
-%	% In natural deduction, contexts are only used for the axiom rule
-%	% Named hypotheses in global context
-%	\(\alpha : P, \beta : Q\) \hspace{6em}
-%	\onslide<2->{\(\text{and-i}(\alpha, \beta)\)}
-%	\vfill
-%	\onslide<3->
-%	How to extend context?
-%	% What do we need? a notation that introduces an hypothesis, with a notion of
-%	% scope: the hypothesis may be used only in the proof pi below
-%	\vfill
-%	\onslide<4->
-%	\begin{tikzpicture}
-%		\node (A) {%
-%				\begin{prooftree}
-%					\hypo{\pi}
-%					\infer1{A, B \vdash C}
-%					\infer1[imp-i]{A \vdash B \imp C}
-%				\end{prooftree}
-%			};
-%		\node [right = 2cm of A, visible on=<5->] (B) { {\tabst{\beta}[B]\pi} };
-%	\end{tikzpicture}
-%\end{frame}
-%
-%% REMOVED in favour of BHK interpretation
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
 \section{Formalising proof systems}
 
 \begin{frame}
 	\tableofcontents[currentsection]
 \end{frame}
 
+\subsection{Pure type systems}
+
+\subsection{Logical frameworks}
+
 \appendix
 
 \section{Logical systems}