Доказательство неразрешимости проблемы остановки
Введение
формальный неразрешимость логика остановка
Философы сформулировали наиболее важные идеи искусственного интеллекта, но для преобразования его в формальную науку потребовалось достичь определенного уровня математической формализации в трех фундаментальных областях: логика, вычисления и вероятность.
Истоки идей формальной логики можно найти в работах философов древней Греции, но ее становление как математической дисциплины фактически началась с трудов Джорджа Буля (1815–1864), который детально разработал логику высказываний, или булеву логику. В 1879 году Готтлоб Фреге (1848–1925) расширил булеву логику для включения в нее объектов и отношений, создав логику первого порядка, которая в настоящее время используется как наиболее фундаментальная система представления знаний.
Одним из принципиально важных результатов математической логики является доказательство неразрешимости в логике первого порядка распознавания проблем как общезначимости, так и выполнимости ее предложений.
Цель исследования – изучить доказательства неразрешимости логики первого порядка. Для достижения данной цели необходимо выделить ряд задач:
1. Изучить основные понятия логики первого порядка.
2. Рассмотреть понятие машины Тьюринга и доказать неразрешимость проблемы остановки.
3. Вывести неразрешимость логики первого порядка из неразрешимости проблемы остановки.
4. Разобрать доказательство неразрешимости логики первого порядка методом Геделя.
1. Понятие формальной системы
Формальная система (или формальная теория) – результат строгой формализации теории, предполагающей полную абстракцию от смысла слов используемого языка, причем все условия, регулирующие употребление этих слов в теории, явно высказаны посредством аксиом и правил, позволяющих вывести одну фразу из других.
Формальная теория считается определенной, если:
- задано конечное или счётное множество произвольных символов (конечные последовательности символов называются выражениями теории);
- имеется подмножество выражений, называемых формулами;
- выделено подмножество формул, называемых аксиомами;
- имеется конечное множество отношений между формулами, называемых правилами вывода.
Обычно имеется эффективная процедура, позволяющая по данному выражению определить, является ли оно формулой. Часто множество формул задаётся индуктивным определением. Как правило, это множество бесконечно. Множество символов и множество формул в совокупности определяют язык или сигнатуру формальной теории.
Чаще всего имеется возможность эффективно выяснять, является ли данная формула аксиомой; в таком случае теория называется эффективно аксиоматизированной или аксиоматической. Множество аксиом может быть конечным или бесконечным. Если множество аксиом бесконечно, то, как правило, оно задаётся с помощью конечного числа схем аксиом и правил порождения конкретных аксиом из схемы аксиом. Обычно аксиомы делятся на два вида: логические аксиомы (общие для целого класса формальных теорий) и нелогические или собственные аксиомы (определяющие специфику и содержание конкретной теории).
Для каждого правила вывода R и для каждой формулы A эффективно решается вопрос о том, находится ли выбранный набор формул в отношенни R с формулой A, и если да, то A называется непосредственным следствием данных формул по правилу R.
Выводом называется всякая последовательность формул такая, что всякая формула последовательности есть либо аксиома, либо непосредственное следствие каких-либо предыдущих формул по одному из правил вывода.
Формула называется теоремой, если существует вывод, в котором эта формула является последней.
Теория, для которой существует эффективный алгоритм, позволяющий узнавать по данной формуле, существует ли ее вывод, называется разрешимой; в противном случае теория называется неразрешимой.
Теория, в которой не все формулы являются теоремами, называется абсолютно непротиворечивой.
Дедуктивная теория считается заданной, если:
– задан алфавит (множество) и правила образования выражений (слов) в этом алфавите;
– заданы правила образования формул (правильно построенных, корректных выражений);
– из множества формул некоторым способом выделено подмножество T теорем (доказуемых формул).
Свойства дедуктивных теорий:
1. Противоречивость. Теория, в которой множество теорем покрывает всё множество формул (все формулы являются теоремами, «истинными высказываниями»), называется противоречивой. В противном случае теория называется непротиворечивой. Выяснение противоречивости теории – одна из важнейших и иногда сложнейших задач формальной логики. После выяснения противоречивости теория, как правило, не имеет дальнейшего ни теоретического, ни практического применения.
2. Полнота. Теория называется полной, если в ней для любой формулы F выводима либо сама F, либо ее отрицание. В противном случае, теория содержит недоказуемые утверждения (утверждения, которые нельзя ни доказать, ни опровергнуть средствами самой теории), и называется неполной.
3. Независимость аксиом. Отдельная аксиома теории считается независимой, если эту аксиому нельзя вывести из остальных аксиом. Зависимая аксиома по сути избыточна, и ее удаление из системы аксиом никак не отразится на теории. Вся система аксиом теории называется независимой, если каждая аксиома в ней независима.
4. Разрешимость. Теория называется разрешимой, если в ней понятие теоремы эффективно, то есть существует эффективный процесс (алгоритм), позволяющий для любой формулы за конечное число шагов определить, является она теоремой или нет.
Основные понятия логики первого порядка
Логика первого порядка (исчисление предикатов) – формальное исчисление, то есть это совокупность абстрактных объектов, не связанных с внешним миром, в котором представлены правила оперирования множеством символов в строго синтаксической трактовке без учета смыслового содержания.
Язык логики первого порядка строится на основе сигнатуры, состоящей из следующих символов:
1) логические
– символы логических операций , 
, 
, ↔, →;
– символы кванторных операций ", $;
– служебные символы: скобки и запятая.
2) нелогические
– множество предикатных символов, с которым связана арность, то есть число возможных аргументов P(n), Q(m), …, P1(n), P2(n);
– символы пропозициональных переменных X, Y, Z, …, X1, X2, … (можно считать, что символы пропозициональных переменных – это нульместные предикатные символы);
– символы предметных переменных x, y, z, …, x1, x2,…;
– символы предметных констант a, b, c, …, a1, a2, …
n-местным предикатом P (x1, x2,…, xn) называется функция P: M1ЧM2Ч…ЧMn → {1,0}, определенная на наборах длины n элементов некоторого множества M= M1ЧM2Ч…ЧMn и принимающая значения в области {1,0}. Множество М называется предметной областью предиката, его элементы – предметными константами.
Отрицанием предиката P(x1, x2,…, xn), определенного на множестве M1ЧM2Ч…ЧMn называется предикат P(x1, x2,…, xn), определенный на том же множестве, который на наборе (a1, a2,…, an) 
M1ЧM2Ч…ЧMn
Конъюнкцией предикатов P(x1, x2,…, xn), определенного на множестве M1ЧM2Ч…ЧMn, и Q(y1, y2,…, ym), определенного на множестве N1ЧN2Ч…ЧNm, называется предикат P Q(x1, x2,…, xn, y1, y2,…, ym) c пердметной областью M1ЧM2Ч…ЧMnЧN1ЧN2Ч…ЧNn, который на наборе (a1, a2,…, an, b1, b2,…, bm) M1ЧM2Ч…ЧMnЧN1ЧN2Ч…ЧNn
Дизъюнкцией предикатов P(x1, x2,…, xn), определенного на множестве M1ЧM2Ч…ЧMn, и Q(y1, y2,…, ym), определенного на множестве N1ЧN2Ч…ЧNm, называется предикат P Q(x1, x2,…, xn, y1, y2,…, yn) c пердметной областью M1ЧM2Ч…ЧMnЧN1ЧN2Ч…ЧNn, который на наборе (a1, a2,…, an, b1, b2,…, bm) M1ЧM2Ч…ЧMnЧN1ЧN2Ч…ЧNn
Импликацией предикатов P(x1, x2,…, xn), определенного на множестве M1ЧM2Ч…ЧMn, и Q(y1, y2,…, ym), определенного на множестве N1ЧN2Ч…ЧNm, называется предикат P → Q(x1, x2,…, xn, y1, y2,…, yn) c пердметной областью M1ЧM2Ч…ЧMnЧN1ЧN2Ч…ЧNn, который на наборе (a1, a2,…, an, b1, b2,…, bm) M1ЧM2Ч…ЧMnЧN1ЧN2Ч…ЧNn
Эквивалентностью предикатов P(x1, x2,…, xn), определенного на множестве M1ЧM2Ч…ЧMn, и Q(y1, y2,…, ym), определенного на множестве N1ЧN2Ч…ЧNm, называется предикат P(x1, x2,…, xn) ↔ Q (y1, y2,…, yn) c пердметной областью M1ЧM2Ч…ЧMnЧN1ЧN2Ч…ЧNn, который на наборе (a1, a2,…, an, b1, b2,…, bm) M1ЧM2Ч…ЧMnЧN1ЧN2Ч…ЧNn
Операцией связывания квантором общности переменной xi в n-местном предикате P(x1, x2,…, xn)), определенном на множестве M1ЧM2Ч…ЧMn, называется операция, в результате которой получается n-1-местный предикат " xi P(x1, x2,…, xi-1, xi+1,…, xn), который при значениях x1 = a1, …, xi-1 = ai-1, xi-1 = ai-1, …, xn = an истинен, если при любых значениях xi = ai высказывание P(a1, a2,…, an) истинно.
Операцией связывания квантором существования переменной xi в n-местном предикате P(x1, x2,…, xn) называется операция, в результате которой получается n-1-местный предикат $ xi P(x1, x2,…, xi-1, xi+1,…, xn), который при значениях x1 = a1, …, xi-1 = ai-1, xi-1 = ai-1, …, xn = an истинен, если при некотором значении xi = ai высказывание P(a1, a2,…, an) истинно.
Вхождение какой-либо переменной в формулу, называется свободным, если оно не входит в область действия никакого квантора по этой переменной.
Формулами логики предикатов являются:
– всякая нульместная предикатная переменная;
– P(n) (x1, x2,…, xn), где P(n) – n-местная предикатная переменная, а x1, x2,…, xn – свободные переменные;
– 
F, где F – формула;
– F1 F2, F1 F2, F1 ↔ F2, F1 → F2, где F1 и F2 – формулы, в которых общие переменные являются одновременно свободными или одновременно связанными;
– " xi P(x1, x2,…, xi-1, xi+1,…, xn) и $ xi P(x1, x2,…, xi-1, xi+1,…, xn), где P(x1, x2,…, xn) – формула, в которой xi – свободная переменная
Определение истинности формул алгебры предикатов вводится с помощью интерпретации. В классическом случае интерпретация определяется следующими данными
1) предметная область;
2) всякой предметной константе ставится в соответствие некоторый предмет, определенный в области;
3) каждому пропозициональному символу ставится в соответствие некоторое значение 1 (истина) или 0 (ложь);
4) каждому предикатному символу языка ставится в соответствие некоторая характеристическая функция.
Классификация формул:
Формула называется
а) выполнимой (опровержимой) на множестве М, если существует ее истинная (ложная) интерпретация на этом множестве;
б) тождественно-истинной (тождественно-ложной) на множестве М, если любая ее интерпретации на этом на этом множестве истина (ложна);
в) выполнимой (опровержимой), если существует предметная область, на которой она выполнима (опровержима);
г) общезначимой (противоречием), если на любой предметной области она тождественно-истинная (тождественно-ложная).
Множеством истинности предиката P(x1, x2,…, xn), заданного на множестве M1ЧM2Ч…ЧMn, называется совокупность всех упорядоченных систем (a1, a2,… an), в которых a1 е M1 a2 е M2,…, an е Mn, таких, что данный предикат обращается в истинное высказывание Р(a1, a2,… an) при подстановке x1 = a1 x2 = a2,…, xn = an. Обозначается P+.
Два n-местных предиката Р(x1, x2,…, xn) и Q(x1, x2,…, xn), заданных на одном и том же множестве M1ЧM2Ч…ЧMn называются равносильными, если набор предметов a1 е M1 a2 е M2,…, an е Mn превращает первый предикат в истинное высказывание Р(a1, a2,… an) тогда же, когда этот набор предметов превращает второй предикат в истинное. Переход от предиката Р(x1, x2,…, xn) к равносильному ему предикату Q(x1, x2,…, xn) называется равносильным преобразованием первого.
Предикат Р(x1, x2,…, xn), заданный на множестве M1ЧM2Ч…ЧMn называется следствием предиката Q(x1, x2,…, xn), если он превращается в истинное высказывание на всех тех наборах значений предметных переменных из соответствующих множеств, на которых в истинное высказывание превращается предикат Q(x1, x2,…, xn).
Понятие машины Тьюринга
Машина Тьюринга есть математическая (воображаемая) машина, а не машина физическая. Она есть такой же математический объект, как функция, производная, интеграл, группа и т.д. И так же как и другие математические понятия, понятие машины Тьюринга отражает объективную реальность, моделирует некие реальные процессы.
Машины Тьюринга – это совокупность следующих объектов
1) внешний алфавит A={a0, a1, …, an};
2) внутренний алфавит Q={q1, q2,…, qm} – множество состояний;
3) множество управляющих символов {П, Л, С}
4) бесконечная в обе стороны лента, разделённая на ячейки, в каждую из которых в любой дискретный момент времени может быть записан только один символ из алфавита А;
5) управляющее устройство, способное находиться в одном из множества состояний
Символом пустой ячейки является буква внешнего алфавита а0.
Среди состояний выделяются два – начальное q1, находясь в котором машина начинает работать, и заключительное (или состояние остановки) q0, попав в которое машина останавливается.
Управляющее устройство может перемещаться влево и вправо по ленте, читать и записывать в ячейки ленты символы алфавита A. Управляющее устройство работает согласно командам, которые имеют следующий вид
qi aj → apX qk
Запись означает следующее: если управляющее устройство находится в состоянии qi, а в обозреваемой ячейке записана буква aj, то (1) в ячейку вместо aj записывается ap, (2) машина переходит к обозрению следующей правой ячейки от той, которая обозревалась только что, если Х= П, или к обозрению следующей левой ячейки, если Х= Л, или же продолжает обозревать ту же ячейку ленты, если Х= С, (3) управляющее устройство переходит в состояние qk.
Поскольку работа машины, по условию, полностью определяется ее состоянием q, в данный момент и содержимым а обозреваемой в этот момент ячейки, то для каждой возможной конфигурации qi aj имеется ровно одно правило. Правил нет только для заключительного состояния, попав в которое машина останавливается. Поэтому программа машины Тьюринга с внешним алфавитом A={a0, a1, …, an} и внутренним Q={q1, q2,…, qm} содержит не более m (n+ 1) команд.
Словом в алфавите А или в алфавите Q, или в алфавите A 
Q называется любая последовательность букв соответствующего алфавита. Под k-ой конфигурацией будем понимать изображение ленты машины с информацией, сложившейся на ней к началу k-того шага (или слово в алфавите А, записанное на ленту к началу k-того шага), с указанием того, какая ячейка обозревается в этот шаг и в каком состоянии находится машина. Имеют смысл лишь конечные конфигурации, т.е. такие, в которых все ячейки ленты, за исключением, быть может, конечного числа, пусты. Конфигурация называется заключительной, если состояние, в котором при этом находится машина, заключительное.
Если выбрать какую-либо незаключительную конфигурацию машины Тьюринга в качестве исходной, то работа машины будет состоять в том, чтобы последовательно (шаг за шагом) преобразовывать исходную конфигурацию в соответствии с программой машины до тех пор, пока не будет достигнута заключительная конфигурация. После этого работа машины Тьюринга считается закончившейся, а результатом работы считается достигнутая заключительная конфигурация.
Будем говорить, что непустое слово б в алфавите А\ {а0} = {a1, …, an} воспринимается машиной в стандартном положении, если оно записано в последовательных ячейках ленты, все другие ячейки пусты, и машина обозревает крайнюю слева или крайнюю справа ячейку из тех, в которых записано слово б. Стандартное положение называется начальным (заключительным), если машина, воспринимающая слово в стандартном положении, находится в начальном состоянии q1 (соответственно в состоянии остановки q0).
Если обработка слова б переводит машину Тьюринга в заключительное состояние, то говорят, что она применима к б, в противном случае – не применима к б (машина работает бесконечно)
Рассмотрим пример:
Дана машина Тьюринга с внешним алфавитом А = {0, 1} (здесь 0 – символ пустой ячейки), алфавитом внутренних состояний Q = {q0, q1, q2} и со следующей функциональной схемой (программой):
q1 0 → 1 Л q2;
q1 1 → 0 С q2;
q2 0 → 0 П q0;
q2 1 → 1 С q1;
Данную программу можно записать с помощью таблицы
| q1 | 1 Л q2 | 0 С q2 |
| q2 | 0 П q0 | 1 С q1 |
Посмотрим, в какое слово переработает эта машина слово 110, исходя из начального положения:
q1
| … | … |
На первом шаге действует команда: q1 0 → 1 Л q2 (управляющее устройство находится в состоянии q1, а в обозреваемой ячейке записана буква 0, в ячейку вместо 0 записывается 1, головка сдвигается влево, управляющее устройство переходит в состояние q2), в результате на машине создается следующая конфигурация:
q2
| … | … |
На втором шаге действует команда: q2 1 → 1С q1 и на машине создается конфигурация:
q1
| … | … |
Третий шаг обусловлен командой: q1 1 → 0 С q2. В результате нее создается конфигурация:
q2
| … | … |
Наконец, после выполнения команды q2 0 → 0 П q0 создается конфигурация
q0
| … | … |
Эта конфигурация является заключительной, потому что машина оказалась в состоянии остановки q0.
Таким образом, исходное слово 110 переработано машиной в слово 101.
Полученную последовательность конфигураций можно записать более коротким способом (содержимое обозреваемой ячейки записано справа от состояния, в котором находится в данный момент машина):
11q10 => 1 q211 => 1q111 => 1q201 => 10q01
Машина Тьюринга – не что иное, как некоторое правило (алгоритм) для преобразования слов алфавита A Q, т.е. конфигураций. Таким образом, для определения машины Тьюринга нужно задать ее внешний и внутренний алфавиты, программу и указать, какие из символов обозначают пустую ячейку и заключительное состояние.
Доказательство неразрешимости проблемы остановки
Проблема остановки машины Тьюринга – это проблема построения такого алгоритма, который мог бы определить закончится или нет вычисление по некоторой задаче. Оказывается, что в общем случае такой алгоритм нельзя построить в принципе, то есть невозможно найти алгоритм, позволяющий по произвольной машине Тьюринга Т и произвольной ее начальной конфигурации qiaj определить придет ли машина Т в заключительное состояние q0, если начнет работу в этой конфигурации.
Если машина Т, запущенная в начальной конфигурации qiaj, останавливается (т.е. попадает в заключительное состояние) через конечное число шагов, то она называется самоприменимой, в противном случае – несамоприменимой.
Теорема.
Не существует машины Тьюринга М, решающей проблему самоприменимости, то есть проблема самоприменимости алгоритмически неразрешима.
Доказательство.
Предположим противное, то есть. пусть существует машина Тьюринга Т, решающая проблему самоприместимости в указанном выше смысле. Построим новую машину Т0, добавив новое состояние q0* и объявив его заключительным, а также добавив новые команды для состояния q0, которое было заключительным в Т:
q0 a1→ a1С q0 (1)
q0 a2→ a2 С q0 (2)
…q0 an→ an С q0* (n)
Рассмотрим теперь работу машины T0.
Пусть M – произвольная машина. Если M – самоприменима, то начальная конфигурация q1ai перейдет с помощью команд машины T через конечное число шагов в конфигурацию q0a1, далее применяется команда (1), и машина T0 никогда не остановится. Если M – несамоприменима, то начальная конфигурация q1ai перейдет с помощью команд машины T через конечное число шагов в конфигурацию q0an, далее применяется команда (n), и машина T0 остановится.
Таким образом, машина T0 применима к кодам несамоприменимых машин Т и неприменима к кодам самоприменимых машин Т.
Теперь применим машину T0 к начальной конфигурации q1ai. Сама машина T0 является либо самоприменимой, либо несамоприменимой. Если T0 самоприменима, то по доказанному она никогда не остановится, начав с q1ai, и потому она несамоприменима. Если T0 несамоприменима, то по доказанному, она останавливается через конечное число шагов, начав с q1aj, и потому она самоприменима. Получили противоречие, следовательно проблема самоприменимости алгоритмически неразрешима, что и требовалось доказать.
Проблема остановки алгоритмически неразрешима, т. к. если бы она была разрешимой, то мы получили бы разрешимость проблемы самоприменимости.