Теорема Трахтенброта

В логике , теории конечных моделей и вычислимости теории теорема Трахтенброта (принадлежащая Борису Трахтенброту ) утверждает, что проблема применимости в логике первого порядка в классе всех конечных моделей неразрешима . Фактически, класс допустимых предложений над конечными моделями не является рекурсивно перечислимым (хотя он корекурсивно перечислим ).

Из теоремы Трахтенброта следует, что теорема Гёделя о полноте (которая является фундаментальной для логики первого порядка) не выполняется в конечном случае. Также кажется нелогичным, что быть действительным для всех структур «проще», чем только для конечных.

Теорема была впервые опубликована в 1950 году: «Невозможность алгоритма проблемы разрешимости на конечных классах».

Математическая формулировка

Мы следуем формулировкам Эббингауза и Флюма.

Теорема

Выполнимость конечных структур неразрешима в логике первого порядка .

То есть множество {φ | φ — предложение логики первого порядка, которому удовлетворяют все конечные структуры} неразрешимо.

Следствие

Пусть σ — реляционный словарь, по крайней мере, с одним символом бинарного отношения.

Множество σ-предложений , действительных во всех конечных структурах, не является рекурсивно перечислимым .

Примечания

1. Это означает, что теорема Гёделя о полноте неверна в конечном итоге, поскольку полнота подразумевает рекурсивную перечислимость.
2. Отсюда следует, что не существует рекурсивной функции f такой, что: если φ имеет конечную модель, то она имеет модель размера не более f(φ). Другими словами, эффективного аналога теоремы Левенгейма–Скулема в конечном не существует.

Интуитивное доказательство

Это доказательство взято из главы 10, разделы 4, 5 «Математической логики» Х.-Д. Эббингауз.

Как и в наиболее распространенном доказательстве первой теоремы Гёделя о неполноте с использованием неразрешимости проблемы остановки , для каждой машины Тьюринга $M$ есть соответствующее арифметическое предложение $\phi _{M}$, эффективно выводимая из $M$, такой, что оно истинно тогда и только тогда, когда $M$ останавливается на пустой ленте. Интуитивно, $\phi _{M}$ утверждает, что «существует натуральное число, которое является кодом Гёделя для записи вычислений». $M$ на пустой ленте, которая заканчивается остановкой».

Если машина $M$ останавливается за конечные шаги, то полная запись вычислений также конечна, тогда существует конечный начальный сегмент натуральных чисел такой, что арифметическое предложение $\phi _{M}$ верно и на этом начальном отрезке. Интуитивно это происходит потому, что в данном случае доказательство $\phi _{M}$ требует арифметических свойств только конечного числа чисел.

Если машина $M$ не останавливается за конечные шаги, то $\phi _{M}$ ложно в любой конечной модели, поскольку не существует конечной записи вычислений $M$ это заканчивается остановкой.

Таким образом, если $M$ останавливается, $\phi _{M}$ верно в некоторых конечных моделях. Если $M$ не останавливается, $\phi _{M}$ неверно во всех конечных моделях. Так, $M$ не останавливается тогда и только тогда, когда $\neg \phi _{M}$ верно для всех конечных моделей.

Множество машин, которые не останавливаются, не является рекурсивно перечислимым, поэтому множество допустимых предложений над конечными моделями не является рекурсивно перечислимым.

Альтернативное доказательство

В этом разделе мы представляем более строгое доказательство Либкина. Обратите внимание в приведенном выше утверждении, что следствие также влечет за собой теорему, и именно это направление мы здесь доказываем.

Теорема

Для каждого реляционного словаря τ, содержащего хотя бы один символ бинарного отношения, неразрешимо, является ли предложение φ словаря τ конечно выполнимым.

Доказательство

Согласно предыдущей лемме, на самом деле мы можем использовать конечное число символов бинарных отношений. Идея доказательства аналогична доказательству теоремы Феджина, и мы кодируем машины Тьюринга в логике первого порядка. Мы хотим доказать, что для каждой машины Тьюринга M мы строим предложение φ _M словаря τ такое, что φ _M конечно выполнимо тогда и только тогда, когда M останавливается на пустом входе, что эквивалентно проблеме остановки и, следовательно, неразрешимо.

Пусть M= ⟨Q, Σ, δ, q ₀ , Q _a , Q _r ⟩ — детерминированная машина Тьюринга с одной бесконечной лентой.

• Q – множество состояний,
• Σ — входной алфавит,
• Δ – алфавит ленты,
• δ — функция перехода,
• q ₀ – исходное состояние,
• Q _a и Q _r — множества состояний принятия и отклонения.

Поскольку мы имеем дело с проблемой остановки при пустом вводе, мы можем предположить, что wlog, что Δ={0,1} и что 0 представляет собой пробел, а 1 представляет некоторый символ ленты. Мы определяем τ так, чтобы мы могли представлять вычисления:

τ := {<, min , T ₀ (⋅,⋅), T ₁ (⋅,⋅), (H _q (⋅,⋅)) _{(q ∈ Q)} }

Где:

• < — линейный порядок, а min — постоянный символ минимального элемента относительно < (наша конечная область определения будет связана с начальным сегментом натуральных чисел).
• T ₀ и T ₁ являются предикатами ленты. T _i (s,t) указывает, что позиция s в момент времени t содержит i, где i ∈ {0,1}.
• H _q являются головными предикатами. H _q (s,t) указывает, что в момент времени t машина находится в состоянии q, а ее головка находится в положении s.

