Новиков Ф.А. Дискретная математика для программистов (860615), страница 28
Текст из файла (страница 28)
Логические связкиТЕОРЕМА 1Пусть А — некоторая формула. Тогда:1) если А — тавтология, то А — противоречие, и наоборот;2) если А — противоречие, то -<А — тавтология, и наоборот;3) если А — тавтология, то неверно, что А — противоречие, но не наоборот;4) если А — противоречие, то неверно, что А — тавтология, но не наоборот;5) если -iA выполнима, то неверно, что А — тавтология;6) если А выполнима, то неверно, что А — противоречие.ДОКАЗАТЕЛЬСТВОТЕОРЕМА 2Очевидно из определений.•Если формулы А и А —> В — тавтологии, то формула В — тавто-логия.О Т противпого. Пусть 1(B) = F.
Но 1(A) = Т, так как А —тавтология. Значит, 1(А —> В) = F, что противоречит предположению о том, чтоА —> В — тавтология.•ДОКАЗАТЕЛЬСТВО4.1.4. Логическое следование и логическаяэквивалентностьГоворят, что формула В логически следует из формулы А (обозначение АВ),если формула В имеет значение Т при всех интерпретациях, при которых формула А имеет значение Т. Говорят, что формулы А и В логически эквивалентны(обозначается AВ или просто А = В), если они являются логическими следствиями друг друга. Очевидно, что логически эквивалентные формулы имеютодинаковые значения при любой интерпретации.ТЕОРЕМА 1РQ = ^ РVQ.Д Л Я доказательства достаточно проверить, что формулы действительно имеют одинаковые истинностные значения при всех интерпретациях.ДОКАЗАТЕЛЬСТВОрQFFТТFТFТP - QТТFТ->РттFFТтFТVQ146Глава 4. Логические исчисленияЕсли А, В, С — любые формулы, то имеют место следующие логические эквивалентности:ТЕОРЕМА 21.2.3.4.5.6.7.8.9.10.А V А = А, А к А = А.AVB = BV A, AkB= Bk А.А V (В V С) = (А V В) V С, А к (В к С) = (А к В) к С.А V (В к С) = (А V В) k (А V С), А & (В V С) = (А & В) V (А к С).(А к В) V А = А, (А V В) к А = А.А V F = А, А к F = F.А V Т = Т, А кТ = А.-п(-нЛ) = А.->{А & /i) = - Л V - В , -.(Л V В) =&А V -.Д = Т, А к -*А = F.ДОКАЗАТЕЛЬСТВОти.Непосредственно проверяется построением таблиц истиннос•ЗАМЕЧАНИЕТаким образом, алгебра ({T,F}; V, &,->) является булевой алгеброй, которая называетсяалгеброй высказываний.ТЕОРЕМА 3Piк .
. .к Рп = • Q тогда w только тогда, когда (Р\к...к Pn)—>Q —тавтология.ДОКАЗАТЕЛЬСТВО[ = • ] Пусть 1(Р\ к.. .к Рп) = Т. Тогда I(Q) = Т и / ( P i & . . . & P n -> Q) == Т. Пусть /(Pi к ... к Рп) = F. Тогда /(Pi & . . . к РпQ) = Т при любойинтерпретации /. Таким образом, формула Pi & .
. . &РП —• Q общезначима.[ < = ] Пусть /(Pi к ... к Рп) = Т. Тогда I(Q) = Т, иначе бы формула Pi & . . . &к Рп —> Q не была бы тавтологией. Таким образом, формула Q — логическоеследствие формулы Р\ к ... к Рп.•ТЕОРЕМА 4PI к . . .к РпQ тогда и только тогда, когда P\k...kPnk~>Q —противоречие.По предыдущей теореме Pi к . . . к Рп =>• Q тогда и толькотогда, когда формула А к ... к Рп —• Q — тавтология.
По первой теореме подраздела 4.1.3 формула Р\ к ... к РпQ является тавтологией тогда и толькотогда, когда формула -«(Pi к ... к Р„ —• Q) является противоречием. Имеем:ДОКАЗАТЕЛЬСТВО-«(PI к ... к Pn-+Q)= -(-(Pi к ...к Рп) V Q) == ---i(Pi к ... к Рп) к ^Q = Pi к ... к Рп к -yQ.•1474.2. Формальные теории4.1.5.
Подстановка и заменаПусть А — некоторая формула, в которую входит переменная х (обозначается А(... х...)) или входит некоторая подформула В (обозначается А(...В...)),и пусть С — некоторая формула. Тогда А(... х ... ){С//х] обозначает формулу,полученную из формулы А подстановкой формулы С вместо всех вхожденийпеременной х, а А(... В... ){С/В} обозначает любую формулу, полученную изформулы А подстановкой формулы С вместо некоторых (в частности, вместоодного) вхождений подформулы В.1Если формула А(... х ...) — тавтология, а В — любая формула, тоА(... х... ){В//х}—тавтология.ТЕОРЕМАДОКАЗАТЕЛЬСТВОПусть С: = А(...х...){В//х). Пусть / — интерпретация фор, мулы С (формула уже не содержит переменной х). Построим интерпретацию Vформулы А, положив х: = 1(B), а значения остальных переменных взяв такимиже, как в интерпретации I.
Тогда I'(A) = 1(C), по Г(А) = Т, следовательно,1(C) = Т.•ТЕОРЕМА 2Если А(... В ...) и В = С, a D: = А(... В ... ){С/В),то А = D.Пусть I — любая интерпретация, содержащая значения длявсех переменных в формулах А, В и С. Тогда 1(B) = 1(C), значит, 1(A) = 1(D). •ДОКАЗАТЕЛЬСТВОТеоремы 1 и 2 аналогичны правилам подстановки и замены, изложенным в разделе 3.2.3.4.2.
Формальные теорииИсторически понятие формальной теории было разработано в период интенсивных исследований в области оснований математики для формализации собственно логики и теории доказательства. Сейчас этот аппарат широко используетсяпри создании специальных исчислений для решения конкретных прикладныхзадач. Рамки книги пе позволяют привести развёрнутые примеры подобных специальных исчислений (они довольно велики), но, тем не менее, такие примерысуществуют.4.2.1. Определение формальной теорииФормальная теория 7 имеет следующие составляющие:1) множество А символов, образующих алфавит',2) множество J слов в алфавите А, 7 с А*, которые называются формулами;3) подмножество Ъ формул, Ъ с 7, которые называются аксиомами',4) множество Я отношений R на множестве формул, R е % R С 3rn+1, которыеназываются правилами вывода.Глава 4.
Логические исчисления148Множество символов Л может быть конечным или бесконечным. Обычно дляобразования символов используют конечное множество букв, к которым, еслинужно, приписываются в качестве индексов натуральные числа.Множество формул 7 обычно задается индуктивным определением, например, спомощью порождающей формальной грамматики. Как правило, это множествобесконечно. Множества Л и Э" в совокупности определяют язык, или сигнатуру,формальной теории.Множество аксиом Ъ может быть конечным или бесконечным. Если множествоаксиом бесконечно, то обычно оно задаётся с помощью конечного множествасхем аксиом и правил порождения конкретных аксиом из схемы аксиом.
Часто аксиомы делятся на два вида: логические аксиомы (общие для целого классаформальных теорий) и нелогические (или собственные) аксиомы (определяющиеспецифику и содержание конкретной теории).Множество правил вывода ft чаще всего конечно.4.2.2. ВыводимостьПусть Fi,..., F n , G — формулы теории 7, то есть F\,... ,Fn,G е 7. Если существует такое правило вывода R, R е % что (F\,..., Fn, G) G Я, то говорят, чтоформула G непосредственно выводима из формул F\,..., Fn по правилу вывода R.Обычно этот факт записывают следующим образом:F l"G'F nw-Здесь формулы Fi,..., Fn называются посылками, формула G — заключением, аR является обозначением правила вывода.ЗАМЕЧАНИЕОбозначение правила вывода справа от черты, разделяющей посылки и заключение, частоопускают, если оно ясно из контекста.Выводом формулы G из формул F i , .
. . , Fn в формальной теории 7 называется такая последовательность формул Е\,..., Ек} что Ek = G, а любая формулаEi (г < к) является либо аксиомой (Ei е Ъ), либо исходной формулой Fj (Ei == Fj), либо непосредственно выводима из ранее полученных формул Ej^,..., Ejn(ji,---,jn< i)- Если в теории Т существует вывод формулы G из формулF i , . .
. , F n , то это записывают следующим образом:F\,...,FnG.Формулы F i , . . . , Fn называются гипотезами вывода. Если теория Т подразумевается, то её обозначение обычно опускают.Если b<j G, то формула G называется теоремой теории 7 (то есть теорема — этоформула, выводимая только из аксиом, без гипотез).Если Г Ьд- G, то очевидно, что Г, A \-<j G, где Г и А — любые множества формул(то есть при добавлении лишних гипотез выводимость сохраняется).4.2. Формальные теории149ЗАМЕЧАНИЕПри изучении формальных теорий нужно различать теоремы самой формальной теориии теоремы об этой формальной теории, или метатеоремы. Это различие иногда не формализуется явно, но всегда является существенным.
В этой главе теоремы конкретнойформальной теории, как правило, записываются в виде формул, составленных из специальных знаков, а метатеоремы формулируются на естественном языке, чтобы их легчебыло отличать от теорем самой формальной теории.4.2.3. ИнтерпретацияВ этом подразделе вводится более общее и строгое определение понятия интерпретации по сравнению с подразделом 4.1.3.Интерпретацией формальной теории Т в область интерпретации М называетсяфункция I : 7 —> М, которая каждой формуле формальной теории Т однозначно сопоставляет некоторое содержательное высказывание относительно объектовмножества (алгебраической системы) М.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
