Игошин Математическая логика и теория алгоритмов (1019110), страница 30
Текст из файла (страница 30)
Пусть у больного выявлены симптомы Юн Яъ 5п а общее число симптомов, задействованных в нашем анализе, пять: 5н Яп Я,, Х4, 5,. Тогда число строк, представляющих интерес в данном случае, равно четырем. Предположим, что эти строки таковы (для простоты примем, что исследуются три заболевания: Т„Т,, Т, и им соответствуют три переменные: ун у,, уз): Анализ выделенных строк показывает, что во всех строках, соответствующих симптомам больного, есть заболевание у, (точнее, Т~) и нет заболевания у, (точнее, Т,), а заболевание уз (т.е. Тз) в одних строках есть, а в других нет. Из этого можно сделать вывод, что у больного нет заболевания Т„но он определенно страдает заболеванием Ть Относительно заболевания Т~ требуются дополнительные исследования.
Для этого нужно увеличить число анализируемых симптомов, выявить дополнительные указания Ге На практике число столбцов и строк построенной таблицы может оказаться столь большим, что ее анализ будет под силу лишь компьютеру. Распознавание образов. Нетрудно видеть, что в самых общих чертах ситуация, рассмотренная в предыдущем пункте, может быть охарактеризована следующим образом. Имеется некоторое множество скрытых причин (болезней) и множество наблюдаемых следствий (симптомов). Кроме того, имеются высказывания, связывающие причины и следствия.
Требуется, опираясь на эти высказывания, по предъявляемому набору следствий (симптомов, 120 наблюдаемых у данного пациента) определить возможные причины, их породившие (болезни пациента). Во второй половине ХХ в. сформировалась область прикладной математики, занимающаяся решением подобных проблем. Она получила название теория распознавания образов. В предыдущем пункте показано, как распознавать «образ болезни», но подобная ситуация встречается весьма часто и вдругих областях науки.
В ге оп о г и и, например, причины труднодоступны, так как это — залегающие на разных глубинах полезные ископаемые. Но следствия сравнительно легко наблюдаемы: это — сопутствующие минералы, выходящие на поверхность, окраска почвы, характер растительности, данные сейсморазведки, аэро- и космической фотосъемки и т.п. В химии скрытые причины — это качественный состав и строение вещества, а наблюдаемые следствия — ответы в тестовых реакциях: помутнение, окраска, запах, выделение теплоты и т.п. В б и о л ог и и: малодоступные гены контролируют легко наблюдаемые признаки.
В кр им и н ал и с тике: скрывшийся преступник оставляет следы, улики, показания свидетелей. В разных науках такое «распознавание образов» называется поразному; лля рассмотренных это — диагностика, геологическая разведка, анализ, раскрытие преступления и т.д. С точки зрения математики здесь решается одна задача, сформулированная как «распознавание образов». Решать ее в самой общей постановке и призвана математическая теория распознавания образов. Один из методов ее решения опирается на теорию булевых функций, которая позволяет в определенном смысле автоматизировать процесс решения, используя для этой цели ЭВМ. Глава 111 ФОРМАЛИЗОВАННОЕ ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ В этой главе рассматривается аксиоматический подход к алгебре высказываний, т.е. такой же подход, какой используется при строгом построении геометрии на базе какой-либо системы аксиом, например систем Гильберта, Вейля и т.д.
Алгебра высказываний предстанет как аксиоматическая теория, в определенном смысле достигнет наивысшей степени строгости изложения и совершенства. Общим вопросам аксиоматических теорий посвящены гл. Ч и Ч1, так что формализованное исчисление высказываний, которое строится в настоящей главе, будет служить примером аксиоматической теории. Применительно к алгебре высказываний аксиоматический подход состоит в следующем. Из всех формул алгебры высказываний выделяется некоторая часть.
Формулы из этой части обьявляются аксиомами. Определяется некоторое правило, по которому из одних формул можно получать новые. Аксиомы выделяются, а правило определяется так, что по нему из аксиом могут быть получены все тавтологии алгебры высказываний, и только они. Таким образом, тавтологии алгебры высказываний оказываются теоремами аксиоматической теории, в результате получаем аксиоматическое построение алгебры высказываний. В качестве системы аксиом могут быть выбраны разные части совокупности всех формул алгебры высказываний. То же относится к правилам получения новых формул.
В зависимости от выбора получаются различные аксиоматизации алгебры высказываний. Общим для них является то, что все они обладают одним и тем же множеством теорем — это совокупность всех тавтологий алгебры высказываний. Мы рассмотрим лишь одну из возможных аксиоматизаций.
й 15. Система аксиом и теория формального вывода В настоящем параграфе будет заложена основа аксиоматической теории высказываний, определены понятия доказательства и теоремы, рассмотрены примеры доказательств теорем и развита теория формального вывода. 122 Начала аксиоматической теории высказываний: первоначальные понятия, система аксиом, правило вывода. К первоначальным, яеопределяемым лоня»лиям аксиоматической теории высказываний относятся следующие: Х„Х,, ..., Մ— пропозициональные переменные; —, — » — логические связки; (,) — технические знаки. Первоначальным понятием является также понятие формулы, которое определяется (как и в алгебре высказываний, см.
определение 2.1) инлуктивным образом: 1) каждая пропозициональная переменная есть формула; 2) если Г~ и Г, — формулы, то выражения -Г„(Г, — » Гг) также являются формулами; 3) никаких других формул, кроме получающихся согласно пунктам 1 и 2 нет. Следующий шаг в построении аксиоматической теории высказываний состоит в выборе системы аксиом. В качестве аксиом выбираются формулы следующих видов: (А!): (à — » (б — » Г)); (А2): (Г-+ (б — » Н)) -» ((Г-+ 6) -+ (Г-+ Н)); (АЗ): ((- 6 — » -Г) -+ ((- 6 -+ Г) -+ 6)), где Г, 6, Н вЂ” произвольные формулы. Таким образом, каждое из выражений (А1), (А2), (АЗ) задает лишь форму аксиомы.
Они превращаются в аксиомы, если вместо Г, 6 и Н подставить конкретные формулы (в частности, пропозициональные переменные). Следовательно, каждое из этих выражений задает бесконечное множество формул. Все они называются аксиомами. Поэтому каждое из выражений (А1), (А2), (АЗ) называют схемой аксиом. Наконец, заключительный шаг, закладывающий основу аксиоматической теории высказываний, состоит в выборе правил вывода. Единственным правилом вывода будет служить правило заключения (или отделения, или тоНия ролелл, или сокращенно МР): из формул Ги à — » 6 непосредственно следует формула б.
Как и в алгебре высказываний, внешние скобки у формулы принято не писать. Поскольку в аксиомах не участвуют связки л, ы, <-ь, то их придется определить. Введем следующие определения: (Г л 6) означает — (Г -» —,6); (Г»~ 6) означает (- à — » 6); (Г+-» 6) означает ((Г-+ 6) л (6-+ Г)). Смысл, например, первого из определений состоит в том, что, каковы бы ни были формулы Г и 6, формула (Г л 6) служит обозначением для формулы — (à — » — 6).
Понятие вывода и его свойства. Заложив основу будущей аксиоматической теории в виде системы аксиом и правила вывода, !23 приступим к ее развитию, т.е. к доказательству теорем. Прежде всего уточним понятия доказательства и теоремы. Определение 15.1. Доказательством или выводом формулы Р из множества формул Г называется такая конечная последовательность В„Вн ..., В, формул, каждая формула которой является либо аксиомой, либо формулой из Г, либо получена из двух предыдуших формул этой последовательности по правилу МР, а последняя формула В, совпадает с г" (В, и с). Если имеется вывод формулы с из множества Г, то говорят, что Р выводима из Г или что Г выводит Р, и пишут Г ь- Р. Элементы из Г называются гипотезами или посылками вывода.
Если же имеется вывод формулы Р из пустого множества гипотез, то говорят, что с" выводима из аксиом (или что с доказуема), а последовательность Вь Вн ..., В, называется доказательством этой формулы. Саму с называют теоремой, и пишут ь- с". Таким образом, запись ь- с служит сокращением утверждения «Ресть теорема». Если множество Г конечно: Г = (Рь Рь ..., Р ), то вместо (Рь У;, ..., с" ) ь- 6 будем писать Рь Рн ..., Р ь- 6. Совокупность аксиом, правил вывода и всех теорем, выводимых из аксиом, и представляет собой аксиоматическую теорию высказываний (или формализованное исчисление высказываний). Наша ближайшая цель состоит в том, чтобы научиться доказывать теоремы в данной теории, т.е. научиться строить выводы формул из аксиом.
Приведем пример доказательства какой-нибудь формулы. Пример 15.2. Доказать: ь- Р-» с". Для доказательства того, что формула с -+ Рявляется теоремой формализованного исчисления высказываний, нужно построить вывод (доказательство) этой формулы из аксиом. Таким выводом является, например, следующая последовательность формул: (1): (г" -» ((с -» с ) -+ г )) -+ ((Р -» (с -» Р)) -+ (Р— > Р)); (2): с -» ((с — » с ) — » с ); (3): (Р— » (Р -» с )) -+ (с — » Р); (4): с -» (Р— » с ); (5): с -» с.