Введение в логику высказываний

2 Лекция №1 ВВЕДЕНИЕ В ЛОГИКУ ВЫСКАЗЫВАНИЙ 2.1 Ключевые (основные) вопросы (моменты) — краткий экскурс в историю логики высказываний; — логика и исчисление высказываний; 2.2 Текст лекции 2.2.1 Краткий экскурс в историю логики высказываний Логика – это наука о формализации мышления, задачей которой является изучение формальных законов построения и вывода суждений и доказательств. Логика использует формальный язык для описания и анализа суждений, формального доказательства утверждений. Логика исследует формальные схемы рассуждений, верные в силу одной их формы, независимо от содержания, что есть результат применения операции абстрагирования к рассуждениям естественного языка. Современная парадигма научного исследования состоит в том, что формальное изучение любой проблемы начинается с замены реальных объектов их абстрактными представлениями, выбираемыми таким образом, чтобы в этих идеализациях были отражены именно те свойства исходных объектов, которые мы хотим изучать. Логика известна человечеству с древних времён и представляет собой искусство правильно рассуждать. Термин “логика” происходит от греч. ”logos”, что означает: слово, понятие, рассуждение. Вообще говоря, способность к рассуждениям – это именно искусство. Имея в распоряжении какие-либо утверждения, истинность которых проверена, к примеру, экспериментально, логик может через умозрительные построения прийти к другому утверждению. Оно, в свою очередь, при искусстве правильно рассуждать, также оказывается истинным (но, вполне возможно, не во всех случаях). Существует логика формальная, логика диалектическая, логика исследования и др. Данное учебное пособие посвящено формальной, а именно математической логике. Первые учения о формах и способах рассуждений возникли в странах Древнего Востока: (Китай, Индия), но в основе современной логики лежат учения созданные в 4 веке до нашей эры древнегреческими мыслителями (главным образом Аристотелем). Аристотелю принадлежит исторически первое отделение логической формы речи от её содержания. Он, в частности, открыл атрибутивную форму высказывания как утверждения или отрицания «чего-то о чем-то» и определил простое суждение (т.е. высказывание) как атрибутивное отношение двух терминов. Он также описал основные виды атрибутивных суждений и правильных способов их обращения. Аристотель рассмотрел конкретные виды рассуждений, которые назвал силлогизмами. Более конкретно, он рассмотрел так называемые категорические утверждения следующих четырех видов: • все А обладают свойством В (все А суть В); • некоторые А обладают свойством В (некоторые А суть В); • все А не обладают свойством В (все А суть не В); • некоторые А не обладают свойством В (некоторые А суть не В). В начале 17 века Г. Галилей вводит в научный обиход понятие о гипотетико-дедуктивном методе: он восстанавливает права абстракции, обосновывает потребность в абстракциях, которые «восполняли» бы данные опытных наблюдений. Он указывает на необходимость введения этих абстракций в систему логических функций в качестве гипотез, с последующим сравнением результатов дедукции с результатами наблюдений. Главным идейным противником применения математических методов к системе логических понятий был психологизм в логике. Психологизм в логике воспринимал математизацию логики как своего рода возрождение схоластики, которое менее всего было способно поставить логические исследования на научный фундамент. Борьба за математизацию логики и привела к мощному развитию этой науки. Начиная с 1930-х годов, закладываются основы т. н. «машинного мышления» – теории алгоритмов. Её выдающиеся деятели: К. Гедель, С. Клини, А. Тьюринг, А. Черч, Э. Пост, А. Марков, А. Колмогоров и др. И хотя была выяснена ограниченность такого мышления, что проявилось в установлении алгоритмической неразрешимости ряда логических проблем (знаменитая теорема Геделя о неполноте символических логик и обоснование алгоритмически неразрешимых задач), все же существенно вырос спрос на применение логики в вычислительной математике и технической кибернетике. На сегодняшний день в многообразии логических теорий выражаются требования, предъявляемые логике современной наукой и практикой. Важнейшим из них является требование в содействии точной постановке и формулировке научно-технических задач и разысканию возможных путей их разрешения. Предлагая строгие методы анализа определенных аспектов рассуждений, логические теории одновременно содействуют и объективному анализу положения вещей в той области знания, которая находит отражение в соответствующих мыслительных процессах. 2.2.2 Логика и исчисление высказываний Элементами логических рассуждений являются утверждения, которые либо истинны, либо ложны, но не то и другое вместе. Такие утверждения называются высказываниями (простыми). Простые высказывания обозначаются пропозициональными переменными, принимающими истинностные значения «И» и «Л». Из простых высказываний с помощью логических связок могут быть построены составные высказывания. Обычно рассматривают следующие логические связки: • отрицание (читается “НЕ”, обозначается “”), • конъюнкция (читается “И”, обозначается “&”), • дизъюнкция (читается “ИЛИ”, обозначается “V”), • импликация (читается “ЕСЛИ… ТО, обозначается “”). Примечательно, что тождества алгебры множеств могут быть переведены на язык математической логики и обратно – таблица 1: Логическая терминология Язык теории множеств “A или B” A+B “A и B” AB “Не A” A’ “Ни A, ни B” (A+B)’, или, что то же, A’B’ “Не сразу A и B” (AB)’, или, что то же, A’+B’ “Если A, то B”, AB “Какое-то A есть B” AB “Никакое A не есть B” AB= “Какое-то A не есть B” AB’ “Нет никакого A” A= Таблица 1 Соответствие языка теории множеств и математической логики Кроме того, в терминах теории множеств силлогизм “если всякое A есть B и всякое B есть C, то всякое A есть C”, принимает простой вид: если AB и BC, то AC. Аналогично “закон противоречия”, утверждающий, что “объект не может одновременно обладать и не обладать некоторым свойством, записывается в виде: AA’=, и “принцип исключённого третьего”, говорящий, что “объект должен или обладать, или не обладать некоторым свойством”, записывается как : A+A’=U. Правильно построенные составные высказывания называются формулами (пропозициональными). Формулы имеют следующий синтаксис: • <формула > :: = И | Л | • <пропозиц. переменная > | ( <формула>) | • (<формула>&<формула>)| • (<формула>V<формула>)| • (<формула> <формула>| Истинностное значение формулы определяется через истинностные значения ("И" или "Л") её составляющих, в соответствии с таблицей 2: A B A A & B A V B A B Л Л И Л Л И Л И И Л И И И Л Л Л И Л И И Л И И И Таблица 2 Истинностные значения логических формул В логике высказываний вводится понятие вывода для формул: если некоторые формулы принять априори истинными (“аксиомы”), то на их основе можно по следующим правилам (“правилам вывода”) ввести дальнейшие формулы как истинные (“доказать”). Эта связь между формулами выражается специальным знаком ├, называемым символом вывода. Говорят, что формула А выводима из множества Н формул, и записывают: Н ├ А. Если А выводима из пустого множества, то это выражается через ├ А. Определение 1. Конкретный набор истинностных значений, приписанных переменным x1,.., xn, называется интерпретацией формулы А. Формула может быть истинной (иметь значение И) при одной интерпретации и ложной (иметь значение Л) при другой. Значение формулы А в интерпретации И будем обозначать I(А). Определение 2. Формула, истинная при некоторой интерпретации, называется выполнимой. Определение 3. Формула, истинная при всех возможных интерпретациях, называется общезначимой (или тавтологией). Определение 4. Формула, ложная при всех возможных интерпретациях, называется невыполнимой (или противоречием). 3 Лекция №2 ВВЕДЕНИЕ В ЛОГИКУ ВЫСКАЗЫВАНИЙ 3.1 Ключевые (основные) вопросы (моменты) — классическое определение исчисления высказываний; — конструктивное определение исчисления высказываний. 3.2 Текст лекции 3.2.1 Классическое определение исчисления высказываний Исчисление высказываний – это формальная теория L, в которой определены следующие компоненты: 1. Алфавит: • и  есть связки • ( , ) есть служебные символы; • а, в,…, а1, в1 ,… есть пропозициональные переменные. 2. Формулы: • переменные суть формулы; • если А, В есть формулы, то ( А) и (АВ) есть формулы. 3. Аксиомы: • А1: (А(ВА)); • А2: ((А(ВС))((АВ)(АС))); • А3: ((В  А)((ВА)В)). 4. Правило: Modus ponens (правило отделения). Здесь А и В – любые формулы. Таким образом, множество аксиом теории L бесконечно, хотя задано 3-мя схемами аксиом. Множество правил вывода также бесконечно, хотя оно задано только одной схемой. При записи формул лишние скобки опускаются, если это не вызывает недоразумений. Другие связки вводятся определениями (но не аксиомами): • А&В:=(АВ), • АVВ:=АВ. Любая формула, содержащая эти связки, рассматривается как синтаксическое сокращение собственной формулы теории L. 3.2.2 Конструктивное определение исчисления высказываний. Алфавит и множество формул те же, что и в подразделе 2.3,аксиомы представляют собой следующие три формулы: • А1: (а(ва)); • А1: ((а(вс))((ав)(ас))): • А1: ((в а)((ва)в)). Правила вывода таковы: Правило подстановки: если формула В является частным случаем формулы А, то В непосредственно выводима из А. Правило Modus ponens (что означает «правило отделения»): если набор формул А, В, С является частным случаем набора формул а, ав, в, то формула С является непосредственно выводимой из формул А и В. Примечание: здесь а, ав, в – это три конкретные формулы, построенные с помощью переменных а, в и связки . Для вывода формул из заданного множества аксиом применяются следующие правила заключения или правила вывода (справедливые для любых формул А, В, С). • ├ А V  А (Tertium non datur); • {В,  ВVВ}├ C (Modus ponens); • Если В = С есть применение правила семантической эквивалентности, булевской алгебры или булевского терма, то также справедливо {В}├ С (применение закона равенства). Отступление: а) Принцип Termium non datur означает т. н. принцип исключенного третьего. Чтобы обосновать этот принцип, в качестве терма допускают только такие термы, для которых на основании их внешнего вида обеспечивается, что они при интерпретации обладают значениями «Истина» и «Ложь», но не значением ┴ («дно», что символизирует отсутствующий результат незавершающегося вычисления). б) Modus ponens’у (см. правило 4 подраздела 2.3) соответствует правило заключения {xy, x}├ y. Заданная система правил вывода существенным образом применяет законы равенства булевской алгебры. Классически, в логике высказываний применяют другую систему вывода, в которой задается не закон равенства для высказываний, а специальные правила вывода для отдельных булевских операторов. Определение 1 Пусть Н – множество формул; тогда формулу А называют непосредственно выводимой из Н, в этом случае пишут: Н├А, если А выводима из Н с помощью одного из правил вывода, т. е. существуют формулы А1…Аn H и справедливо, что {A1,…, Аn}├ A,что соответствует одному из правил (1-3). Тем самым понятие выводимости монотонно в следующем смысле: если Н1 Н2 и имеет место Н1├ А1, то справедливо Н2├ А. Часто используется также запись (А1…Аn)/A вместо {А1,…, Аn} ├ А. Определение 2 Если Н – множество формул и задана последовательность непосредственных выводов вида: Н├ А1, Н {А1}├ А2, Н  {t1,..., tn}├ An+1, то А1,…, Аn+1 называют выводом над H, а высказывание Аn+1 –выводимым из H (для чего также пишут Н├ An+1). Из заданного множества высказываний Н могут быть выведены дальнейшие высказывания с помощью вышеприведенных правил вывода. Выводимые высказывания могут снова использоваться для вывода последующих высказываний. Лемма 1 (Взаимосвязь между импликацией и выводимостью). Если имеет место Н├ А1  А2, то справедливо также Н {A1}├ A2. Понятие вывода формализует концепцию математических доказательств. Из заданного множества Н высказываний, которые принимаются за истинные, т. е. аксиом, выводятся дальнейшие высказывания по точно установленным правилам вывода. Определение 3 Множество Н аксиом вместе с множеством правил вывода называется формальной системой или теорией, а выводимые формулы называются теоремами. Теория является противоречивой, если каждая формула является выводимой. Теорема 1 (о противоречивости каждой теории логики высказываний для любого множества аксиом, которые содержат false). Если в теории логики высказываний false выводимо, то выводимо любое высказывание А, т. е. Справедливо {false} ├ A для любой формулы А. Теорема 2 (о корректности выводов). Каждое (из пустого множества аксиом) выводимое высказывание А со свободными идентификаторами x1, …., xn типа bool (где n N) для любой конкретизации И либо Л для Х1, …., Хn даёт значение И. Теорема 3 (о полноте логики высказываний без атомарных высказываний). Если формула логики высказываний А, которая не содержит никаких элементарных атомарных высказываний, со свободными идентификаторами х1,..., хn типа bool для каждой подстановки вместо х1,…, хn значений истинности определяет значение И («истина» ), то формула А выводима. Идея доказательства. Можно показать, что формула А только тогда определяет значение И для всех конкретизаций В, когда А сводима к true. 4 Лекция №3 ИСЧИСЛЕНИЕ ПРЕДИКАТОВ 4.1 Ключевые (основные) вопросы (моменты) — логика и исчисление предикатов; — правила вывода в логике предикатов первого порядка; — метод резолюции для логики предикатов первого порядка; 4.2 Текст лекции 4.2.1 Логика и исчисление предикатов Рассмотренное ранее исчисление высказываний не всегда позволяет выразить многие факты и суждения, в том числе используемые в повседневной жизни. В целях обобщения указанного исчисления в его предложения обычно вводят параметры. Дадим объекту дальнейшего обсуждения, а именно исчислению предикатов, нестрогое определение и проанализируем некоторые предложения. Определение 1 (нестрогое). Предикат – это функция одного либо нескольких аргументов с булевскими значениями истина и ложь. Рассмотрим следующие два предложения: 1) “Все комплектующие, которые выпускает фирма IBM, стоят менее 100 долларов”; 2) “Фирма IBM выпускает винчестеры”. Отсюда нужно вывести, что винчестеры фирмы IBM стоят менее 100 долларов. Однако пока этого нельзя сделать, поскольку текст второго предложения не входит непосредственно в первое, даже если попытаться чуть изменить словесные формулировки. Попробуем применить исчисление предикатов. Введём в предложения параметры, поместив их в скобках в качестве аргументов (по аналогии с обычной записью для функций). Получим следующее: IBM_ выпускает (HardDisc) стоит_менее (HardDisc, 100) IBM_ выпускает (HardDisc). Здесь “IBM_ выпускает“ и “стоит_менее” – предикаты. При этом следует отметить, что, например, утверждение IBM_ выпускает (Cofe) имеет значение ложь, и так же ложное значение имеет стоит_менее (HardDisc, 0). Поскольку номенклатура выпускаемых фирмой IBM изделий не ограничивается винчестерами, смысл полученной записи из двух утверждений относительно HardDisc должен быть расширен, что может быть проделано при помощи кванторов. Введём переменную x и квантор общности , тогда получим всего одно утверждение x IBM_ выпускает (x) стоит_менее (x, 100). Поскольку в полученное утверждение входит квантор общности, означающий “для всех”, “для каждого”, то при формальном прочтении оно звучит так: “Для каждого x, если IBM поставляет x, этот x стоит менее 100 долларов.” Квантор существования применяется, когда нужно показать, что существует хотя бы одно значение переменной, для которой истинно данное утверждение. При использовании обоих упомянутых кванторов и введения ещё одной переменной y предыдущее утверждение запишется в виде x IBM_ выпускает (x) y (стоит (x, y) менее (y, 100)), что означает: “Для любого x, если IBM поставляет x, обязательно найдётся y, такой, что x стоит y долларов и y менее 100”. Итак, сформулируем строгое определение: Определение 2 (строгое). Предикатом называется отображение прямого произведения заданных множеств в множество значений истинности P: {И, Л}, где M1, M2,.., Mn – заданные множества, И, Л – символы для обозначения соответственно истины и лжи. Характерно, что в классической логике предикатов рассматривают только такие элементарные высказывания, которые обладают значениями либо “Л”, либо “И”, но не каким-то третьим значением. Определение 3 Исчисление предикатов (первого порядка) – это формальная теория К, в которой определены следующие компоненты: 1. Алфавит: • связки основные – ,  • дополнительные  , V • служебные символы ( , ) • кванторы всеобщности  • существования  • предметные константы a, b...a1, b1,… • переменные x, y…x1, y1… • предикаты P, Q,… • функторы f, g,… C каждым предикатом и функтором связано некоторое натуральное число, которое называется арностью или местностью. 2. Формулы имеют следующий синтаксис: • <формула>:: = <атом> • <формула> • (<формула><формула>) • <переменная><формула> • <переменная><формула> • <атом>::=<предикат>(<список термов>) • <список термов>::=<терм><терм>,<список термов> • <терм>::=<константа> • <переменная> • <функтор>(<список термов>) При этом должны быть выполнены следующие условия: • функтор f в терме должен быть n-местным; • предикат p в формуле также должен быть n-местным. Формулы вида A и A, называются литеральными формулами (или литералами). В формулах  x A и  x A подформула A называется областью действия квантора по x. Обычно связки и кванторы упорядочивают по приоритету следующим образом: , , , , V, . Лишние скобки при этом отсутствуют. Исчисление предикатов, которое не содержит предметных констант, функторов, предикатов и собственных аксиом, называется чистым. Исчисление предикатов, которые содержат предметные константы и/или функторы и/или предикаты и связывающие их собственные аксиомы, называются прикладными. Исчисление предикатов, в котором кванторы могут связывать только предметные переменные, но не могут связывать функторы или предикаты, называется исчислением первого порядка. Исчисления, в которых кванторы могут связывать не только предметные переменные, но и функторы, предикаты или иные множества объектов, называются исчислениями высшего порядка. Все операции над значениями истинности можно обобщить до операций над множествами предикатов над заданным множеством M. Если имеется предикат p над множеством M, то имеется непосредственная возможность превратить p в элементарное высказывание, задаваемое с помощью такой формы высказывания: “Для всех xM справедливо p(x)” или “По крайней мере, для одного xM справедливо p(x)”. Если первое из этих высказываний истинно, то предикат p называется общезначимым; если справедливо второе высказывание, то предикат p называется выполнимым. Пусть t – есть формула с идентификаторами из семейства множеств идентификаторов X и пусть m – есть тип носителя М, который является множеством возможных значений для идентификатора xM, тогда: квантор  можно выразить через отрицание с помощью квантора , и наоборот: ( m x : t)=( m x : t), ( m x : t)=(  m x : t). 4.2.2 Правила вывода в логике предикатов первого порядка Идентификаторы, такие как x в формуле логики предикатов  m x : t, называются связанными. Связанные идентификаторы могут быть переименованы без изменения терма логики предикатов. Имеет место следующий закон переименования: ( m x : t )= m y : (t[y/x]) – если y не входит в t как свободный идентификатор, ( m x : t) =  m y : (t[y/x]) – если y не входит в t как свободный идентификатор. Это означает, что формулы, получающиеся из других формул логики предикатов путем переименования связанных идентификаторов, семантически эквивалентны. Правила подстановки для кванторизованных термов логики предикатов достаточно сложны. Подстановка в таком терме с кванторами описываются следующими равенствами, при условии если x и y – различные идентификаторы и x не является свободным в t`: ( m x : t)[t`/x]=  m x : t, ( m x : t)[t`/y]=  m x : (t[t`/y]) Если же x – свободный идентификатор в t`, то перед подстановкой связанного идентификатора  m x : t с помощью приведенных выше законов переименования его необходимо переименовать, чтобы могла быть сделана подстановка ( m x : t)[t`/y]. Справедливо следующее: “И”, если для всех  () : IB[/x][t] = “И”, IB[ m x : t] = “Л”, в противном случае. “И”, если для всех  () : IB[/x][t] = “И”, IB [ m x :t] = “Л”, в противном случае. Теорема 1 (первая теорема Гёделя о неполноте). Во всякой достаточно богатой теории 1-ого порядка существует такая истинная формула F, что ни F, ни F не являются выводимыми в этой теории. Теорема 2 (вторая теорема Гёделя о неполноте). Во всякой достаточно богатой теории первого порядка формула F, утверждающая непротиворечивость этой теории, не является выводимой в ней. Примечание. Вполне возможно, что непротиворечивость одной конкретной теории может быть установлена средствами другой, более мощной формальной теории. Но тогда возникает вопрос о непротиворечивости этой второй теории и т. д. 4.2.3 Метод резолюции для логики предикатов первого порядка Метод (принцип) резолюций был предложен Ж. Эрбраном в 1930 г., а впервые реализован на ЭВМ Дж. Робинсоном в 1963 г. В основе так называемого метода резолюций лежит идея «доказательства от противного». Используемые в методе резолюций так называемые резольвенты представляют собой вершины дерева вывода, соответствующие выводимым дизъюнктам. Определение 4 Резолютивный вывод Ф из множества дизъюнктов S есть такая конечная последовательность Ф1,…, Фk дизъюнктов, что Фk=Ф и каждый дизъюнкт Фi или принадлежит S, или является резольвентой дизъюнктов, предшествующих Фi. Определение 5 Универсальным замыканием формулы Ф (x1,…, xn) называется предложение x1…xn Ф (x1,…, xn). Теорема 3 (о полноте метода резолюций). Если S – множество дизъюнктов, то множество универсальных замыканий формул из S невыполнимо тогда и только тогда, когда существует резолютивный вывод 0 из S. В качестве противоречия F при доказательстве от противного по методу резолюций может быть использована пустая формула, обозначаемая . Пустая формула по определению является противоречием, не имеет никакого значения и ни в какой интерпретации не является истинной. Рассмотрим метод резолюций применительно к исчислению предикатов. Пусть C1 и C2 два предложения в исчислении предикатов. Правило вывода называется методом резолюций в исчислении предикатов, если в предложениях C1 и C2 унифицируемые литералы P1 и P2, т. е. C1=P1VC`1 и C2=P2VC`2. В указанной форме записи метода резолюций предложения C1 и C2 являются резольвируемыми, а предложение , полученное из предложения применением унификатора , резольвентой. Метод резолюций служит основой языков логического программирования, главным отличием которых от так называемых “процедурных” языков является то, что программа не указывает, как что-либо следует делать для решения задачи, а описывает некоторые элементы и связи между ними и ставит конкретную цель. При этом компьютер самостоятельно ищет стратегию для решения поставленных вопросов. Сформулируем основные положения метода резолюций. 1. Модель исследуемого “мира” представляется множеством аксиом, которые преобразуются в множество дизъюнктов S. 2. Для доказательства справедливости теорем в данном “мире” необходимо взять её отрицание и, преобразовав в форму дизъюнкнта, добавить к множеству S. Если теорема верна, то новое множество дизъюнктов должно быть противоречиво. 3. Доказательство противоречивости сводится к доказательству того, что из данного множества дизъюнктов может быть выведен пустой дизъюнкт. 4. В техническом аспекте метод резолюций состоит из унификаций и получения множества резольвент до тех пор, пока не будет получена пустая резольвента. 5. Для уменьшения числа резольвент (и следовательно, для повышения эффективности вывода) очень существенна стратегия вывода. 6. Если множество дизъюнктов S противоречиво, то пустой дизъюнкт будет найден за конечное число шагов. При непротиворечивости множества дизъюнктов S процесс установления факта непротиворечивости может быть бесконечным. 5 Лекция №4 ОСНОВНЫЕ ПОНЯТИЯ МОДАЛЬНОЙ ЛОГИКИ 5.1 Ключевые (основные) вопросы (моменты) — основные понятия модальной логики; — синтаксис и семантика модальной логики; 5.2 Текст лекции 5.2.1 Основные понятия модальной логики Рассмотренные нами ранее суждения классической логики (как простые, так и сложные) подразумевали лишь факт их истинности либо ложности. Для моделирования многих технических задач такой формализм является неприемлемым. Поэтому были введены неклассические логики, включающие в себя так называемые модальные логики, которые подразделяются на временную, динамическую и другие логики. Название “модальная логика” связано с тем, что в модальные логические системы входят такие операторы над логическими формулами, которые позволяют модифицировать их интерпретацию. Определение 1 Модальная логика – это область логики, посвящённая изучению модальностей, построению исчислений, в которых модальности применяются к высказываниям, наряду с логическими операциями, и сравнительному исследованию таких исчислений. Модальные операции, такие как, ‘‘возможно’’, “необходимо”, и другие, могут относиться как к высказываниям или предикатам, так и к словам, выражающим какие-либо действия или поступки. В системах модальной логики, для которых справедливы принцип исключённого третьего и закон снятия двойного отрицания   , для операторов возможности  и необходимости  справедливы соотношения двойственности: • А  А • А    А, вполне аналогичные законам де Моргана алгебры логики: • (АB) (  А& B) • (А&B) (  А  B). Эта аналогичность сохраняется также для соответствующих соотношений логики предикатов для кванторов, связывающих операторы возможности  и необходимости  с отрицанием , а именно: ◦ А  А ◦ А    А. В аксиоматических системах модальной логики в качестве исходной обычно вводят одну модальную операцию (используя какую-либо из этих эквивалентностей в качестве определения другой операции). Аналогично вводятся и другие модальные операции (не входящие в число логических операций и не выражаемых через них). Системы модальной логики могут быть интерпретированы в терминах многозначной логики (простейшими системами модальной логики являются трёхзначные: '' истина'', ''ложь'', ''возможно''). Это обстоятельство, а также возможность применения многозначной логики к построению теории т. н. “правдоподобных” выводов указывают на её глубокое родство с вероятностной логикой. Помимо “абсолютных” модальностей, в модальной логике приходится иметь дело с т. н. “относительными”, т. е. связанными с каким-либо условием (“А возможно, если В”, и т. п.). Понятия всякого рода относительных модальностей удаётся легко формализовать, дополняя аппарат модальной логики аппаратом логики предикатов. Введём три понятия, поясняющие связь между операторами необходимости и возможности. Два суждения противоречивы, если они несовместимы ни по истинности, ни по ложности. Контрарными являются суждения, совместимые по ложности, но несовместимые по истинности. Два суждения находятся в отношении подчинения, лишь, если из первого следует второе, но из второго не следует первое. Модальные формулы всегда можно записать посредством оператора , поскольку справедливо: A. Приведём одну важную зависимость, также выражаемую через оператор : A  AA, что читается следующим образом: высказывание “случайно A” эквивалентно высказыванию “возможно A и возможно не-A”. 5.2.2 Синтаксис и семантика модальной логики Определение 2 Структурой называется пара F=(W, R), где W – непустое множество, а R – бинарное отношение на множестве W. Элементы такого множества называются точками. Определение 3 Пусть P – множество высказываний модального языка L. Тогда P-моделью на структуре (W, R) называется тройка M=(W, R, V), причём V (p) интерпретируется как множество точек из W, в которых высказывание p истинно. Пусть wW и A – модальная формула. Запись M |= wp означает, что A истинна в точке w модели M. Тогда можно сформулировать следующие правила: • M|=wp, если wV(p); • M|=wA1A2, если из M|=wA1 следует M|=wA2; • M|=w A, если M|wA; • M|=wA, если M|=tA хотя бы для одного tW, такого, что wRt; • M|=wA, если из wRt следует M|=tA для tW. Последнее правило означает, что формула A истинна в точке w модели M, если она истинна во всех точках t, которые находятся в отношении R с точкой w. Сформулируем теперь понятие истинной формулы применительно к модели, структуре и общезначимой формуле. Формула A истинна в модели M, если она истинна во всех точках этой модели, т. е. если M|=wA для всех wW, что обозначается как M = wA. Формула A истинна в структуре F=(W, R), если она истинна в любой модели (W, R, V), т. е. если M|=wA для всех моделей M=(W, R, V). Это обозначается как F |= A. Формула общезначима, если она истинна во всех структурах F=(W, R). Это обозначается |=A. 6 Лекция №5 СХЕМЫ МОДАЛЬНЫХ ФОРМУЛ И ОБЗОР МОДЕЛЕЙ 6.1 Ключевые (основные) вопросы (моменты) — схемы модальных формул; — обзор других формально-логических моделей. 6.2 Текст лекции 6.2.1 Схемы модальных формул Определение 1 Модальная логика называется нормальной, если она содержит: • множество всех теорем логики высказываний, область действия которых распространяется на формулы модальной логики высказываний; • схему аксиомы дистрибутивности:K: (AB) (AB), назовём её схемой K, что читается следующим образом: “если необходимо, что A влечёт B, то из необходимости A следует необходимость B”; • модальные правила выводимости:A├A, т. е. A необходимо истинна при условии истинности A. Классическими обозначениями для некоторых схем являются следующие: • D: AA, • T: AA, • AA, (*) • B: AA, • AA, (**) • L: ((AA)B)((BB)A), • W: (AA)A. Приведём словесные названия некоторых из схем. Схему T называют схемой аксиомы знания. Схему (*) называют схемой аксиомы положительной интроспекции. Схема (**) называется аксиомой негативной интроспекции. Необходимо отметить, что выбор модальной схемы зависит от моделируемого понятия. Наряду с алгебраическими семантиками в модальной логике построены так называемые семантики возможных миров. Основным понятием в этих семантиках является понятие возможного мира. Под возможным миром понимается существующее или мыслимое положение дел либо возможный ход событий. Поэтому, когда речь идёт о достижимости из одного мира другого, под этим следует понимать некоторое отношение, переводящее одно состояние в другое. Вспомним некоторые свойства, которыми может обладать бинарное отношение. • Рефлексивность: s (sRs) • Транзитивность: stu (sRttRusRu) • Симметричность: st (sRttRs) • Евклидовость: stu (sRtsRutRu) Определим понятие возможных миров и их семантики. Точки wW назовём возможными мирами универсума, а отношение R - отношением достижимости. Таким образом, структура состоит из множества W возможных миров, связанных отношением R. Если два мира s и t принадлежат универсуму W, то достижимость мира t из мира s обозначается sRt. Приведённые определения целесообразно представить следующим рисунком (рис. 1). Рис. 1 Сфера миров, достижимых из w1 Если представить универсум W возможных миров, то для каждого мира wiW множество достижимых из wi миров можно изобразить в виде сферы миров. В частности, на этом рисунке мир w2 достижим из мира w1. Истинные формулы в w2 возможно истинны в w1. Однако мир w3 недостижим, т. е. невозможен с позиций w1. Разнообразные трактовки модальных формул в разных модальных логиках могут приводить к изменению форм отношений достижимости, определяемых через R. 6.2.2 Обзор других формально-логических моделей 1) Логика возможного Определение 5 Необходимо истинной в мире S называется формула, которая подтверждается во всех мирах t, достижимых из S. Формула вида A читается «A необходимо истинна». Определение 6. Возможно истинной в мире S называется формула, которая подтверждается хотя бы в одном из миров, достижимых из S. Чтение формулы A следующие: «возможно, что A истинна». В универсуме один из миров можно было бы рассматривать в качестве «реального». Формула A, необходимо истинная в реальном мире, истинна и во всех мирах, достижимых из «реального мира», а, следовательно, и в самом реальном мире (свойство рефлективности). Таким образом, формула вида AA истинна в рассматриваемой структуре. Модальные понятия делятся на логические и физические (фактические). Например, положение дел может быть логически необходимо, логически возможно либо физически возможно, логически случайно либо физически случайно. Логически возможно то, что не противоречит законам логики. Поэтому не всё то, что логически возможно, возможно физически. Физически возможно то, что не противоречит законам физики, природы и общественным законам. Логически необходимо то, что является законом логики. Физически необходимы законы физики, природы и логические следствия из них. Например, если за V обозначить скорость света, то формула  (V<300000 км/с) истинна в реальном мире при условии, что V – физическая необходимость. На самом деле полагают, что законы физики подтверждаются во всех мирах, достижимых из реального мира. Однако логически возможно, чтобы указанная формула была ложной. 2) Временные логики Отношение достижимости, обозначение sRt, во временных логиках означает, что t следует за S. Следовательно, во временной логике возможные миры представляют состояния некоторого мира в различные моменты его эволюции. Интерпретация формулы A может быть такой: «во все будущие моменты произойдёт A», а формулы A такой: «по крайней мере в один из будущих моментов произойдёт A». Если же sRt определено как «t предшествует S», то формулы A и A соответственно могут читаться так: «во все прошлые моменты было A» и «по крайней мере, в один из моментов было A». Для временной логики естественными являются структуры (W, R), у которых W – это одно из множеств, а R – это отношение порядка (, , , ). 3) Динамические логики Динамическая логика основана на сопоставлении некоторого модального оператора каждой команде какого-то языка программирования. В этом контексте множество W интерпретируется как совокупность возможных состояний в ходе вычислений. Отношение sRt определяет, что вычисления начинаются в момент S и заканчиваются в момент t. Тогда недетерминированная программа может приводить к многочисленным результатам. В этом случае формула A будет означать «все выполнения программы оканчиваются тем, что A истинна», а формула A – «хотя бы одно выполнение программы заканчивается тем, что A истинна». 7 Лекция №6 НЕМОНОТОННЫЕ РАССУЖДЕНИЯ И МЕТОДЫ ПОИСКА 7.1 Ключевые (основные) вопросы (моменты) — модифицируемые рассуждения и свойства немонотонных логик; — зацикливание немонотонных рассуждений и его преодоление; — стратегии немонотонного вывода в глубину и ширину. 7.2 Текст лекции 7.2.1 Модифицируемые рассуждения и свойства немонотонных логик Важной чертой нерационального рассуждения является способность вырабатывать здравые суждения, хотя они могут быть и недостоверными. В частности, при неполной, неточной и изменчивой информации рассуждения зачастую бывают предположительными, всего лишь правдоподобными и, следовательно, подлежащими пересмотру, то есть модификации. Например, используя непрофессиональное, но распространенное представление о понятии «машины» как о некоторой системе, способной перемещаться в пространстве и зная, что «Кибер» - это машина, можно сделать вывод о возможности перемещения «Кибера». Такой вывод можно считать приемлемым. Однако его нельзя признать абсолютно корректным, так как не учитываются возможные использования этого термина в другой предметной области, где свойство перемещения может быть нехарактерным для машины. Если же будет сделано уточнение, что «Кибер» - это ЭВМ, то принятое рассуждение должно быть пересмотрено, путём опровержения допущения о возможности перемещения «Кибера». Несмотря на простоту приведённого примера, его трудно формализовать в рамках классической логики. Природа модифицируемых рассуждений базируется на двух фундаментальных разновидностях: Рассуждения являются модифицируемыми, когда они являются предположительными и, следовательно, правдоподобными. Такие рассуждения неточны, так как зависят от неполной, неточной или изменчивой информации. Рассуждения модифицируемы, когда они зависят от знаний, предполагаемых полными, но таковыми не являющихся либо перестающих быть таковыми. Немонотонный вывод характеризуется тем, что множество теорем необязательно растёт с множеством аксиом. Модифицируемые рассуждения не являются в классическом смысле общезначимыми. Этому можно дать следующее пояснение: вывести p из множества посылок A и отказ от p, как только к A добавлена новая информация q, означает, что допустимо вывести p. Свойства монотонности и, как следствие, транзитивности, здесь не удовлетворяются. Неадекватность систем дедукции классической логики для формализации модифицируемых рассуждений объясняется тем, что их правила являются позволяющими. Они имеют вид: q – теорема, если p1, p2,…, pn – теоремы. С одной стороны, моделирующая модифицируемые рассуждения система может обладать ограничивающими правилами вывода: q - теорема, если p1, p2,…, pn – теоремы. Таким образом, с помощью немонотонных логик предполагается моделирование общезначимых модифицируемых рассуждений. 7.2.2 Зацикливание немонотонных рассуждений и его преодоление Существенным обстоятельством, усложняющим осуществление систем немонотонного вывода, является возможность зацикливания рассуждений. Это объясняется необходимостью модификации правил вывода, так как немонотонная система должна обеспечивать возможность отказа от ранее сделанных выводов. С этой целью правила оснащаются условиями применения, проверка которых динамически изменяется с множеством посылок. Эти условия до вывода проверяют выполняемость некоторого утверждения вместе с выведенными ранее утверждениями из существующей системы посылок. Проблема здесь состоит в соотнесении выводимости и выполняемости. Необходимо также отметить, что отдельные заключения могут быть получены лишь после того, как будет установлена невыводимость каких-то других результатов. Практическая реализация алгоритмов модифицируемых рассуждений достаточно сложна. В настоящее время применяются три семейства немонотонных логик. I. Логики умолчаний. Эти логики часто называют логиками типичного. Они введены и развиты Рейтором для формализации рассуждений, являющихся всего лишь выполнеными. Следовательно, немонотонность в них обусловлена необщезначимостью правил вывода. При неполной информации мы можем получить только правдоподобные предположительные заключения. Часто бывает, что правила истинные в большинстве случаев, мы принимаем как абсолютно общие, хотя в них и допускаются исключения. Логики умолчаний позволяют формировать рассуждения в виде правил вида: . Смысл состоит в следующем. Если мы допускаем истинность  и если  выполнимо при сделанных допущениях , то можно допустить и истинность . В приведённом правиле символ M – метасимвол, отражающий возможность (выполнимость) некоторого факта. Здесь следует обратить внимание на то, что в связи с возникающими алгоритмическими и вычислительными трудностями, по данному направлению неизвестны какие-либо значительные практические реализации. II. Модальные немонотонные логики Мак-Дермотта. Они основаны на аксиоматических системах модальной логики и предназначены для характеризации множеств взаимно выполняемых утверждений, которые можно вывести из какого-то задаваемого множества посылок. Немонотонные логики Мак-Дермотта предлагают независимую от области применения (и в этом смысле универсальную) аксиоматическую систему оценки выполняемых множеств утверждений. Для формализации модифицируемых рассуждений используется модальная логика. Кроме того, в рамках этой логики предусмотрена возможность устранения зацикливаний при задании правил немонотонного вывода. Здесь имеет место ситуация, когда опровергнутый ранее вывод, на следующем шаге при поступлении дополнительной информации множеств вновь оказаться непротиворечивым. Поскольку история предыдущих доказательств не сохраняется, по существу доказательство уже пройденного пути начинается с самого начала. Таким образом, можно сделать вывод о невысокой эффективности таких систем. III. Автоэпистемические логики. Они позволяют осуществлять формализацию уравнения вида: «если я не предполагаю, что p подтвердится, то подтверждается q». Под идеально разумными понимаются рассуждения, содержащие следующие идеализации: можно выводить только ожидаемые идеологические следствия из исходного множества предположений и все эти логические следствия надо принять во внимание. Это важное обстоятельство ставит под сомнение реализуемость задач, основанных на этих логиках, поскольку для рассуждений нужны неограниченные ресурсы. 7.2.3 Стратегии немонотонного вывода в глубину и ширину Для задач, сформулированных в терминах пространства состояний, существуют различные подходы к проблеме поиска решающего пути. Пространство состояний – это граф, вершины которого соответствуют ситуациям, встречающимся в задаче, а решение задачи сводится к поиску пути на графе. Вершины графа соответствуют проблемным ситуациям, а дуги – разрешённым переходам из одних состояний в другие. Отыскание плана решения задачи эквивалентно построению пути между заданной начальной ситуацией и некоторой указанной заранее конечной ситуацией, которая называется целевой вершиной. Основными стратегиями поиска являются поиск в глубину и поиск в ширину. Для обеих стратегий допустимы следующие допущения: • процесс вывода заключения интерпретируется как дедуктивный процесс доказательства теории; • логический вывод по существу сводится к достижению цели G на основе последовательного процесса доказательства истинности (или ложности) частичных целей. Проход в глубину (рис. 1) образует путь, который может и не достигать цели, поэтому должен быть предусмотрен механизм возврата для поиска альтернативы, вновь ведущей вглубь. При этом история альтернатив должна быть сохранена для того, чтобы при повторном поиске в глубину «не проходить» старый безуспешный путь. Рис. 1. Поиск в глубину Другой подход к построению системы немонотонных рассуждений основан на использовании стратегии поиска в ширину. Принцип стратегии поиска в ширину заключается в следующем. В противоположность поиску в глубину стратегия поиска в ширину предусматривает переход в первую очередь к вершинам, ближайшим к стартовой вершине. В результате процесс поиска имеет тенденцию развиваться более в ширину, чем в глубину, что проиллюстрировано на рис. 2. Рис. 2. Поиск в ширину Поиск в ширину реализуется алгоритмически не так легко, как поиск в глубину. Причина этого в том, что приходится сохранять всё множество альтернативных вершин-кандидатов, а не только одну вершину, как при поиске в глубину. Кроме того, если в процессе поиска необходимо получить решающий путь, то одного множества вершин не достаточно. Поэтому хранят множество путей-кандидатов. Для того, чтобы выполнить поиск в ширину при заданном множестве путей-кандидатов, необходимо: если голова первого пути – это целевая вершина, то взять путь в качестве решения, в противном случае удалить первый путь из множества кандидатов и породить множество всех возможных продолжений этого пути на один шаг, множество продолжений добавить в конец множества кандидатов, а затем выполнить поиск в ширину с полученным новым множеством.