Вычислимость и логика

Санкт-Петербург, осень 2011

Описание

Курс предназначен для студентов направления Computer Science.

Преподаватели

Список лекций

Вычислимые функции, разрешимые и перечислимые множества

Вычислимые функции, разрешимые множества, определения перечислимого множества. Теорема Поста. Перечислимые множества как проекции разрешимых. Вычислимость функции и перечислимость ее графика. Универсальная функция. Вычислимая функция, которую нельзя доопределить до всюду определенной. Пример перечислимого, но неразрешимого множества.

Теорема Успенского-Райса, теорема о неподвижной точке

m-сведения, другие примеры неразрешимых множеств. Последовательность Шпеккера. Теорема Успенского-Райса. Теорема Клини о неподвижной точке. Программа, печатающая свой текст. Доказательство теоремы Клини для искуcственного языка программирования.

Теорема о неподвижной точке (окончание). Машины Тьюринга

Главные универсальные функции. Вывод теоремы Успенского-Райса из теоремы Клини. Машины Тьюринга. Неразрешимость проблемы равенства слов в полугруппе (выводимости в одностороннем и двустороннем ассоциативном исчислении). Определение примитивно рекурсивных функций.

Примитивно рекурсивные и частично рекурсивные функции

Примитивно рекурсивные функции: примеры. Примитивная рекурсивность вычислимых функций за примитивно рекурсивное время. Частично рекурсивные и вычислимые функции. Теорема о нормальной форме. Функция Аккермана.

Функции Аккермана. Пропозициональные формулы

Оценка примитивно рекурсивных функций функцией Аккермана. Функция Аккермана не является примитивно рекурсивной. Перечислимые множества и системы доказательств. Пропозициональные формулы, КНФ, ДНФ. Метод резолюций для исчисления высказываний. Связь с алгоритмами расщепления.

Предикатные формулы. Арифметика

Предикатные формулы (формулы I-го порядка). Интерпретации. Выразимость в арифметике. Арифметичность графика вычислимой функции.

Арифметическая иерархия

Арифметическая иерархия. Универсальные множества в арифметической иерархии. Строгость арифметической иерархии. Теоремы Тарского и Геделя. Прямое доказательство теоремы Геделя о неполноте.

Невыразимость: автоморфизмы и эллиминация кванторов

Невыразимость: метод автоморфизмов. Элиминация кванторов. Простейшие примеры. Задача о разрезании квадрата на меньшие квадраты.

Элиминация кванторов в теории вещественных чисел

Элиминация кванторов в теории вещественных чисел (алгоритм Тарского).

Полнота исчисления предикатов

Предваренная нормальная форма. Скулемизация. Метод резолюций для исчисления предикатов. Теорема о полноте исчисления предикатов. Множество тавтологий является неразрешимым перечислимым множеством.

Теории и модели

Теории, совместность и непротиворечивость, теорема о компактности. Примеры теорий. Аксиоматизация теорий с помощью элиминации кванторов. Арифметика Пеано. Теории и модели.

Ультрафильтры и теорема о компактности

Гильбертовское исчисление предикатов. Генценское исчисление секвенций.

Колмогоровская сложность

Колмогоровская сложность, ее невычислимость. Нижняя оценка на сложность вычисления палиндрома.