partowp
33 lines
959 B
TeX
33 lines
959 B
TeX
\documentclass{paper}
|
|
\pagestyle{empty}
|
|
\begin{document}
|
|
|
|
\setcounter{section}{-1}
|
|
\section{Greetings}
|
|
\section{Agenda}
|
|
\begin{itemize}
|
|
\item Three parts:
|
|
\begin{enumerate}
|
|
\item What I know:
|
|
\begin{itemize}
|
|
\item Impredicativity
|
|
\item in logic: BHK
|
|
\end{itemize}
|
|
\item What has been done:
|
|
\begin{itemize}
|
|
\item An idea to avoid impredicative implication
|
|
\item Construct a logical system with this idea
|
|
\item There are well-behaved algebraic models for this system.
|
|
\end{itemize}
|
|
\item What we're going to do:
|
|
\begin{itemize}
|
|
\item Analiticity and the problem of $cut$
|
|
\item Introduce a new analytic system
|
|
\item what we hope to achive
|
|
\end{itemize}
|
|
\end{enumerate}
|
|
\end{itemize}
|
|
\part{Impredicativity}
|
|
\section{What is impredicativity?}
|
|
\textbullet We know impredicative definitions are
|
|
\end{document} |