Альтернативные системы аксиом

 

Альтернативные системы аксиом

Система аксиом Гилберта Иакермана

Связки:

, ,

Вводятся следующие аксиомы:

Система аксиом Россера

Вводятся связки:

&,-,A->B=-(A&-B)>(A&A)&B->B

(A->B)->(-(B&C)->-(C&A))

Система аксиом Мередита:

(Связки: ->, -)

[((A->B)->(-C->-D))->C]->((C->A)->(D->B))

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

Если дана формула Ф(А1… Аn) и имеются некоторые формулы Ф1…Фn, то мы можем получить формулу Ф(Ф1…Фn), подставив формулы Фi вместо соответствующих пропозиционных переменных.

Система аксиом Клини.

(K1) А->(B-A)

(K2)

(K3) A&B->A

(K4) A&B->B

(K5) A->(B->(A&B))

(K6) A->(AB)

(K7) B->(AB)

(K8) (A->C)->((B->C)->((AvB))->C

(K9) (A->B)->((A->-B)->-A)

(K10) - -A->A

Здесь все логические связки вводятся напрямую, а не рассматриваются, как сокращения друг друга.

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

Например, рассмотрим эквивалентность формул:

(A->-B) в аксиоматике ИВ L и A&B.

На основании схемы К5 и МР доказывается, что из формулы A&B выводится формула в аксиоматике К формула А->В. Далее на основе аксиом К3 и К4 видим что из A&B выводится А, из A&B выводится В.

В теории L имеется тавтология A->(B->-(A->-B)) выводимость которой можно доказать с помощью теоремы о полноте. Исходя из этой формулы и МР, получаем, что .

В аксиоматике L имеет место тавтологии и , следовательно, по МР имеем и .

В итоге можно сделать вывод (A&B).

На основании вышеизложенного, можно сделать вывод

По аналогии можно вывести

Что касается , то уже было доказано и.

Таким образом, мы можем переносить аксиомы между схемами аксиом.

Теорема

Рассмотрим теоремы:

F1…Fn,

т.е. тогда, когда последняя формула является тавтологией.

Рассмотрим доказательство:

Выводимость G и множества F1…Fn означает по теореме дедукции

F1,F2…Fn-1Fn->G…

(тут типа все через импликации через вложенные скобки)

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

Представим импликацию через дизъюнкцию:

Отсюда следует, что выводится т. и т.т., когда последняя формула является тавтологией.

Пример покажем с использованием ModusTollens.

Покажем, что

Для этого нам нужно доказать что

является тавтологией

Просто находим таблицу истинностей для всех значений P и Q.

F1…Fn,

т.е. является противоречием.

Док - во. В соответствие с предыдущей теоремой, эта теорема равносильна является тавтологией, это в свою очередь равносильно , раскроем импликацию

,

далее по законам Де Моргана

В качестве примера рассмотрим доказательство корректности еще одного правила вывода ModusTollendoTollens. Т.е. покажем, что

В соответствии с только что доказанной теоремой надо вывести, что

по таблице истинности видно, что это верно.

Теорема

F1,…,FnýGÛ когда выводима формула ýF1&F2&…&Fn®G, т.е. когда эта формула - тавтология

Док-во:

F1,…,Fn |- Góпо теореме дедукции F1,…, Fn-1 |- FnàG<=>F1,…, Fn-2 |- Fn-1à (FnàG) <=> … <=> |- F1à (F2à … à (Fnà G) … ) <=> {по теореме ополноте} <=>F1à (F2à … à (FnàG) … ) - тавтология ? =

ùF1V (F2à … à(FnàG) … ) = … = ùF1VùF2V … VùFnVG = (по з-ну Де Моргана) = ù (F1&F2& … &Fn) VG = F1&F2& … &Fnà G - тавтология.

Теорема:

F1, … ,Fn |- G<=>

является ли формула F1&F2& … &Fn&ùG - противоречием ?

Док-во:

По предыдущей теореме: F1, … ,Fn |- G<=>F1&F2& … &FnàG - тавтология ? <=>ù (F1&F2& … &FnàG) - противоречие ?<=>ù (ù (F1&F2& … &Fn) VG) - противоречие ?<=> {по з-ну Деморгана} <=>F1&F2& … &Fn&ùG - противоречие ?

Способ доказательства утверждения от противного: (А àB) à (ùBàùA).

Пример:

Докажем, что из формулы PàQ и ùQ выводится ùP, т. е. PàQ, ùQ |- ùP/

По 1-й теореме достаточно показать, что формула ((PàQ) &ùQ) àùP - тавтология.

PQ123ЛЛИИИЛИИЛЛИЛЛЛЛИИИЛЛ

тавтология=>такая выводимость имеет место.

Приведение формулы к КНФ. Выводимость на основе противоречия

Дизъюнктом наз. дизъюнкция пропозициональных переменных или их отрицаний, кот.наз. литералами. Для простоты дизъюнкт принято записывать как перечень литералов, т. е. если C = L1VL2V … VLn, то С = (L1, …, Ln).

КНФ наз. логическое произведение дизъюнктов. Принято считать, что в дизъюнкте переменные и литералы не повторяются, т. к. LVL = L, LVùLº И (тождественная истина).В КНФ нет одинаковых дизъюнктов, т. к. C&C = C.

Пример:

(AVùB)(AVC)( ùAVB) - КНФ.

КНФ тоже можно записывать как множество дизъюнктов. Т. е. есть

КНФ С1 С2 … Сn => (C1, C2, …,Cn) - КНФ.

Приведем формулу

F1& … Fn&ùG к КНФ => вопрос: КНФ - противоречива ?

Для приведения формулы к КНФ используются тождества булевой алгебры:

A à B = ù A V Bº B = (A à B)(B à A)&И = AV И = И& (B V C) = (A & B) V (A & C)V (B & C) = (A V B) & (A V C)

ù (AVB) = ùA&ùB

ù (A&B) = ùAVùB

з-ны иденпатентности, ассоциативности, дистрибутивности.

Пример: (AàB) V (A&ùC) приведем к КНФ.

(A à B) V (A &ù C) = ù A V B V (A &ù C) = (ù A V B V A) & (ù A V B V ù C) = ù A V B V ù C.

Теперь проверяем на противоречивость КНФ.

Резольвентой 2-х дизъюнкта R(C1, C2), где

C1 = L1 V L2 V … V Lk,2 = ù L1 V L2 V … V Lm,

наз. R(C1, C2) = L2 V … V Lk V L2 V … V Lm

Пример: C1 = A V ù B V C, C2 = ù A V ù B V D

Тогда R(C1, C2) = ùBVCVD

Замечание: не имеет смысла искать R(C1, C2), если C1 = ùAVB, а C2 = AVùB, т. к. в любом случае получим ТИ (и по А, и по В), а мы ищем противоречивость формулы.

Понятие резольвенты. Логическое следование резольвенты из дизъюнктов

Пусть C1, … Cm - мн-во дизъюнктов, тогда резолютативным выводом из этого множества дизъюнкта D наз. цепочка дизъюнктов A1, A2, …, Ak (=D), где A1 - либо исходный дизъюнкт, либо получен из исходных дизъюнктов с помощью метода резолюций.

Лемма: резольвента является логическим следствием своих дизъюнктов, т. е. R, C1, C2. C1&C2àR - тавтология (*).

Док-во:

Если R - резольвента

С1, С2, то С1 = LVL1V … V Lk, C2 = ù L V L1 V … V Lm.

Если (С1&C2) = Л, то ф-ла (*) - И

·если истина - 1 из литералов L1, …, Lk (C1), то этот литерал войдет и в R =>R - истина => импликация - истина;

·если С1 = И за счет литерала L, по С2 - тоже истина, а ùL = Л, а С2 = И за счет какого-то литерала кроме L => этот литерал войдет и в R =>R = И => импликация - И.

Следствие: Пусть дана КНФ С1& … &Cn и резольвента R = R(Ci, Cj). Тогда эта формула КНФ C1& … &CnºC1& … &Cn&R.

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

Если л.ч. = Л =>п.ч. = Л

Если л.ч. = И =>п.ч. = И (по лемме)

Замечание: для проверки на противоречивость КНФ (мн-ва дизъюнктов) можно порождать резольвенты до тех пор, пока не получим ТЛ.

Резольвенты находятся не только для исходных дизъюнктов, но и для тех резольвент, кот. порождаются.

Теорема о полноте метода резолюций

Теорема о полноте метода резолюций:

КНФ (множество дизъюнктов) - противоречие <=> из множества дизъюнктов выводится резолютотивно пустой дизъюнкт.

Док-во:

Если выводим пустой дизъюнкт, то формула - противоречие. Это возможно только в том случае, если

C1 = L, C2 = ùL

Но тогда имеем КНФ: LùLº Л.

{C1& … &Cn = C1& … &Cn&R1 = … = C1& … &Cn&R1& … &L&ùLº Л}

II

Пусть исходная формула - противоречие. Покажем, что выводится пустой дизъюнкт (по индукции).

Есть C1, …, Cn

Выводится пар-р K(S) = å (кол-во вхождений всех литералов) - n (кол-во дизъюнктов) аксиома резолюция противоречие

Например, КНФ: (ùBVA)C(BVùD)K(S) = 5 - 3 = 2

БИ: докажем справедливость при K(S) = 0 (для всех таких формул)

K(S) = 0 <=> формула имеет вид L1L2 … Lnº Л, т. е. в дизъюнкте 1 литерал, КНФ - произведение литералов <=> эта формула º Л <=> , когда в ней есть пара L и ùL => пустой дизъюнкт выводится.

Индуктивный переход: пусть мы доказали для k£m. Докажем для формулы, у которой k = m + 1 > 0.

Если K> 0 => 1 из дизъюнктов содержит хотя бы 2 литерала (пусть С1).

С1 = LVC1.

Исх. формула: S = C1& … &Cn = C1& S = (L V C1) S.

Эта формула -противоречие <=>, когда формула S = LS VC1S - противоречие.

Но у формул LS и C1S характеристика К меньше, чем у формулы S на 1.

Берем КНФ C1S (для нее выполнимо предположение индукции) => для нее пустой дизъюнкт выводим (с помощью метода резолюций). Берем этот вывод, кот. применяли к C1S и применяем его к S. S и C1S отличаются тем, что во 2-й формуле отбросили литерал L. Тогда из S получим либо пустой дизъюнкт, либо литерал L => из S можно вывести L. По предположению индукции из LS можно получить пустой дизъюнкт => получился вывод из S пустого дизъюнкта.

Алгоритм метода резолюций для ЛВ

Алгоритм метода резолюций для исчисления высказываний.

Представляем формулу, противоречивость которой нужно показать в виде КНФ. Для этого можем пользоваться алгеброй тождеств булевой алгебры.

i=1

Находим все всевозможные резольвенты

Дополняем исходное множество всеми найденными резольвентами.

(Батарея села)

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

Понятие предиката, функции, терма

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

Рассмотрим классический пример: пусть имеются предпосылки: все люди смертны, Сократ-человек, следовательно Сократ - смертен. С точки зрения логики вывод здесь безупречен, но он уже выходит за рамки ИВ. С помощью пропозициональных связок и букв:

.

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

Лена и Таня сестры.

В море корабли.

Кот отобрал еду у Ковалева.

Снег белый.

Мальчик отправил брату письмо.

По правилам ИП эти предложения можно записать следующим образом:

Сестры (Лена, Таня)

В (море, корабли)

Отобрал еду (кот, Ковалев)

Белый (снег)

Отправил (мальчик, брат, письмо)

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

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

По количеству термов выделяют одноместные предикаты, двуместные и многоместные. Предикатную форму так же называют атомом. Термы так же могу иметь разнообразный вид, в первом примере оба терма обозначены конкретными объектами (Лена и Таня), такие объекты называются индивидными константами, во втором примере оба терма заданы в самом общем виде, какие-то корабли в каком-то море, их можно просто обозначить через x,y. В данном случае они представляют собой индивидные переменные.

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

Не следует путать предикатный и функциональный символы.

Предикат Отец (x,y) - означает x является отцом y. Это либо правда, либо нет, поэтому область значений предиката - это множество {0,1} или {И, Л}. Тогда как функция O(y), обозначающая отец объекта y, в качестве области определения имеет все человечество. Область значений данной функции - это мужская половина человечества, достигшая определенного возраста.

Равенство x=O(y), означает «Отцом y является x».

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

Алфавит ИП

Словарь ИП содержит:

Константы - a,b,c

Переменные - х,y,z

Функциональные - f,g,h

Предикатные -P,Q,R

Высказывания - p,q,r

Пропозициональные связки -

Кванторы общности - .

Рассмотрим понятие формулы - вначале введем понятие терма по индукции:

Предметные константы и переменные - это термы

Если t1…tn - это термы, и f - n-местная функция, то f(t1…tn) - тоже терм, других нет.

Атомарная формула - это предикат, в который подставлены термы A(t1…tn).

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

Пример: пусть имеем формулу . В первом случае связная, во втором свободная.

Высказывания можно воспринимать как 0-арный предикат.

Обозначения с - Сократ, H - «быть человеком», M - «быть смертным».

Навешиванием квантора всеобщности предикату мы фактически сопоставляем k-арный предикат который истинен тогда и только тогда, когда истинен исходный предикат с этими значениями и любым значением x0.

По аналогии навешиванием квантора существования и (к+1)- арного предиката Р(х0, …, хк) получаем к-арный предикат. Сущ. х0 Р(х0, х1,…, хк) - этот предикат истинен тогда и только тогда, когда исходный предикат для тех же значений переменных истинен хотя бы на 1 из возможных значений х0.

Понятие подстановки в ЛП

Согласно определению терма, множество всех термов T(F) содержит так же множество переменных Х. Подстановкой называется отображение v:X->T(F) такое что для всех х прин. Х за исключением некоторого подмножества из Х имеет место v(x)=x, т.е. в том случае когда х попадает в это конечное счетное множество Х она заменяется некоторым, указанным для нее термом, в противном случае - остается собой. F - множество функций, применяемых теорией. T - множество термов теории с учетом множества функциональных символов F .

Распространив подстановку v до некоторой функции v: T(F)->T(F) полагаем:

1)Если то

)Если t - символ константы, то

)Если для некоторой n-арной операции F, то

