Меня эта тема дико проперла, когда я ее узнал, и я сильно пожалел, что ничего подобного не было на мехматском курсе логики. Речь идет про теорему Тарского об алгоритмической разрешимости замкнутой арифметической формулы первого порядка с вещественными переменными. Звучит страшно (и, вероятно, я, как человек далекий от логики, напутал значения каких-то слов), но по сути это означает следующее.
Допустим есть формула, содержащая некоторый конечный набор переменных, рациональные числа, знаки арифметических действий, знаки сравнения, логические операции, два основных квантора и технические скобочки. Допустим, формула имеет смысл, а каждая переменная вещественна и связана каким-либо квантором. Теорема Тарского утверждает, что истинность этой формулы можно проверить алгоритмически.
Например, утверждение ∀p∀q [(p*p-4*q≥0) => ∃x (x*x+p*x+q=0)] представляет из себя общеизвестный школьный факт, но его истинность можно было бы проверить алгоритмически согласно Тарскому. Равно как и ложность утверждения ∀p∀q [(p*p-3*q≥0) => ∃x (x*x+p*x+q=0)]
Но это игрушки. А вот, например, крайне неочевидное следствие теоремы Тарского, описанное в книге Грюнбаума про многогранники. Допустим есть конечное множество М. Абстрактной схемой S на этом множестве называется любая совокупность подмножеств множества М. Назовем схему реализуемой, если существует выпуклый многогранник, у которого вершины соответствуют элементам М, а множества вершин всевозможных граней многогранника — элементы схемы S. Так вот: реализуемость схемы многогранником — алгоритмически разрешимая задача, поскольку ее можно записать арифметической формулой первого порядка (некий сокращенный вариант этой формулы на рисунке).
Разумеется, если честно написать каждую переменную в этой формуле, каждый отдельный логический символ и каждый отдельный квантор, получится какая-то длиннючая простыня. В оригинале сложность алгоритма Тарского не ограничена никакой башней экспонент (!) от длины проверяемой формулы. Матиясевич утверждает, что сейчас сложность алгоритма понизили до двойной экспоненты. Но даже и так: очевидно, что алгоритм, проверяющий реализуемость схемы многогранником, будет дико сложным. Важно, что он существует. В частности, можно алгоритмически проверить, является ли симплициальный комплекс границей выпуклого симплициального многогранника.
А вот алгоритмически проверить, является ли симплициальный комплекс триангуляцией сферы уже нельзя по теореме Новикова. Отсюда, в частности, следует, что классы триангулированных сфер и границ выпуклых симплициальных многогранников различаются, а значит существуют невыпуклые триангуляции сферы.
Этот факт, конечно, можно доказать приведением конкретного нехитрого примера в размерности 3 (сфера Барнетта). Но классно, что его можно вывести из алгоритмической науки и двух адовых теорем.
Возвращаясь к началу: жалко, что про теоремы Тарского и Адяна, имхо, фундаментальнейшие результаты о разрешимости и неразрешимости соотв., и про их следствия не рассказывают в обязательных курсах на мехмате (*не рассказывали когда я был студентом, не знаю, как сейчас).
Комментариев нет:
Отправить комментарий