Предложение φ _M утверждает, что (i) <, min , Ti _и H _q интерпретируются, как указано выше, и (ii) что машина в конечном итоге останавливается. Условие остановки эквивалентно утверждению, что H _q∗ (s, t) выполняется для некоторых s, t и q∗ ∈ Q _a ∪ Q _r , и после этого состояния конфигурация машины не меняется. Конфигурации останавливающейся машины (неостанавливающаяся машина не конечна) можно представить как τ (конечное) предложение (точнее, конечную τ-структуру, удовлетворяющую этому предложению). Предложение φ _M : φ ≡ α ∧ β ∧ γ ∧ η ∧ ζ ∧ θ.

Разбиваем его по компонентам:

• α утверждает, что < — линейный порядок и что min — его минимальный элемент
• γ определяет начальную конфигурацию M: он находится в состоянии q ₀ , головка находится в первой позиции и лента содержит только нули: γ ≡ H _{q 0} ( min , min ) ∧ ∀s T ₀ (s, min )
• η утверждает, что в каждой конфигурации M каждая ячейка ленты содержит ровно один элемент из Δ: ∀s∀t(T ₀ (s, t) ↔ ¬ T ₁ (s, t))
• β налагает основное условие согласованности на предикаты H _q : в любой момент времени машина находится ровно в одном состоянии:

$\forall t\exists !s(\bigvee _{q\in Q}H_{q}(s,t))\land \neg \exists s\exists t(\bigvee _{q,q'\in Q,q\neq q}H_{q}(s,t)\land H_{q'}(s,t))$

• ζ утверждает, что в какой-то момент M находится в состоянии остановки:

$\exists s\exists t\bigvee _{q\in Q_{a}\cup Q_{r}}H_{q}(s,t)$

• θ состоит из комбинации предложений, утверждающих, что T _i и H _q хорошо ведут себя по отношению к переходам M. В качестве примера пусть δ(q,0)=(q',1, left), что означает что если M находится в состоянии q и читает 0, то он записывает 1, перемещает головку на одну позицию влево и переходит в состояние q'. Мы представляем это условие дизъюнкцией θ ₀ и θ ₁ :

$\theta _{0}\equiv \forall s\forall t(s\neq {\underline {min}}\land T_{0}(s,t)\land H_{q}(s,t))\to \theta _{2}$

Где _θ2 :

$T_{1}(s,t+1)\land H_{q'}(s-1,t+1)\land \forall s'(s\neq s'\to (\bigwedge _{i=0,1}T_{i}(s',t+1)\leftrightarrow T_{i}(s',t)))$

И:

$\theta _{1}\equiv \forall s\forall t(s={\underline {min}}\land T_{0}(s,t)\land H_{q}(s,t))\to \theta _{3}$

Где θ ₃ :

$T_{1}(s,t+1)\land H_{q'}(s,t+1)\land \forall s'(s\neq s'\to (\bigwedge _{i=0,1}T_{i}(s',t+1)\leftrightarrow T_{i}(s',t)))$

s-1 и t+1 — определяемые сокращения первого порядка для предшественника и преемника в соответствии с порядком <. Предложение θ ₀ гарантирует, что содержимое ленты в позиции s изменится с 0 на 1, состояние изменится с q на q', остальная часть ленты останется прежней и головка переместится в s-1 (т. е. на одну позицию в сторону слева), предполагая, что s не является первой позицией в ленте. Если да, то все обрабатывается θ ₁ : все то же самое, за исключением того, что голова не движется влево, а остается на месте.

Если φ _M имеет конечную модель, то это такая модель, которая представляет собой вычисление M (которое начинается с пустой ленты (т. е. ленты, содержащей все нули) и заканчивается состоянием остановки). Если M останавливается на пустом входе, то набор всех конфигураций остановочных вычислений M (закодированных с помощью <, T _i и H _q s) является моделью φ _M , которая конечна, поскольку набор все конфигурации остановки вычислений конечны. Отсюда следует, что M останавливается на пустом входе тогда и только тогда, когда φ _M имеет конечную модель. Поскольку остановка на пустом входе неразрешима, то же самое касается и вопроса о том, имеет ли φ _M конечную модель. ${\mathcal {A}}$ (эквивалентно, является ли φ _M конечно выполнимой) также неразрешимо (рекурсивно перечислимое, но не рекурсивное). На этом доказательство завершается.

Следствие

Множество конечно выполнимых предложений рекурсивно перечислимо.

Доказательство

Перечислить все пары $({\mathcal {A}},\phi )$ где ${\mathcal {A}}$ конечно и ${\mathcal {A}}\models \phi$.

Следствие

Для любого словаря, содержащего хотя бы один символ двоичного отношения, множество всех конечно допустимых предложений не является рекурсивно перечислимым.

Доказательство

Согласно предыдущей лемме, множество конечно выполнимых предложений рекурсивно перечислимо. Предположим, что множество всех конечно допустимых предложений рекурсивно перечислимо. Поскольку ¬φ конечно допустимо тогда и только тогда, когда φ не является конечно выполнимым, мы заключаем, что множество предложений, которые не являются конечно выполнимыми, рекурсивно перечислимо. Если и множество A, и его дополнение рекурсивно перечислимы, то A рекурсивно. Отсюда следует, что множество конечно выполнимых предложений рекурсивно, что противоречит теореме Трахтенброта.

Ссылки

• Булос, Берджесс, Джеффри. Вычислимость и логика , Издательство Кембриджского университета, 2002.
• Симпсон, С. «Теоремы Чёрча и Трахтенброта». 2001. [1]