Терм называется результатом подстановки v к терму t.

Пример: пусть у нас присутствуют 3 переменные . Будем рассматривать функции свойственные теории множеств, т.е.

,

Введем подстановку:

Тогда:

Подстановку часто записывают в виде пар {xi=ti}

Пусть заданы 2 терма s и t. И надо найти подстановку, делающую их равными. Подстановка v называется унификатором s и t если .

Унификатор называется наибольшим общим унификатором s и t и обозначается m.g.u(s,t)=v. Если для любого другого унификатора w тех же самых термов s и t существует такая подстановка , что композиция . Композицию можно рассматривать как суперпозицию. Если для термов существует хотя бы 1 унификатор, то среди унификаторов существует наибольший общий.

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

1)Подстановки применяются только для свободных переменных (в том числе и функциональных), во всех местах их вхождения в данную форму.

2)Переменную можно заменить константой, но не наоборот.

3)Не следует заменять переменные содержащие ту же самую переменную т.е. - неправильная. (один пункт пропустил)

)Одна функция не может подставляться вместо другой но может

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

A(x:=t) - получаем из формулы А заменой x на t.

Понятие интерпретации в ЛП. Выполнимость, общезначимость, невыполнимость и противоречивость формул

Интерпретации.

Говорим, что задана интерпретацияI для формулы или множество формул I, если задано не пустое множество Р называемое областью интерпретации. Каждому символу сопоставляется элемент из Р, каждому символу предиката сопоставляется отношение. Каждому символу функции реальная функция из множества G. Формула выполнима, если есть интерпретация, в которой она истина.

