Теорема о низкой базисе
Теорема о низком базисе — одна из нескольких базисных теорем теории вычислимости , каждая из которых показывает, что для заданного бесконечного поддерева бинарного дерева , можно найти бесконечный путь в дереве с определенными свойствами вычислимости. Теорема о низком базисе, в частности, показывает, что должен существовать путь с низким уровнем базиса ; то есть прыжок по Тьюрингу пути эквивалентен по Тьюрингу проблеме остановки. .
Заявление и доказательство
[ редактировать ]Теорема о низкой базисности утверждает, что каждое непустое класс в (см. арифметическую иерархию ) содержит множество низкой степени (Soare 1987:109). По определению это эквивалентно утверждению, что каждое бесконечное вычислимое поддерево двоичного дерева имеет бесконечный путь низкой степени.
В доказательстве используется метод принуждения с классы (Купер 2004:330). Хайек и Кучера (1989) показали, что низкий базис доказуем в формальной системе арифметики, известной как .
Аргумент принуждения также можно сформулировать явно следующим образом. Для множества X ⊆ω пусть f ( X ) = Σ { i }( X )↓ 2 - я , где { i }( X )↓ означает, что машина Тьюринга i останавливается на X (сумма ведется по всем таким i ). Тогда для каждого непустого (светлого лица) S ⊆2 ой , (единственный) X ∈ S , минимизирующий f ( X ), имеет низкую степень Тьюринга. Это потому, что X удовлетворяет условию { i }( X )↓ ⇔ ∀ Y ∈ S ({ i }( Y )↓ ∨ ∃ j < i ({ j }( Y )↓ ∧ ¬{ j }( X )↓)), поэтому функция i ↦ { i }( X )↓ может быть вычислена из индукцией по i ; обратите внимание, что ∀ Y ∈ S φ( Y ) для любого установить φ. Другими словами, остановка машины на X обусловлена = конечным условием, которое допускает X ′ .
Приложение
[ редактировать ]Одним из применений теоремы о низкой базисности является построение пополнений эффективных теорий так, чтобы пополнения имели низкую степень Тьюринга. Например, теорема о низкой базисности подразумевает существование степеней PA строго ниже .
Ссылки
[ редактировать ]- Цензер, Дуглас (1999). " Классы теории вычислимости» . В Гриффоре, Эдвард Р. (ред.). Справочник по теории вычислимости . Stud. Logic Found. Math. Vol. 140. North-Holland. стр. 37–85 . ISBN 0-444-89882-4 . МР 1720779 . Збл 0939.03047 .
- Купер, С. Барри (2004). Теория вычислимости . Чепмен и Холл/CRC. ISBN 1-58488-237-9 . .
- Гаек, Петр; Кучера, Антонин (1989). «О теории рекурсии в IΣ1». Журнал символической логики . 54 (2): 576–589. дои : 10.2307/2274871 . JSTOR 2274871 . S2CID 118808365 .
- Йокуш, Карл Г. младший; Соаре, Роберт И. (1972). «П(0, 1) Классы и степени теорий» . Труды Американского математического общества . 173 : 33–56. дои : 10.1090/s0002-9947-1972-0316227-0 . ISSN 0002-9947 . JSTOR 1996261 . Збл 0262.02041 . Оригинальная публикация, включая дополнительную поясняющую прозу.
- Нис, Андре (2009). Вычислимость и случайность . Оксфордские руководства по логике. Том. 51. Оксфорд: Издательство Оксфордского университета. ISBN 978-0-19-923076-1 . Збл 1169.03034 . Теорема 1.8.37.
- Соаре, Роберт И. (1987). Рекурсивно перечислимые множества и степени. Исследование вычислимых функций и вычислимо порождённых множеств . Перспективы математической логики. Берлин: Springer-Verlag . ISBN 3-540-15299-7 . Збл 0667.03030 .