Пятница 31.05. М.Р. Старчак: "О совместности систем выражений вида НОД(a,x+b)=d с приложением к проблемам элиминации кванторов"

Пятница, 31 мая, ПОМИ РАН, ауд. 106. Начало в 17:00.

Докладчик: М.Р. Старчак (Санкт-Петербургский государственный университет).

Тема: О совместности систем выражений вида НОД(a,x+b)=d с приложением к проблемам элиминации кванторов.

Abstract

Разрешимость элементарной теории целых чисел с единицей, сложением, равенством и отношением порядка (назовём её PA) была доказана Мойжешем Пресбургером в 1929 году. Было показано, что если обогатить сигнатуру экзистенциально выразимыми отношениями делимости на константы 2, 3, 4 и т.д., то по всякой формуле можно построить эквивалентную бескванторную. Так как отрицания отношений равенства, порядка и делимостей выразимы бескванторными формулами, то, в действительности, достаточно рассматривать только положительные (не содержащие логической связки отрицания) экзистенциальные фомулы. Помимо доказательства разрешимости, процесс элиминации кванторов позволяет описать выразимые в рассматриваемой структуре множества.

Элементарная теория целых чисел с единицей, сложением, порядком и делимостью (PAD) неразрешима, как было показано Дж. Робинсон в 1949 году. В то же время, в 1976 году независимо А.П. Бельтюковым и Л. Липшицем была доказана разрешимость экзистенциальная теории указанной структуры (назовём эту теорию EPAD). Так как неделимость оказывается экзистенциально выразимой, в данном случае невозможно построить по положительной экзистенциальной формуле эквивалентную бескванторную.

Всякую делимость x на число a можно записать в виде НОД(a,x)=a. В докладе будет дано необходимое и достаточное условие разрешимости систем выражений вида НОД(a,b+x)=d, где a и b — целые числа, причем a не равно 0; d — положительное целое. Этот результат является обобщением китайской теоремы об остатках. Далее будут рассмотрены примеры структур, элементарные теории которых неразрешимы, экзистенциальные разрешимы как подтеории EPAD, но для положительных экзистенциальных формул которых уже можно построить эквивалентные бескванторные с помощью полученного обобщения китайской теоремы.