Определение: Замыканием формул А с параметрами х1,х2,..,хn является формула вида: для каждого х1,х2,..хn А. Формула исчисления предикатов называется общезначимой, если ее замыкание истинно в любой интерпретации. При проверке общей значимости формул важно помнить, что по ее параметрам берутся кванторы всеобщности. Например, квадрат действительного числа положителен, но оно не общезначимо, т.к. 0 в квадрате =0, что не является положительным числом. Общезначимым будет утверждение квадрат любого действительного числа неотрицателен. Формула называется невыполнимой, если замыкание ее отрицания общезначимо. Формула выполнима если не верно, что она невыполнима. Общезначимость формулы - это обобщение тавтологии в ИВ. Можно сформулировать это утверждение более формально. Интерпретация называется моделью формул или множеством формул, если на ней все формулы тождественно истины. Формулы А и В эквивалентны, если каждая из них является логическим следствием другой.

Общезначимость тавтологий

Общезначимые формулы - это обобщение тавтологий в исчислении высказываний. Исчисление высказываний позволят выводить все тавтологии из некоторого набора базисных тавтологий (названных аксиомами) с помощью некоторых правил вывода (на самом деле единственного правила modusponens).

1)Пусть A - тавтология, x1,. . . , xn - набор пропозициональных переменных, которые входят в A, а F1, . . . , Fn - формулы ИП. Тогда формула A(F1, . . . , Fn) общезначима.

