По определению ф-ии f(n,x) имеем f(n0,x)ÎKÛn0Ïw. Но в силу леммы имеем f(n0,x)=Ф(a(n0),x). Если бы класс К был разрешимым, то существовал бы алгоритм Ck(m0)={1, если Ф(m0,x)ÎK; 0, если Ф(m0,x)ÏK. Из этого условия и доказанных соотношений вытекает разрешимость мн-ва w. Действительно, n0Ïw, когда f(n0,x)ÎKÛФ(a(n0),x)ÎKÛCk(a(n0))=1. Но это противоречит условию, гласящему, что мн-во w не разрешимо. Значит сделанное предположение о разрешимости класса К ведет к противоречию и значит должно быть отвергнуто. Теорема доказана.
Замечание: Подчеркнем, что эта теорема говорит о невозможности распознавать св-ва вычислимых ф-ий, а не программ их вычисляющих.
Вопрос22.
Дать определение формального исчисления и формального вывода в нем.
Опишем вначале общее понятие формального исчисления. Всякое ФИ характеризуется своими: 1) языком; 2) аксиомами; 3) правилами вывода.
1) Язык исчисления формируется из алфавита и правил образования выражений. Алфавит есть множество символов, конечное или бесконечное. Основные объекты, которыми оперирует ФИ – это его выражения. Выражения – это некоторые слова в алфавите исчисления. Множество выражений обычно определяется индуктивно. Как правило выражения – это легко распознаваемые объекты (иными словами множество выражений явл. обычно разрешимым подмножеством мн-ва всех слов). В некоторых языках рассматриваются выражения различных типов (например, в т.н. исчислении предикатов рассматривают термы и формулы).
2) Аксиомы исчисления – это элементы некоторого подмн-ва выражений. Обычно мн-ва аксиом устроены достаточно просто: оно конечно или по крайней мере разрешимо.
3) Правила вывода явл. ф-иями на мн-ве выражений со значениями в том же мн-ве. Различные правила вывода могут зависеть от различного числа переменных. Отметим также, что произвольное правило вывода не обязательно, как ф-ия всюду определено.
При этом понятие вывода в исчислении также формулируется в общем виде: формальным выводом в ФИ наз. всякую конечную посл-ть выражений этого исчисления Ф1, Ф2,…,Фn – формул, в которой ф-ла Фi – либо аксиома, либо получается из некоторого числа ф-л, предшествующих ей в этой посл-ти, путем применения к ним одного из правил исчисления.
Примеры.
1) Язык: (Алфавит А={а}, выражения = WА)
2) Аксиома: L – пустое слово
3) Правило вывода: wÎ WА, r(w) = awa.
Примеры выводов.
1) L (=Ф1), аа (=Ф2), аааа (=Ф3) Ф2 = r(Ф1); Ф3 = r(Ф2) – формальный вывод.
2) L (=аксиома), аа (=r(Ф1)), L (=аксиома) – формальный вывод
3) L, аа, аа, аа – формальный вывод
4) L, ааа – не формальный вывод
5) L, аааа – не формальный вывод
Вопрос23.
Дать определение исчисления высказываний.
ИВ: 1) Язык: алфавит = {А1, А2, А3,…(бесконечно много переменных); знак Ù, Ú, ù, ® (логические (булевы) связки); ( , )} В ИВ имеются выражения лишь одного типа – формулы. Определение формул дается индуктивно: а) всякая переменная есть формула (атомная); б) если Ф1, Ф2 – формулы, то и (Ф1ÙФ2), и (Ф1ÚФ2), и (Ф1®Ф2), и ù Ф1 – формулы; в) никаких формул, кроме этих, нет.
2) Аксиомы: 1) (А1®(А2®А1)). Условимся о некоторых сокращениях. Разрешим вместо А1, А2,… употреблять А, В, С,… Откажемся от внешних скобок. Тогда: 1) (А1®(А2®А1))ºА®(В®А); 2) (А®(В®С))®((А®В)®(А®С)) – первая группа аксиом: группа импликаций. Группа конъюнкций: 3) (АÙВ)®А; 4) (АÙВ)®В; 5) (А®В)®((А®С)®(А®(ВÙС))). Группа дизъюнкций: 6) А®(АÚВ); 7) В®(АÚВ); 8) (А®С)®((В®С)®((АÚВ)®С)). Группа отрицаний: 9) А®ù ùА; 10) ù ùА®А; 11) (А®В)®(ùВ®ùА)
3) Правила вывода: а) modas ponens – правило заключения r1(Ф®Y, Ф)= Y; б) r2(Ф)=SYАФ, где SYАФ – результат подстановки в формулу Ф формулы Y вместо каждого вхождения переменной А в формулу Ф.
Пример вывода в ИВ.
Покажем, что формула А®А выводима. Построим вывод этой формулы: 1) А®(В®А) – аксиома; 2) (А®(В®С))®((А®В)®(А®С)) – аксиома; 3) (А®(В®А)) ®((А®В) ®(А®А)) – SACФ2; 4) (А®В) ®(А®А) – modas ponens Ф1, Ф3; r1(Ф®Y, Ф)= Y; 5) (А®(В®А)) ®(А®А) – SВ®АВФ4; 6) А®А – modas ponens Ф1, Ф5.
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.