Доказательство. 2 страница

1.8 Логические эквивалентности с кванторами

Теорема. Разноименные кванторы не всегда коммутируют.

Доказательство. Пусть имеется двуместный предикат D(x,y)= «x делится на y» на множестве натуральных чисел. Тогда очевидно, что $ x " y D(x,y) º0 и " y $ xD(x,y) º1.

Теорема. Имеют место следующие логические следования и эквивалентности

	"xP(x)≡$xØP(x)	Законы де Моргана
	Ø$x P(x) ≡"x ØP(x)
	" x " y P(x,y) ≡ " y " x P(x,y)	Коммутация одноименных кванторов
	$ x $ y P(x,y) ≡ $ y $ x P(x,y)
	" x(P(x)&Q(x))≡ " xP(x)& " xQ(x)	Законы дистрибутивности
	$ x(P(x)ÚQ(x))≡ $ xP(x)Ú $ xQ(x)
	" x(P(x)ÚQ(y))≡ " xP(x)ÚQ(y)	Законы ограничения действия
	" x(P(x)&Q(y))≡ " xP(x)&Q(y)	Кванторов
	$ x(P(x)&Q(y))≡ $ xP(x)&Q(y)
	$ x(P(x)ÚQ(y))≡ $ xP(x)ÚQ(y)
	$ y " x P(x,y)® " x $ y P(x,y)º1

Формула А находится в предваренной форме, если она имеет следуюший вид

А=Q₁x₁…Q_nx_nB(x₁,…x_n),

где Q₁,…,Q_n – некоторые кванторы, а В – бескванторная формула. Приставка Q₁x₁…Q_nx_n называется префиксом, а формула В – матрицей.

Теорема. Для любой формулы исчисления предикатов существует логически эквивалентная ей формула в предваренной форме.

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

· Исключают импликации

· Для внесения Ø внутрь скобок применяют законы де Моргана и закон двойного отрицания

· Для переноса кванторов применяют законы дистрибутивности, законы ограничения действия кванторов и равносильности с переименованием кванторов (Q₁ Q ₂ – кванторы существования или всеобщности)

(Q₁ x)P(x)& (Q ₂ x) R(x)≡ (Q₁ x) (Q ₂ z)(P(x)&R(z))

(Q₁ x)P(x)Ú (Q ₂ x) R(x)≡ (Q₁ x) (Q ₂ z)(P(x)ÚR(z))

Пример. Рассмотрим построение предваренной формы для формулы " xP(x)® $ x R(x).

" xP(x)® $ x R(x)≡ Ø( " xP(x))Ú $ x R(x) ≡ $ xØP(x)Ú $ x R(x) ≡ $ x(ØP(x)Ú R(x))

1.9 Термы и формулы в исчислении предикатов

Чтобы наглядно показать чем отличаются термы и формулы, рассмотрим следующий пример.

Пусть имеется предикат D(x,y)= «x+y>x» на множестве натуральных чисел N. Определим две функции f(x,y) и g(x,y), x, y Î N следующим образом:

.

Функция f(x,y) определяет истинностное значение предиката при определенных значениях предметных переменных x и y. Значение функции g(x,y) принадлежит той де предметной области, что и предметные переменные x и y. Для записи функций типа функции f(x,y) используются формулы, а для записи функций типа функции g(x,y) – термы.

Дадим точные определения формулы и терма в исчислении предикатов. Сначала определим алфавит формул и термов. В алфавит входят:

a) Предметные переменные x_i, y_j;

b) Функциональные переменные , n,m =0,1,2,…, n – арность (местность);

c) Предикатные переменные , n,m =0,1,2,…, n – арность (местность);

d) Логические символы ®, Ø, " (дополнительные Ú, &,$)

e) Служебные символы (,)

Последовательность символов в исчислении предикатов называется термом, если она удовлетворяет следующему определению:

1. любая предметная переменная, любая нульарная функциональная переменная является термом;

2. если Т₁,…, Т_n – термы, то (Т₁,…, Т_n)– терм;

3. других термов нет

Пример. Выражение является термом. Выражение не является термом.

Придадим теперь функциональным символам следующие значения: – умножение двух чисел, – возведение в степень, – сложение двух чисел. Тогда терм выгляди так . Полагая x₁=x₂ =1, x₃=x₄ =2, получаем, что терм равен 9. Таким образом, если заданы значения всех функциональных и предметных переменных, входящих в терм, то чтобы получить значение терма следует выполнить все операции сопоставленные переменным.