2)Докажем, что формула ? x ? y A(x, y)?? y ? x A(x, y) общезначима.

Интерпретацию бинарного предикатного символа удобно представлять в виде ориентированного графа (быть может, бесконечного). Множествовершин графа совпадает с областью интерпретации,а упорядоченная пара (x, y) принадлежит множествурёбер графа тогда и только тогда, когда пара (x, y)принадлежит отношению [A].

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

Исчисление предикатов 1-го порядка

Говорят, что задано исчисление предикатов первого порядка, когда:

) задан алфавит:

¾счётного множества X символов переменных;

¾счётного множества P предикатных символов;

¾счётного множества F функциональных символов;

¾символов пропозициональных связок ? и ¬

¾кванторного символа ?(квантор всеобщности);

¾служебных символов: скобок закрывающей ) и открывающей (, а также символа запятой,.

2) введено понятие формулы;

) заданы аксиомы исчисления высказываний:

A?(B?A) (A1)

(A?(B?C))?((A?B)?(A?C)) (A2)

(¬B?¬A)?(( ¬B?A)?B) (A3)

и кванторныесхемы аксиом:

?xA?A(x:=t) в условиях (A4)

? x(A?B)?(A??xB) в условиях (A5)

) заданы правила вывода:

¾modus ponens:

