colloq2.tex

\documentclass[11pt,a4paper,oneside]{scrartcl}
\usepackage[utf8]{inputenc}
\usepackage[english,russian]{babel}
\usepackage[top=1cm,bottom=1cm,left=1cm,right=1cm]{geometry}

\begin{document}
\pagestyle{empty}

\begin{center}
{\large\scshape\bfseries Программа курса <<Математическая логика>>}\\
{\large\scshape Вопросы ко второму коллоквиуму.}\\
\itshape ИТМО, группы M3232--M3239, осень 2023 г.
\end{center}

%\vspace{0.3cm}

\begin{enumerate}
\item Исчисление предикатов. Общезначимость, следование, выводимость. Теорема о дедукции в исчислении предикатов.
Теорема о корректности исчисления предикатов.
\item Непротиворечивые множества формул. Доказательство существования моделей у непротиворечивых множеств формул 
в бескванторном исчислении предикатов.
Теорема Гёделя о полноте исчисления предикатов. Полнота исчисления предикатов.
\item Машина Тьюринга. Задача об останове, её неразрешимость. Неразрешимость исчисления предикатов.
\item Порядок теории (0, 1, 2). Теории первого порядка. Аксиоматика Пеано. Арифметические операции. Формальная арифметика. 
\item Примитивно-рекурсивные и рекурсивные функции. 
функций вычисления простых чисел. Частичный логарифм.
Выразимость отношений и представимость функций в формальной арифметике. Характеристические функции.
Функция Аккермана. 
\item Бета-функция Гёделя. 
Гёделева нумерация. Рекурсивность представимых в формальной арифметике функций.
\item Непротиворечивость (эквивалентные определения), $\omega$-не\-про\-ти\-во\-ре\-чи\-вость. 
Первая теорема Гёделя о неполноте арифметики.
Формулировка первой теоремы Гёделя о неполноте арифметики в форме Россера. 
Синтаксическая и семантическая неполнота арифметики.
Неполнота расширений формальной арифметики.
Ослабленные варианты: арифметика Пресбургера, система Робинсона.
\item Вторая теорема Гёделя о неполноте арифметики, $Consis$. 
Лемма об автоссылках. Условия Гильберта-Бернайса-Лёба. Неразрешимость формальной арифметики. Теорема Тарского о невыразимости истины.
\item Лямбда-исчисление. Пред-лямбда-термы и лямбда-термы. Альфа-эквивалентность, бета-редукция
и бета-эквивалентность. Теорема Чёрча-Россера. 
Комбинатор неподвижной точки. Комбинаторный базис $SK$.
Истина и ложь. Чёрчевские нумералы. 
Натуральный вывод. Импликативный фрагмент интуиционистского исчисления высказываний.
Просто-типизированное лямбда исчисление. Изоморфизм Карри-Ховарда (высказывание, доказательство, импликация, конъюнкция, дизъюнкция, ложь). 
\end{enumerate}
\end{document}