Дадим теперь определение формулы исчисления предикатов. Последовательность символов в исчислении предикатов называется формулой, если она удовлетворяет следующему определению:

1. Каждый предикатный символ арности нуль является формулой;

2. если – n =арный предикатный символ и Т₁,…, Т_n – термы, то (Т₁,…, Т_n)– формула. Все входящие в эту формулу предметные переменные – свободные;

3. если F₁, F₂ – формулы, то Ø(F₁), (F₁®F₂) –формулы. Свободные вхождения переменных в F₁, F₂ остаются свободными в формулах Ø(F₁), (F₁®F₂);

4. Если переменная x – свободная в F, то" x(F) – формула. Вхождения других переменных (отличных от x) остаются свободными в формуле" x(F);

5. других формул нет

Одна и та же переменная может иметь в одной и той же формуле как свободные, так и связанные вхождения. Формула, не содержащая свободных вхождений переменных, называется замкнутой. Квантор существования вводится определением $ хА:=Ø " xØA.

1.10 Аксиомы и правила вывода в исчислении предикатов

Поскольку ИП является расширением ИВ, то и множество аксиом ИП является расширением множества аксиом ИВ. Логическими аксиомами для ИП аксиомы ИВ и аксиомы ИП:

A₁: (A®(B®A)),

A₂: ((A®(B®C))®((A®B)®(A®C))),

A₃: ((ØB®ØA)®((ØB®A)®B)),

P₁: " x A(x)®A(t), где формула А(х) не содержит терм t

P₂: "x(A®B)® (A®"xB), если формула А не включает свободных вхождений х.

Правилами вывода в ИП служат:

§ (modus ponens): ,

§ правило обобщения .

Понятие выводимой формулы определяется так же, как и в исчислении высказываний.

Пример. Доказать выводимость в исчислении предикатов

"x"yA ├ "y"xA

Следующий вывод доказывает выводимость данной формулы

	"x"yA	гипотеза
	"x"yA ®"yA	P1
	"yA	MP 1,2
	"yA ®A	P1
	А	MP 3,4
	"хA	"+ 5
	"y"xA	"+ 6

Очень полезными оказываются производные правил вывода, которые позволяют сократить длину вывода формулы. Рассмотрим некоторые из них для исчисления предикатов.

Правило индивидуализации (ПИ) Если А(х) не содержит терм t, то "xA(х) ├ A(t).

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

	"xA(x)	гипотеза
	"xA(x) ®A(t)	P1
	A(t)	MP 1,2

Правило существования (ПС). Если терм t свободный для переменной х в формуле A(x), то A(t) ├ $ xA(x).

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

	"xØA(x)®ØA(t)	P1
	("xØA(x)® ØA(t))® (A(t)®Ø"xØA(x))	(A®ØB)®(B®ØA)– тавталогия B A(t), A"xØA(x)
	A(t)®Ø"xØA(x) A(t)®$ xA(x)	MP 1,2

1.11 Теоремы об исчислении предикатов первого порядка

Исчисление предикатов, которое не содержит предметных констант, функторов, предикатов и собственных аксиом, называется чистым. Исчисление предикатов, которое содержит предметные константы и (или), функторы и (или) предикаты и связывающие их собственные аксиомы, называется прикладным. Исчисление предикатов, в котором кванторы могут связывать только предметные переменные, но не могут связывать функторы, предикаты или иные множества объектов, называются исчислениями высших порядков.

Значение формулы определено лишь тогда, когда задана какая-нибудь интерпретация входящих в нее символов. Под интерпретацией (моделью) будем понимать предметную область W с определенными на ней n-арными предикатами.

Формула A выполнима в данной модели, если существует набор < a ₁, a ₂,..., a _n>, a _i ÎW, значений свободных переменных x ₁, x ₂,..., x _n формулы A такой, что A (a ₁, a ₂,..., a _n) принимает значение истина.

Формула A истинна в данной модели, если она принимает значение истина на любом наборе < a ₁, a ₂,..., a _n>, a _i ÎW значений своих свободных переменных x ₁, x ₂,..., x _n.