если выводимы формулы A и A?B, то выводима формула B.

¾правилом обобщения (Gen):

если выводима формула A, то выводима формула ?xA.

Общезначимость для каждого хAàA(x:=t)

Теорема. Если терм t свободен для переменной x в формуле A, то формула ?xA?A(x:=t) общезначима.

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

Если заключение импликации истинно, то и вся импликация истинна.

Теперь предположим, что в некоторой интерпретации при некоторой оценке переменных ? формула A(x:=t) имеет оценку ложь.

Обозначим через ? оценку терма t при оценке переменных ?. Рассмотрим оценку переменных ??, которая отличается от оценки ? разве что в переменной x, оценка ?? которой равна ?. Сравним оценку формулы A при оценке переменных ?? и оценку формулы A(x:=t) при оценке переменных ?.

Так как терм t свободен для переменной x в формуле A, то свободны все вхождения переменных в экземпляры терма t, подставленные вместо свободных вхождений x. Поэтому при оценке формулы A(x:=t) оценка любой вершины, которая лежит на пути от вершины t к корню, использует лишь оценку ? терма t при оценке переменных ? (последнее правило оценки не применяется, так как все вхождения переменных втерм t свободны).

В точности те же оценки получат эти вершины, когда вычисляется оценка формулы A при оценке переменных ??.

В остальных вершинах оценки формул A и A(x:=t) и подавно совпадают (там записано одно и то же).

Итак, при оценке переменных ?? оценкой формулы A является ложь. То же самое верно для формулы A(x:=t) при оценке ?. Тогда по последнему правилу оценки формула ?xA имеет оценку ложь при оценке ?. Значит, в этом случае оценка формулы ?xA?A(x:=t) - истина.

