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

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

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

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

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

Мы следуем формулировкам Эббингауза и Флума ^[2]

Теорема

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

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

Следствие

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

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

Замечания

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

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

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

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

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

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

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

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

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

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

Теорема

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

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

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

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

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

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

τ := {<, мин , 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 , T _i и 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 : в любой момент времени машина находится ровно в одном состоянии:

${\displaystyle \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 находится в состоянии остановки:

${\displaystyle \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'. Мы представляем это состояние дизъюнкцией θ ₀ и θ ₁ :

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

Где θ ₂ равно:

${\displaystyle 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)))}$

И:

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

Где θ ₃ равно:

${\displaystyle 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 ) является моделью φ _M , которая конечна, поскольку множество всех конфигураций останавливающихся вычислений конечно. Отсюда следует, что M останавливается на пустом входе тогда и только тогда, когда φ _M имеет конечную модель. Поскольку остановка на пустом входе неразрешима, то и вопрос о том, имеет ли φ _M конечную модель (эквивалентно, является ли φ _M конечно выполнимым), также неразрешим (рекурсивно перечислимым, но не рекурсивным). Это завершает доказательство. ${\displaystyle {\mathcal {A}}}$

Следствие

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

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

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

Следствие

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

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

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

Ссылки

1. Трахтенброт, Борис (1950). «Невозможность алгоритма для проблемы разрешимости на конечных классах». Известия Академии наук СССР . 70 (4): 569–572.
2. Эббингауз, Хайнц-Дитер ; Флум, Йорг (1995). Теория конечных моделей . Springer Science + Business Media. ISBN 978-3-540-60149-4.
3. Либкин, Леонид (2010). Элементы теории конечных моделей . Тексты по теоретической информатике . ISBN 978-3-642-05948-3.

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