Введение
В логике, теории конечных моделей и теории вычислимости, теорема Трахтенброта (установленная Борисом Трахтенбротом) утверждает, что задача определения справедливости формул логики первого порядка в классе всех конечных моделей неразрешима. Фактически, класс справедливых формул относительно конечных моделей не является рекурсивно перечислимым (хотя он является ко-рекурсивно перечислимым). Теорема Трахтенброта влечет за собой, что теорема о полноте Гёделя (фундаментальная для логики первого порядка) не выполняется в конечном случае. Также представляется контринтуитивным, что справедливость для всех структур оказывается "проще", чем справедливость только для конечных структур. Теорема была впервые опубликована в 1950 году под названием: "О невозможности алгоритма для задачи разрешимости на конечных классах".
Теорема
Удовлетворимость для конечных структур не разрешима в логике первого порядка. То есть, множество {φ | φ – формула логики первого порядка, которая выполняется во всех конечных структурах} является неразрешимым.
Интуитивное доказательство
Это доказательство взято из главы 10, раздела 4, 5 "Математической логики" Х. Д. Эббингауза. Как и в наиболее распространенном доказательстве первой теоремы о неполноте Гёделя, использующем неразрешимость проблемы останова, для каждой машины Тьюринга существует соответствующее арифметическое предложение , эффективно выводимое из , такое, что оно истинно тогда и только тогда, когда машина останавливается на пустой ленте. Интуитивно, утверждает: "существует натуральное число, являющееся кодом Гёделя для записи вычислений машины на пустой ленте, завершающейся остановкой". Если машина останавливается за конечное число шагов, то и полная запись вычислений конечна, а значит, существует конечный начальный отрезок натуральных чисел, на котором арифметическое предложение также истинно. Интуитивно это связано с тем, что для доказательства в этом случае требуются арифметические свойства лишь конечного числа чисел. Если машина не останавливается за конечное число шагов, то ложно в любой конечной модели, поскольку не существует конечной записи вычислений, завершающейся остановкой. Таким образом, если машина останавливается, то истинно в некоторых конечных моделях. Если машина не останавливается, то ложно во всех конечных моделях. Следовательно, машина не останавливается тогда и только тогда, когда истинно во всех конечных моделях. Множество машин, которые не останавливаются, не является рекурсивно перечислимым, поэтому множество истинных предложений в конечных моделях также не является рекурсивно перечислимым.