Итак, при обеих возможных оценках формулы A(x:=t) формула ?xA?A(x:=t) имеет оценку истина. Поэтому она общезначимая.

Корректность ИП и следствия из нее

Теорема. В ИП выводимы только общезначимые формулы.

Доказательство. Нужно проверить общезначимость аксиом и то, что правила вывода сохраняют общезначимость. Мы уже доказали общезначимость аксиом: аксиомы (A1-A3) общезначимы по утв. 3.38 («Пусть A - тавтология, x1,. . . , xn - набор пропозициональных переменных, которые входят в A, а F1, . . . , Fn - формулы ИП. Тогда формула A(F1, . . . , Fn) - общезначима»), а общезначимость аксиом (A4-A5) доказана в утверждениях3.48, 3.45 («Если терм t свободен для переменной x в формуле A, то формула ?xA?A(x:=t)-общезначима» и «Если в формуле A нет свободных вхождений переменной x, то формула ? x(A?B)?(A??xB) - общезначима»).

(A1)

(A2)

(A3)

(A4)в условиях 3.48

(A5) в условиях 3.45

Если при некоторой оценке переменных формулыA, A?B истинны, то и формула B также истинна при этой оценке переменных. Поэтому правило modusponens из общезначимых формул выводит только общезначимые.

Остаётся проверить, что правило обобщения сохраняет общезначимость. Действительно, из общезначимости A следует, что в любой интерпретации при любой оценке переменных она истинна. Но тогда по определению интерпретации квантора формула ?x A также истинна в любой интерпретации при любой оценке переменных.

Как следствие получаем непротиворечивость исчисления предикатов. Поскольку в исчислении предикатов выводятся только общезначимые формулы, то из формул A и -|A выводимой может быть только одна.

Буквально так же, как в исчислении высказываний, определяется вывод из множества формул (гипотез). Формулы, выводимые из аксиом исчисления предикатов и аксиом некоторой теории T , называются выводимыми в T или (формальными) теоремами теории T. Так как аксиомы исчисления предикатов содержат аксиомы исчисления высказываний, а правило modus ponens является одним из правил вывода, то любая тавтология выводима в исчислении предикатов. Мы сформулируем это утверждение в виде леммы.

Лемма 3.53. Пусть A1, A2, . . . , An- формулы исчисления предикатов, а ?(x1, . . . , xn) - тавтология, в которую входят переменные x1, . . . , xn. Тогда формула ?(A1, . . . ,An) выводима в исчислении предикатов.

Доказательство этой леммы очевидно: нужно подставить в вывод формулы ? в исчислении высказываний вместо переменных xi формулы Ai. Полученная последовательность формул будет выводом в исчислении предикатов.

Ослабленная и слабая теорема дедукции

Теорема 3.54 (ослабленная теорема дедукции).Если ?,A ? B и существует вывод B из ?,A, в котором не применяется правило обобщения к свободным переменным формулы A, то ? ? A?B.

Доказательство. Следуем схеме доказательства теоремы дедукции для исчисления высказываний: вывод ?1, . . . ,?n формулы B из гипотез ?,A, который существует по условию теоремы, заменяется на последовательность формул A??1, . . . ,A??n и индукцией по n доказывается, что эту последовательность можно дополнить до вывода. Для этого надо разобрать два случая.

. Формула ?i является аксиомой (A1-A5) или формула ?i получена по правилу modusponens из предыдущих формул ?j , ?k, j, k < i. В этих случаях построение вывода A??i в предположении, что уже выведены формулы A??k, k < i, в точности повторяет доказательство теоремы дедукции для исчисления высказываний.

. Формула ?i является выводом по правилу Gen из формулы ?k, k < i. Это означает, что ?i = ?x?k. Добавим следующие формулы перед формулой A??i:

? x(A??k) (Gen)

? x(A??k)?(A??x?k) (A5)

