Метод элиминации кванторов и его применения
Лектор: Сперанский Станислав Олегович (к.ф.-м.н., с.н.с., Математический институт им. В.А. Стеклова РАН, г. Москва)
Даты:
8 ноября (среда), 16:20-17:55, ауд. 5211 НГУ
10 ноября (пятница), 14:30-16:05, ауд. 5273 НГУ
11 ноября (суббота), 12:40-14:15, ауд. 5211 НГУ
Видео:
Аннотация:
Одним из важнейших методов доказательства алгоритмической разрешимости для элементарных (первопорядковых) теорий является так называемый «метод элиминации кванторов». В частности, с помощью него были получены доказательства разрешимости теорий двух фундаментальных структур:
1) упорядоченной группы целых чисел по сложению [Пресбургер 1929];
2) упорядоченного поля вещественных чисел [Тарский 1951].
Более того, из соответствующих доказательств можно извлечь явные аксиоматизации обеих теорий и вывести интересные результаты об определимости в (1) и (2). Стоит также отметить, что теория (1) эквивалентна теории натуральных чисел со сложением, а к теории (2) сводится элементарная геометрия. Работы Тарского и Пресбургера оказали и продолжают оказывать большое влияние на развитие теоретической информатики. Цель настоящего мини-курса — познакомить слушателей с методом элиминации кванторов и его применениями в изучении элементарных теорий.