Формула A общезначима или (тождественно истинна в логике предикатов), если она истинна в любой интерпретации.

Формула A выполнима (в логике предикатов), если существует модель, в которой A выполнима.

Формула А – тавталогия в ИП, если тавталогией является формула, полученная из А опусканием всех кванторов и термов вместе со всеми соответствующими скобками и переменными. Например, аксиома P₁: " x A(x)®A(t) является тавталогией, поскольку формула A®A тавталогия.

Теорема. Если формула А – тавталогия в ИП, то А является теоремой в ИП и может быть введена с использованием лишь аксиом A₁, A₂,A₃ и правила вывода МР.

Теорема. (Теорема Геделя о полноте исчисления предикатов) Формула доказуема в исчислении предикатов тогда и только тогда, когда формула общезначима.

Доказательство. Покажем только необходимость утверждения, поскольку доказательство достаточности более сложное. Аксиомы ИП являются общезначимыми формулами. При использовании правил вывода для общезначимых формул можно получить только общезначимую формулу.

Теорема (Теорема Черча о неразрешимости исчисления предикатов ).

ИП является полуразрешимой теорией

1.12 Метод резолюций для исчисления предикатов

Метод резолюций используется во многих системах логического программирования. Метод был предложен в 1965 г. А. Робинсоном

Метод резолюций работает с особой стандартной формой формул, которые называются предложениями. Предложение – это бескванторная дизъюнкция литералов. Любая формула ИП может быть преобразована во множество предложений, используя следующие шаги.

· Приведение к предваренной форме,

· Элиминация кванторов существования с использованием преобразований

$ x₁Q₂x₂…Q_nx_nA(x₁,x_2,…x_n)Þ Q₂x₂…Q_nx_nA(a,x_2,…x_n)

" x₁ …" x_i-1 $ x_iQ_i+1x_i+1…Q_nx_nA(x₁,…,x_i,…x_n) Þ

Þ" x₁… " x_i-1Q_i+1x_i+1…Q_nx_nA(x₁,…,f(x_1,…x_i-1),…x_n),

где а – новая предметная константа, f – новый функциональный символ, Q₂,…,Q_n – любые кванторы. После этого этапа формула содержит только кванторы всеобщности. Такой вид формул называется скулемовская стандартная форма.

· Элиминация кванторов всеобщности с использованием преобразования

" х А(х) ÞА(х)

После этого шага формула не содержит кванторов.

· Приведение к конъюнктивной нормальной форме и элиминация конъюнкций. После этого этапа получаем множество предложений, соответствующее формуле.

Пример. Преобразовать во множество предложений формулу

"x(P(x)®$y(E(y)&D(x,y))

"x(P(x)®$y(E(y)&D(x,y))º"x(ØP(x)Ú$y(E(y)&D(x,y))º

º"x$y(ØP(x)Ú(E(y)&D(x,y))Þ "x(ØP(x)ÚE(f(x))&D(x,f(x)) Þ

ÞØP(x)ÚE(f(x))&D(x,f(x))º(ØP(x)ÚE(f(x)))&(ØP(x)ÚD(x,f(x))) Þ{ØP(x)ÚE(f(x)),ØP(x)ÚD(x,f(x))}

При рассмотрении метода резолюций для исчисления высказываний особое внимание уделялось поиску контрарных пар во множестве предложений. В логике предикатов этот поиск заметно усложняется, поскольку в формулы входят предметные переменные.

Рассмотрим пример. Пусть имеется два предложения C₁ и C₂ (P, R, Q – предикаты)

C₁=P(y)ÚR(y),

C₂=ØP(f(x))ÚQ(x).

Не существует ни одной литеры в C₁ контрарной какой-либо литере в C₂. Однако если подставить терм f(а) вместо y в предложении C₁ и а – вместо х в C₂, то получим предложения C₁’ и C₂’, в которых уже существуют контрарные литеры (P(f(а)), ØP(f(а)))

C₁’=P(f(а))ÚR(f(а)),

C₂’=ØP(f(а))ÚQ(а).

Следовательно, эти два предложения можно резольвировать и получить резольвенту C₃’= Q(а)Ú R(f(а)). Таким образом, для получения резольвент из предложений в логике предикатов необходимо выполнить подстановки соответствующих термов вместо переменных.

Пусть X – множество предметных переменных из W и T – множество термов над переменными из X. Подстановкой называется отображение s: X® T. Подстановка s называется конечной, если s(х)¹ х лишь для конечного числа элементов х из X. Подстановка, не имеющая элементов, называется тождественной. Подстановку будем обозначать как множество пар s={x₁t₁, …, x_kt_k }, x₁, …, x_k – переменные, t₁, …, t_k – термы.

Пусть имеется две подстановки s={x₁t₁, …, x_kt_k} и n = {y₁p₁, …, y_np_n}. Произведением подстановок s и n называется подстановка s*n, полученная из множества { x₁n(t₁),…,x_kn(t_k), y₁p₁,…,y_np_n } отбрасыванием всех элементов, имеющих вид x_jn(t_j), для которых n(t_j)= x_j и всех элементов y_jp_j таких, что y_jÎ{x₁, …, x_k}. Приведем пример произведения подстановок. Пусть

s={x₁t₁, x₂t₂}={xf(y), yz},

n = {y₁p₁, y₂p₂, y₃p₃}={xa,yb, zy}.

Тогда s*n={xn(f(y)), yn(z), xa, yb, zy}. Поскольку n(z)= y, то элемент yn(z) отбрасываем. Также отбрасываем элементы xa, yb, т.к. x и y принадлежат множеству термов первой подстановки. Окончательно получаем s*n={xf(b), zy}

Подстановка s называется унификатором для множества термов {t₁, …,t_k}, если s(t₁)= s(t₂)=…= s(t_k). В рассмотренном выше примере подстановка s={xа,у f(а)} является унификатором для множества термов {f(x), y}. Наименьший возможный унификатор называется наиболее общим унификатором (НОУ).

Пусть имеется две конечные последовательности термов (t₁, …, t_k) и (p₁, …, p_k). Унификатором двух последовательностей термов называется подстановка s такая, что s(t₁)=s(p₁), …, s(t_k)=s(p_k).

Рассмотрим теперь правило резолюции, т.е. правило вывода, которое используется в методе резолюций. Пусть А и В – два предложения в исчислении предикатов. Правило вывода называется правилом резолюции в исчислении предикатов, если в предложениях А и В существуют унифицируемые контрарные литералы Р₁ и Р₂, т.е. А=Р₁Ú А₁ и В=ØР₂Ú В₁, причем Р₁ и Р₂ являются унифицируемыми унификатором s. В этом случае резольвентой предложений А и В является предложение (А₁ÚВ₁) s, полученное из предложения А₁ÚВ₁ применением унификатора s.

Пусть нужно установить выводимость Г├ F в ИП методом резолюций. Воспользуемся доказательством от противного и будем доказывать выводимость Г, ØF├ Æ. Для этого каждая формула множества Г и формула ØF независимо преобразуются в множества предложений. В полученном совокупном множестве предложений отыскиваются резольвируемые предложения, к ним применяется правило резолюции в ИП и резольвента добавляется во множество до тех пор, пока не будет получено пустое предложение. При этом возможны три случая:

· Среди текущего множества предложений нет резольвируемых. Это означает, что теорема опровергнута, т.е. формула F не выводима из множества формул Г.

· В результате очередного применения правила резолюции получено пустое предложение. Это означает, что теорема доказана, т.е. Г├ F.

· Процесс не заканчивается, т.е. множество предложений пополняется все новыми резольвентами, среди которых нет пустых. Это ничего не означает.

Таким образом, ИП является полуразрешимой теорией, а метод резолюций является частичным алгоритмом автоматического доказательства теорем.

Пример. Покажем выводимость формулы "х"уА(х,у)® "у"хА(х,у) методом резолюций. Возьмем отрицание этой формулы и преобразуем во множество предложений.

Ø("х"уА(х,у)® "у"хА(х,у))º Ø(Ø("х"уА(х,у))Ú "у"хА(х,у))))º "х"уА(х,у)& Ø("у"хА(х,у)) º ("х"уА(х,у))& ($y$xØА(х,у)) º("y"xА(х,у))& ($y$xØА(х,у))º

º"y$y₁"x$x₁(А(х,у)&ØА(х₁,у₁))º"y"x(А(х,у)&ØА(g(х,y),f(у)))Þ {А(х,у),ØА(g(х,y),f(у))}