В первой строке правило обобщения применяется к формуле A??k, которая встречается раньше формулы A??i в последовательности формул, которую мы пополняем. Вторая строка - это аксиома (A5). Условия утверждения 3.45 («Если в формуле A нет свободных вхождений переменной x, то формула

? x(A?B)?(A??xB)

общезначима») в данном случае выполнены, потому что по условию x не является свободной переменной формулы A.

Следствие 3.55 (слабая теорема дедукции).

Если ?,A ? B иформула A замкнутая, то?? A?B.

Доказательство. Замкнутая формула вообще не содержит свободных переменных, поэтому любой вывод B из ?,A удовлетворяет условию теоремы 3.54.

Теорема о полноте ИП

Теорема о полноте для ИП:

В любом ИП 1-го порядка формула является тавт-ей <=> она общезначимой.

Док-во:

Покажем, что если - теорема, то она общезначима.

Проверяем непосредственно, что схемы аксиом явл. общезначимы: (A1) - (A5)

MP и G из из общезначимых формул дают общезначимые формулы => любая теорема - общезначима.

Утв.: (Гёдель)

Любой раздел математики может быть описан как теория 1-го порядка.

Пример теории 1-го порядка, аксиоматическая арифметика. Теорема Гёделя о неполноте

Пусть задана произвольная теория 1-го порядка. Если к ее алфавиту добавить предикат "равенство": P(x, y) = (по опр.) "x = y" и в число собственных аксиом ввести 2 аксиомы:

(AP1): "x (x = x)

(AP2): (x = y) à (A(x) àA(y))

при любом предикате А, то полученная теория наз. теорией 1-го порядка с равенством.

Рассмотрим МП 1-го порядка с равенством. {Это т. н. аксиоматика Пеано}

Добавим в алфавит символ const 0 - "ноль", функциональный символ ' - "штрих"

x' - это (х + 1),

и произвольный набор функциональных символов (+, *) (ф-й), и добавляем аксиомы:

1)x = y à (y = z à x = z)

2)ù (x' = 0)

)x = y à x' = y'3') x' = y' à x = y

)x + 0 = x

)x + y' à (x + y)'

)x * 0 = 0

)x * y' = x * y + x

)

для любого предиката А выполнимо:

9)[A(0) & ("x (A(x) à A(x')))] à A(x), A(0) - базис индукции, ("x (A(x) à A(x'))) - индуктивный шаг.

Эта аксиома определяет метод математической индукции.

Арифметика - основа всей математики. Она вкл. в любой раздел математики.

Теорема Гёделя о полноте:

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

Следствие:

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

2)такая аксиоматическая теория неразрешима.

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

Предварённая нормальная форма

Определение 3.68. Формула называется предварённой нормальной формой, если она имеет вид

x1Q2x2. . .QkxkA, (3.28)

где Qi? {?, ?}, а формула A не содержит кванторов. Заметим, что для предварённой нормальной формы выполняется условие разделённости переменных.

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

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

Лемма 3.70. Пусть A, B - формулы исчисления предикатов, причём B не содержит переменной x.

Тогда следующие пары формул эквивалентны

|?xAи? x-|A, -|?xAи? x-|A,??xAи? x(B?A), ?xA?Bи? x(A?B),??xAи? x(B?A), ?xA?Bи? x(A?B).

Доказательство. Эквивалентность первых двух пар формул сразу следует из эквивалентности формул A и -|-|A, так как -|?xA является сокращением для -|-|? x-|A,

а ? x-|A - сокращением для-|? x-|-|A.

Для доказательства остальных эквивалентностей рассмотрим некоторую интерпретацию с областью M.

Зафиксируем значения всех параметров формул A иB кроме x. Тогда B приобретает определённое истинностное значение.

Используем тавтологии

?x ? 1, 1?x ? x, x?0 ?-|x, x?1 ? 1.

Эквивалентность левых двух пар формул становится очевидной. Совпадение значений правых пар формул при B = 1 также очевидно. Остаётся проверить совпадение значений пары формул

-|?xAи? x-|A, -|?xA

и ? x-|A.

Это уже было сделано выше.

Альтернативные системы аксиом Система аксиом Гилберта Иакермана Связки: , ,

Больше работ по теме: