1626435694-d107b4090667f8488e7fa1ea1b3d0faa (844295), страница 44
Текст из файла (страница 44)
Для каждой конструкции, выводимой в исчислении, можно указать историю ее вывода, отправляясь от аксиом. В своем наглядном представлении эта история имеет зид дерева, терминалами которого являются аксиомы, а остальные вершины— это заключения правил вывода; при этом входные дуги такой вершины укааывают на источник посылок, а выходная дуга указывает на место использования заключения в качестве посылки следу»ощего правила. Таков дерево называется деревом вывода коцструкции в исчислении. Исчисление само по себе, однако, не наполняет выводимые в нем конструкции каким бы то ни было смыслом.
Для этого нам потребуются еще некоторые определения. «) Пусть чвтателя не смущает, что в пределах одной главы мм кспоаг зувм слова оюсылка» я «закяюченяе» как дяя аргументов кмпяикяцяи, так и дяя составных частек правила вывода. Это «девство т«рывиологвв ке сзучааио. ВСЭ ГЛ, Е, КРАТКОЕ ПОВТОРЕНИЕ МАТЕМАТИЧЕСКОЕ ЛОГККН Исчисление раекоемеьноппей алгебры логики (лечисеение Т) Аксиомы и схемы аксиом А1) )1 1, А2) ) ) Х Х АЗ) Х~/У У~/Х А4) ХЧУЧЯ ХЧ(У~/2) А5) Х~/Х ° Х , Аб) Х~/) Х Ф А7) Х~/1 Х А8) ) (Х~/У) 1 Х& ) У отрицание, двойное отрицание, коммутативность, ассоциативность, поглощение, исключенное третье, дкзъюнкция с ложным, дистрибутивность отрица- ния днстркбутивность конъюнк- ции, имплнкация, эквивалентность, А9) Хй(У~/Я) ХЛУ)/Х кс А(0) Х ~ У 1 Х Ч У А11) Х= — У (Х ~ У)й(У:э Х) А12) ()гп)р» Х вЂ” Ю'"р" Х лишние скобки левого операнда, лкшниескобки и 2 3 4 5 правого операнда, лишние скобки формулы.
А(8) Хрп(Яя — 3) Хрпй и — 1 А14) (К) гг Исчисление раыносильностей называется коррекпичмм, если 'любая выводимая в нем равносильность оказывается тождественной. Исчисление называется полным, если любая толсдественкая $звкосильность выводима в нем. Аксиомы и правила вывода полного исчисления называются 'нееаеиеиммми, если устранение любого одного из нвх делает исчисление неполным. Исчисление равносильностей. 'Геперь мы можем сказать, что 'калача построения алгебры логических формул — это задача нахождения корректного и полного исчисления равносильностей, состоящего из независимых аксиом и правил вывода. Введем для краткости еще несколько обозначений.
Назовем одночлен, конъюнкцию, дизъюнкцию, имплнкацию и формулу соответственно формулами первого (высшего), второго, третьего, четвертого и пятого приоритетов. Аналогично операции А,1/,:» и ~ получают номера приоритетов со второго по пятый. Буквы Ф" и р" означают соответственно формулу и операцию л-го приоритета. у ( зт г") — формула у, в которой выделено одно вхождение подформулы У г и-го приоритета.
У (Х) — формула, в которой выделены все вхождения переменной Х. 2 62. АЛГЕБРА ЛОГИКИ Правила вывода П1),у, „* И, <Х> — И, <Х>, уз*) правило замены переменной, у 1 <()>з)> оз <(уз)> П2а) 2 > « правило равносильной (я) \и) (я) ПОДСтаНОВКИ' П2б) 2 )> 4 Корректность данного исчисления устанавливается без труда.
Схемы аксиом А12 — А14 позволяют в преобразованиях убирать лишние скобки. Язык логических формул приемлет формулы ви- да, например, ((А )('В)) или же (А б( В) = С. У нас нет другой возможности, кроме как, введя специальные аксиомы, утвер>кдать такие очевидные ие«Блестка, как ((А')('В)) — А )/В, (А«г(В) = С вЂ” ААВжС. Формула г'з, подставляемая на место переменной Х в прави» ле П1, должна заведомо вычисляться раньше выполнения операций из У ) и (т'2, по отношению к которым Х была операндом. Для этого Рз заключается в скобки, гарантируя наивысший приоритет. При этом, естественно, могут вноситься и лишние скобки, нр это будет «замечено» аксиомами А12 и А13.
Условие на приоритеты в правиле П2 также гарантирует, что приоритет формулы, ставшей на место 9 (("), будет не больше и, так что дерево разбора формулы У з не будет испорчено. Заметим, что, создавая «инструмент» для тождественных преобразований логических формул, исчисление играет е)це одну роль, весьма важную саму по себе. Каждая аксиома, каждое правило вывода опираются па некоторое свойство формул или функций, задаваемых формуламп.
Выполняя преобразование, описываемое аксиомой илк правплом вывода, мы можем четко сознавать, каков свойство формулы нли функции использовано. 'Способность исчислений фиксировать, нли, как еще говорят, постулировать, формализовать те или иные свойства абстрактных объектов (в данном случае — булевых функций) объясняет их центральное положение в математических методах рассуждения.
По существу, каждая математическая дисциплина, базирующаяся на аксиоматическом методе, в своем строгом изложении есть не что иное, «) Мы различаем метаперемениые)т, виачекияыи которых могут быть любые формулы, и метаперемеиные бг, зиачеииями которых могут ™быть только такие формулы, которые образуют выводимые равносильности, используемые в качестве посылки правила вывода. гоз Гл. г. кРАткое повтОРение мАтемАтическОЙ ЛОГики как исчисление со своим языком конструкций, изобрал«аюших или обозначающих абстрактные объекты аксиом, постулируюших свойства объектов, и правил вывода, позволяющих строить цепочки рассуждений. Само исчисление тоже описывается в некотором метаязыке, который даже если не вводится явно, логически тем не менее в каждой математической работе присутствует. Такие свойства исчисления как корректность, полнота и независимость являются не только его, так сказать, «деловыми характеристиками», но отражают адекватность, законченность и неизбыточность теории, формализуемой данным исчислением.
Полнота исчисления равноснльностей. Продолжим рассмотрение исчисления равносильностей. Сначала покажем, что задаваемое исчислением отношение равносильности обладает стандартными свойствами отношений эквивалентности. Равносильности Р1) Р— Р— рефлексивность, Р2) .' — симметричность, «1 РЗ) ', ' ' '. ' — транзитивность. 1 Деревья вывода этих свойств показаны на рис. 6.2 (выделяемые вхождения подформул и переменных подчеркнуты).
Замегим, что деревья для правил вывода (случан б) и в)) представляют условный вывод, в котором терминалами являются не аксиомы, а равносильности или формулы, образующие посылку доказываеморо правила. На рис. 6.2, в) показан сокращенный вывод, в котором вместо поддерева вывода У'» У'1 из,Т 1 У г помещена обозначающая его «метавершина». Доказанные свойства отношения равносильности позволяют выводить целые цепочки эквивалентных преобразований. Т е о р е м а 6. Пусть Р— логическая формула, переменныв которой принадлежат множеству логических переменных (Х,... ..., Х„). Тогда выводима одна из двух равносильностей Р- К(Х„..., Х„) или где К(Х„..., Х„) — дизьюнктивная совершенная нормальная форма.
Прежде чем доказывать теорему, заметим, что в силу корректности исчисления и теоремы 5 формула К (Х1,..., Х„) находится единственным образом и нвлнется дизъюнктивной совершенной нормальной формой функции, задаваемой формулой Р. Полное доказательство теоремы 6 слишком громоздко, и мы лишь наметим этапы преобразования Р в К, сопроводив нх при- ь Е Ь АЛГЕБРА ЛОГИКИ мером.
В примере мы используем более компактные обозначения для конъюнкции (Х2Х2 — без анака операции) и для отрицания (Х). Пусть г = (Хг = Ха~/Ха). Сначала г' приводится к форме, содержащей только переменные, дизъюнкции, конъюнкции и отрицания. Эквивалентность тг-Г а) 'рт-$ в), '~т мт 4 Рвс. 6.2. Деревья вывода в всчвслекия равкосвльиостей. а) Р1г рефлексивкость.
б) Р2: сммметрвчвость. в) РЗ: тракзятмвкость (под- черкнуть выделяемые вхождеввв формул и перемеивмх). устраняется по А11, импликация — по А10, константа 1 — с по- мощью А1 и А7. Хь — Ха)/Ха (Ха~ Ха'г/Хф(Хагг/Ха-з Х,) — ( ) ХЯ(Ха)/Ха))() (Ха)/Ха))/Хт)— По аксиоме А8 отрицание, стоящее перед скобками, распределяется по слагаемым дизъюнкции. Если в скобках — конъюнкция, она также по А8 заменяется на дизъюнкцию.
Двойные отрицания убираются по А2: - (Х,~/Ха~/Ха)(Х2Ха~/Х,)— После этого раскрываются все скобки по А9. При этом используются свойства конъюнкции ХХ Х и ХХ 1, которые получаются из Аб и Аб с помощью А8 и А2. Если все конъюнкции (а5) ~45) ХРХ-Х ХРХ-)( Чгг г" ~г ~г гтт П2 лдс Гл. в. кРАткОе повтОРение'мАтемАтическои логики окажутся равными т, мы получим равносильность Р д: Х Х Х ~/Х Х ~/Х Х, Для совершенной формы нужно, чтобы все конъюнкции состояли из всех переменных Х„..., Х„. Всюду, где это нужно, дополнительные переменныевводятсядомножением конъюнкций на тождественно истинную дизъюнкцию (Х~/Х). При этом используется свойство конъюнкции Х$ Х (из А7): -ХдХзХв~~ Х,Х,(Х,~Х,))~Х,(Х,~~Х,)Х,— -Х„Х,Х,)(Х,ХдХ,УХ,Х,Х,УХ,Х,Х,)(Х,Х,Х, «Приведя подобныеэ по А5 и упорядочив конъюнкции лексико- графически с помощью АЗ, получим дизъюнктивную нормальную совершенную форму — ХдХдХв)/ ХдХдХД ХдХдХД ХдХдХв.~у гу Те р е м а 7.
Исчисление равносильностсй полно. Действительно, пусть Рд и Рд — эквивалентные формулы. Это значит, что они задают одну и ту яде булеву функцию В этом случае по теореме 6 имеют место две выводимые равносильности Р К, Р, К, где К вЂ” или д или совершенная нормальная форма функции 1. В силу симметричности и траизитивности отношения равносильности немедленно получаем, что Р Р .Тттт й С.З. вдсчисление высказываний Общезначимые формулы.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