Резольвируем полученное множество предложений

	А(х,у)	xg(a,b), yf(b)
	ØА(g(х,y),f(у))	xa, yb
	Æ	ПР из 1,2

Выводимость доказана.

Пример. Проверить правильность рассуждения

Всякий, кто может решить эту задачу, – математик.

Ни один математик не может решить этой задачи.

Значит, она неразрешима.

Определим на множестве людей следующие предикаты

R(x)= «х может решить эту задачу»

M(x)= «х математик»

Тогда фразы можно записать в логической символике следующим образом

"х (R(х) → M(x))

$ х (M(x) →R(х))

$ х R(х)

или

"х (R(х) → M(x)), $ х (M(x) →R(х)) ├ $ х R(х)

Проверим выводимость методом резолюций. Возьмем преобразуем во множество предложений гипотезы и отрицание вывода.

Множество предложений { R(х)Ú M(x), R(х), M(x), R(a) } легко резольвируется до получения пустой формулы. Таким образом, данное рассуждение правильное.

2. Элементы теории алгоритмов и рекурсивных функций

2.1 Понятие алгоритма

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

Теория алгоритмов получила бурное развитие в 40-х годах прошлого столетия в связи с созданием быстродействующих электронных вычислительных и управляющих машин. Появление ЭВМ способствовало развитию теории алгоритмов, вызвало к жизни разделы этой теории (алгоритмические системы и алгоритмические языки), имеющие ярко выраженную прикладную направленность. Наконец, теория алгоритмов оказалась тесно связанной и с рядом областей лингвистики, экономики, физиологии мозга и психологии, философии, естествознания. Примером одной из задач этой области может служить точное описание алгоритмов, реализуемых человеком в процессе умственной деятельности.

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

Алгоритм – это совокупность правил, соблюдение которых при вычислениях приводит к решению поставленной задачи. Это неформальное определение алгоритма, известное еще со времен Аль Хорезми (IX век). Можно выделить некоторые черты, присущие каждому алгоритму.

· Дискретность. Преобразование начальных данных происходит пошагово. На каждом шаге из данных по правилам получается новая совокупность данных.

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

· Направленность. Для алгоритма есть критерий, позволяющий определить, что является результатом работы алгоритма.

· Элементарность шагов алгоритма. Описание действий на каждом шаге алгоритма должно быть достаточно простым.

· Массовость. Применимость алгоритма не к одной задаче, а к целому классу задач.

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

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

2.2 Машина Тьюринга

Первый важный и достаточно широкий класс алгоритмов был описан Тьюрингом и Постом в 1936-1937гг. Алгоритмы этого класса осуществляются особыми машинами, называемыми в настоящее время машинами Тьюринга-Поста или просто машинами Тьюринга. Машины Тьюринга копируют в существенных чертах работу человека, вычисляющего по заданной программе, и часто рассматриваются в качестве математической модели для изучения функционирования человеческого мозга.

Поскольку алгоритм по сути – это совокупность правил, то чтобы решить проблему интерпретации (понимания) правил, необходимо задать конструкцию интерпретирующего устройства. Для этого нужно определить язык, на котором описывается множество правил поведения, и машину, которая может интерпретировать утверждения, сделанные на таком языке, и таким образом, выполнять шаг за шагом каждый точно определенный процесс.

Английский математик А.М.Тьюринг в 1937 году впервые предложил модель вычислительной машины, известной теперь под названием машина Тьюринга, которая представляет собой воображаемую машину или математическую модель машины.

Машины Тьюринга – чистая абстракция и никогда не были реализованы. Польза от нее в том, что с ее помощью можно доказать существование или несуществование алгоритмов решения различных задач. Так как машина выполняет определенный алгоритм, то к машине предъявляются требования, вытекающие из свойств алгоритмов. Во-первых, машина должна быть полностью детерминированной (вычисления должны быть точные и общепонятные) и действовать в соответствии с заданной системой правил. Во-вторых, она должна допускать ввод различных “начальных данных” (соответствующих различным задачам из данного класса задач). В-третьих, заданная система правил работы машины и класс решаемых задач должны быть согласованы так, чтобы всегда можно было “прочитать” результат работы машины.

Под одноленточной машиной Тьюринга понимают такое кибернетическое устройство, которое состоит из следующих элементов: