Глава 1 Исчисление высказываний - копия. Исчисление высказываний
 Скачать 46.25 Kb.
|
Y истинно, когда X и Y имеют одинаковые истинностные значения, в противном случае X ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ 1.1. Понятие формальной системы Появление формальных систем было обусловлено осознанием того факта, что совершенно различные системы, будь то технические, социальные, экономические или биологические, обладают глубоким сходством. Действительно, каждая конкретная система состоит из каких-то первичных (базовых) элементов, обладающих какими-то свойствами. Затем, исходя из наличия исходных описаний, можно логическим путём вывести описание новых свойств, причём утверждения о наличии исходных или выведенных свойств воспринимаются как истинные на основании смысла определений данных элементов. В формальной системе (ФС), оперирующей теми или иными символами, эти символы воспринимаются просто как элементы, с которыми обращаются согласно определенным правилам, зависящим лишь от формы выражений, образованных из символов. Здесь нет понятия истинности, оно появляется лишь в связи с возможными приложениями (интерпретациями) этой системы. Формальные системы, с которыми мы будем иметь дело, — это аксиоматические системы, т. е. системы с наличием определённого числа исходных заранее выбранных и фиксированных высказываний, называемых аксиомами. Говорят, что аксиоматическая ФС «проста» и «эффективна». Под «простотой» будем понимать то, что для любой реальной системы, являющейся интерпретацией данной аксиоматической системы, можно обойтись одним и тем же числом исходных допущений, необходимых для получения тех или иных выводов любой системы. Говоря об «эффективности» ФС, следует иметь в виду то, что каждый вывод аксиоматической системы может быть автоматически перенесён на любую из её интерпретаций. Поскольку любая рассматриваемая в книге формальная система имеет аксиомы, слово «аксиоматическая» в дальнейшем будет опускаться. Предъявим к формальным системам ещё одно требование. Это требование связано с понятием эффективной процедуры. Под эффективной процедурой (алгоритмом) в интуитивном смысле будем понимать совокупность предписании, позволяющую посредством формального выполнения этих предписаний через конечное число шагов получить ответ на любой вопрос из некоторого класса вопросов. Формальная система считается заданной, если выполнены следующие условия. 1. Задано некоторое множество, состоящее из конечного или бесконечного числа элементов, которые носят название термов. Имеется другое конечное множество, элементы которого есть связка или операции. 2. Любую линейно упорядоченную совокупность термов и операции будем называть формулой. Из множества формул выделим подмножество правильно построенных формул (ППФ). Для ППФ задаются правила их конструирования, т. е. определяется эффективная процедура, позволяющая по данному выражению выяснить, является ли оно ППФ или нет в данной ФС. 3. Выделено некоторое множество ППФ, называемых аксиомами ФС. Понятие аксиомы должно быть эффективным, т. е., также, как и для ППФ, должна иметься эффективная процедура, позволяющая для произвольной ППФ решить, является ли она аксиомой. 4. Имеется конечное множество Д1, Д2,... отношений между ППФ, называемых правилами вывода. Понятие «вывода» также должно быть эффективным. Иными словами, должна иметься эффективная процедура, позволяющая для произвольной конечной последовательности ППФ решить, может ли каждый член этой последовательности быть выведен из одной или нескольких предшествующих ППФ этой последовательности посредством некоторых фиксированных правил вывода. Выводом в ФС называется любая последовательность ППФ А1, А2, .... Аn такая, что для любого i (1≤i≤n) ППФ Аi есть либо аксиома ФС, либо непосредственное следствие каких-либо предыдущих ППФ по одному из правил вывода. ППФ В называется теоремой (или выводимой ППФ) ФС, если существует вывод в ФС, в котором последней ППФ является В. Понятие теоремы не обязательно эффективно, так как вообще говоря, может и не существовать эффективной процедуры, позволяющей узнавать по данной ППФ существует ли её вывод в ФС. Формальная система, для которой такая эффективная процедура существует, называется разрешимой, в противном случае — неразрешимой. ППФ В выводима из ППФ А1, А2,….Аn , или является следствием множества А1, А2,….Аn тогда и только тогда, когда существует такая конечная последовательность ППФ В1, В2, …, Вr, что Вr есть В и для любого i (1 ≤ i ≤ г) Bi есть: 1) либо аксиома, 2) либо Аi 3) либо непосредственное следствие некоторых предыдущих ППФ по одному из правил вывода. Элементы последовательности ППФ А1, А2, .... Аn называются посылками вывода (или гипотезами). Сокращённо вывод В из А1, А2,….Аn будем записывать А1, А2, ..., An |— B, или если Г = {А1, А2, ..., AJ}, то Г |— B. Вывод ППФ В без использования посылок есть доказательство ППФ В, а сама В — теорема, что записывается |— В. Приведём несколько свойств понятия выводимости из посылок. 1. Если ГÍП И Г |— В, то П |— В. Это значит, что если ППФ В выводима из множества посылок Г, то она также будет выводима, если к Г добавятся новые посылки. 2. Г |— В тогда и только тогда, когда в Г существует конечное подмножество П, для которого П |— В. Это очевидно, исходя из (1). 3. Если П |— А и Г |— В для любой ППФ В из множества П, то Г |— А. Это значит, что если ППФ А выводима из П и каждая содержащаяся в П ППФ выводима из Г, то ППФ А выводима из Г. Таким образом, любая ФС задаётся четвёркой: <Т, Н, A, В>, где Т — множество термов и операций; Н — множество правил конструирования ППФ; А — система аксиом; В — множество правил вывода. Пример 1.1. Рассмотрим неандертальскую систему счисления. Множество Т состоит из палочек и операций: сложения, приписывания одной палочки к другой и равенства. Правила конструирования ППФ: 1) | есть ППФ; 2) если α — ППФ. то α | также ППФ; 3) если α и β — ППФ, то α + β также ППФ; 4) если α и β — ППФ, то α = β также ППФ; 5) других ППФ нет. Отсюда ||...|| — ППФ (правило 2); ||...|| + ||...|| — ППФ (правила 2, 3);  — ППФ (правила 2, 4) (как в случае n≠ m, так и в случае n = m);||...|| + ||...|| = |...|| + ||...|| + ||...| = ||...| …－ППФ (правила 2, 3, 4) и т.д., но + || не есть ППФ, так как нет такого правила образования ППФ. Система аксиом состоит из одной аксиомы: | = |. Правила вывода: 1) все аксиомы выводимы, т. е. являются теоремами; 2) если |— α = р, то |— α + | = р |; 3) других правил вывода нет. Найдём множество теорем: | = | — теорема (правило 1); | + | = || — теорема (правило 2); | + | + ...+ | = ||... || — теорема (правило 2), n n т. е. теоремой будет любая ППФ. в которой слева и справа от знака равенства стоит одно и то же число палочек. Теперь рассмотрим расширение формальной системы путём ввода дополнительных правил на множества Н, А и R. Пусть на множество Н, задающее синтаксис ФС, действуют некоторые правила h, фиксирующие изменения в правилах Н, т. е. правила изменяют синтаксис формальной системы. В системах принятия решений такая задача может рассматриваться, например, как задача перевода фактов из одной системы представления знаний в другую. Далее, пусть в ФС допускается как добавление новых аксиом, так и исключение старых. Это может делаться с помощью некоторых правил g, изменяющих систему аксиом А. Эти правила целенаправленно изменяют А, причём нахождение тех из них, которые задают целевые факты, может трактоваться, например, как задача поиска закономерностей мира, в котором функционирует та или иная система принятия решений. И наконец, пусть в ФС разрешается изменять набор правил вывода R, что и делается с помощью некоторых правил р. Для систем принятия решений проблема изменения правил R может пониматься, например, как задача адаптации данной системы к внешней среде. Таким образом, полученная семёрка <Т, Н, A, R, h,g, р> будет характеризовать расширение формальной системы, называемое семиотической системой. Её особенность проявляется прежде всего в том, что семиотическая система является открытой, так как множество аксиом А может изменяться с помощью правил g. Кроме того, такая система пригодна как для реализации дедуктивных, так и недедуктивных процессов, а также вследствие её открытости процессов обучения и адаптации. Для функционирования семиотической системы необходимо задать проблемно ориентированную формальную систему и правила её изменения. Отметим, что сама формальная система не является ни языком, ни системой знания, она не содержит никаких утверждений об объектах, а является просто исчислением — некоторого рода действиями по определенным правилам над последовательностями термов. Мы рассмотрим для класса формальных систем, являющихся математической базой для построения систем принятия решений: исчисление высказываний и исчисление предикатов первого порядка. 1.2. Основные понятия исчисления высказываний Здесь рассматривается только минимум сведении об исчислении высказываний, необходимый для построения первого класса ФС. В исчислении высказываний будем иметь дело только с формулами, составленными из элементарных формул, соединённых некоторыми связками. Элементарные формулы будут интерпретироваться как простые высказывания, записанные в виде повествовательных предложении естественного языка и принимающие два значения: истина (И) или ложь (JI). Если простое высказывание А истинно, то говорят, что А принимает значение И, если А ложно, то Л. Символы И и Л будем называть истинностными значениями. Сложное высказывание имеет истинностное значение, которое однозначно определяется истинностными значениями простых высказываний, из которых оно составлено. Например, «Если студент ложится поздно спать и пьёт на ночь кофе, то утром он встаёт в дурном расположении духа пли с головной болью». Это сложное высказывание состоит из следующих простых высказываний: «Студент ложится поздно спать». «Студент пьёт на ночь кофе». «Утром студент встаёт в дурном расположении духа». «Утром студент встаёт с головной болью». Обозначим сложное высказывание через А, а простые соответственно через Y, Z, U, V. Тогда сложное высказывание запишется в виде А = Если Y и Z, то U или V. Для обозначения используемых в этом примере связок «если ... то», «и», «или» введём специальные символы →, ＆, ˅. Тогда в символическом виде высказывание А запишется так: А=(Y&Z) → (U˅V). Каждую логическую связку можно рассматривать как операцию, которая образует новое высказывание — сложное высказывание более простых высказываний. Рассмотрим следующие логические связки (операции): 1) отрицание ¬ А. ¬ А истинно, когда A ложно, и ложно, когда А истинно; 2) конъюнкция А & Y. A & Y истинно, когда А и Y оба истинны, в противном случае А & Y ложно; 3) дизъюнкция А ˅ Y. А ˅ Y ложно, когда А и Y оба ложны, в противном случае А ˅ Y истинно. Дизъюнкция понимается, как неразделительное «или», т. е. высказывание «А или Y» утверждает истинность либо одного из высказываний, либо обоих вместе; 4) импликация А → Y. А → Y ложно, когда А—истинно, а Y — ложно, в противном случае А → Y истинно. А → Y читается как «если A то Y» или «А влечёт Y»; 5) эквивалентность (равнозначность) X |
| X Y Z | ¬ Y | X ˅ ¬ Y | (X ˅ ¬ Y)→Z |
| Л Л Л Л Л И Л И Л Л И И И Л Л И Л И И И Л И И И | И И Л Л И И Л Л | И И Л Л И И И И | Л И И И Л И Л И |
Для того чтобы сократить количество скобок в формуле, часто используют правила силы операций:
связка _| сильнее связок &, ˅, →, ;
связка & сильнее связок ˅, →, ;
связка ˅ сильнее связок →, ;
связка → сильнее связки ;
Внешние скобки всегда будем опускать и вообще везде, где не возникает двусмысленностей, будем пользоваться минимумом скобок.
Пусть дана формула В и Х1, Х2, ..., Хn — атомы, в ней встречающиеся. Тогда под интерпретацией формулы B будем понимать приписывание истинностных значений атомам Х1, Х2, ..., Хn.Говорят, что формула В истинна в данной интерпретации тогда и только тогда, когда B принимает значение И в этой интерпретации; в противном случае говорят, что В ложна в этой интерпретации. Если имеется n различных атомов в формуле, то существует 2n различных интерпретаций для этой формулы. Для удобства в формуле, имеющей атомы X1 ,Х2, ..., Хn интерпретации можно представлять в виде множества {m1,m2, ..., mn}, где mi есть либо Xi если X принимает значение И, либо ¬ Xi, если JI.
Например, множество { |¬ Х1, Х2, X3,¬ X4} представляет собой
интерпретацию, в которой атомы Х1, Х2, X3, X4 принимают соответственно значения JI, И, И. Л.
Формула исчисления высказывании, которая истинна во всех интерпретациях, называется тавтологией или общезначимой формулой. Примерами тавтологии являются X ˅ ¬ X, Х → (Y → X). Чтобы в этом убедиться, необходимо рассмотреть их истинностные таблицы.
Аналогично, формула исчисления высказываний называется противоречием или тождественно ложной, если она принимает значение JI во всех интерпретациях. Например, A ¬ А, A & ¬ A.
Если формула В истинна в некоторой интерпретации I, то говорят, что I удовлетворяет формуле В или что В удовлетворяется интерпретацией I. Аналогично, если В ложна в некоторой интерпретации I, то говорят, что I не удовлетворяет В или В не удовлетворяется I. Например, формула A1 ˅ ¬ А2, удовлетворяется интерпретацией {А1, А2), НО не удовлетворяется {¬ А1, А2}.
Истинностные таблицы дают нам эффективную процедуру для решения вопроса о том, является ли данная формула общезначимой или противоречием. Однако составление ИСТИННОСТНЫХ таблиц, особенно для сложных формул, является утомительным и непрактичным делом. Поэтому установим несколько правил образования тавтологий из тавтологий (ясно, что для получения противоречия надо применить к тавтологии операцию отрицания). Как правило, все теоремы будут даваться без доказательства. Желающие доказать их могут попробовать сделать это сами или обратиться к учебникам по математической логике.
Теорема 1.1. Пусть В есть некоторая формула, а В* — формула, полученная из B подстановкой формулы С вместо атома X везде, где он встречается в B. Тогда, если В — тавтология, то и В* также тавтология.
Этот результат позволяет нам получать из тавтологии путём подстановок вместо атомов соответствующих формул другие тавтологии. В дальнейшем он будет фигурировать в ФС как правило подстановки.
Условимся называть формулу В равносильной формуле С (т. е. В = С) тогда и только тогда, когда истинностные значения В и С совпадают при каждой интерпретации В и C. Например,
А1→А2 = ¬А1 ˅ А2, ¬ (А1 ˅ A2) = ¬ А1 & ¬ A2, ¬ (А1 & А2) =
= ¬ А1 ˅ ¬ A2 и т. д.
Теорема 1.2. Формула В С является тавтологией тогда и только тогда, когда В = С.
Доказательство очевидно.
Теорема 1.3. Если В и В → С—тавтологии, то С—также тавтология.
Доказательство очевидно. Этот результат известен как правило дедуктивного вывода — modus ponens.
1.3. Исчисление высказывании как формальная система
Рассмотрим формальную аксиоматическую систему ФС для исчисления высказываний.
1. Исходными термами ФС являются буквы латинского алфавита с индексами или без них. Исходные термы называются высказывательными переменными или атомами. Исходными символами логических связок являются ¬, ＆, ˅, →, которые интерпретируются как отрицание, конъюнкция, дизъюнкция и импликация. Для удобства записи формул введём ещё пару символов (,),. называемых скобками. Других исходных символов исчисление высказываний не имеет.
2. Правила образования ППФ:
а) все атомы есть ППФ;
б) если А и В — ППФ, то ¬ А, A&В, A ˅ В, A → В — также ППФ;
в) других правил образования ППФ нет.
Примеры ППФ: Х→Ø Y, (Х&Y)→(Y ˅ Ø Z). Для удобства внешние скобки будем опускать, а применяя правила силы операций, перейдём к той же форме записи ППФ, что и формул исчисления высказывании. При интерпретации ППФ интерпретируются все атомы, в неё входящие, а затем производится интерпретация результатов логических операций. Окончательный результат интерпретаций операций считается результатом интерпретации всей ППФ. Понятие ППФ, как мы уже выяснили в 1.1, является эффективным.
3. Система аксиом (П. С. Новиков).
I а1 А→(В→А);
а2 (А→(В→C))→((A→B)→(А→С));
II aЗ А&В→А;
а4 А & В →В;
а5 (А→В)→((А→C)→(A→B＆C));
III а6 А→А ˅ В;
а7 В→А ˅ В;
а8 (А→С)→((В→С)→(А ˅ В)→С));
IV а9 (А→В)→(ØВ→ØА);
а10 А→ØØА;
all ØØА→А.
Все аксиомы — общезначимые ППФ.
4. Правила вывода.
п. 1. Все аксиомы выводимы.
п.2. Правило подстановки. Пусть А — ППФ, содержащая атом X.
Тогда, если А — теорема исчисления высказываний, то заменив в ней атом X всюду, куда он входит, на произвольную ППФ В, мы получим также теорему. Сокращённо обозначим это правило через ПС. В принципе, считая, что каждая аксиома понимается как схема аксиом, т. е. включает в себя бесконечно много аксиом, это правило излишне. Мы оставим его ввиду наглядности и ясности изложения.
п. 3. Правило modus ponens (правило дедуктивного вывода).
Если А и А →В — теоремы, то B — также теорема. Это правило
будем сокращённо обозначать через МР.
п. 4. Других правил вывода нет.
Пример 1.2. Обозначим через Р любую выводимую ППФ в ФС1. Покажем, что |— X→Р:
1) |— Y→ (X→ Y) al;
2) |— P→ (X→P) ПС;
3) |—X→ Р МР.
Пример 1.3. Покажем, что |— X→ X:
1) |—(X→(F→ Z))→((X→F)→(X→Z)) а2;
2) |—(Х → (Y→ Х))→((Х→Y)→(Х→Х)) ПС;
3) |—(Х→Y)→(Х→Х) МР;
4) |—(Х→ Р)→(Х→Х) ПС, здесь |—Р;
5) |—X→ X Пр. 1.2 и МР.
Считаем, что каждая ППФ В выводима из множества посылок
А1, А2, ..., Аn, если:
1) каждая Ai (1≤i≤n) выводима из А1, A2, ..., An;
2) каждая выводимая в ФС ППФ выводима также из А1, A2, ..., An;
3) из выводимости А и А → B из А1, А2, ..., Аn следует выводимость B из А1, A2, ..., An.
Если А1, A2, ..., An являются аксиомами или другими выводимыми ППФ, то множество выводимых из них ППФ совпадает со множеством всех выводимых в данной ФС1 ППФ.
Понятие выводимости сводится к понятию доказуемости с помощью теоремы Ж. Эрбрана о дедукции, которая гласит:
Если А1,A2, ...,An |—B, то |—A1→(А2→(...(Аn→В)...)).
Таким образом, показывается, что если ППФ В выводима из посылок А1, А2, ..., Аn, то ППФ A1→ (А2→ (… (Аn→ В) ...)) есть теорема. Как следствие этой теоремы, приведём несколько правил ФС, которые значительно сокращают путь доказательства теорем.
Правило 1 (правило силлогизма).
Если |—А→ В и |— В→ С, то |— А→С.
Очевидно, что
1) А →В, В→ С, A |—C МР;
2) |—(А→ В)→ ((В →С)) → (А→С)) теорема дедукции;
3) |—(В→С)→(А→С) МР;
4) |—А→ С МР.
Правило 2 (разновидность силлогизма).
Если А |—В, С |— D и В, D |— Е, то А, С |— Е.
1) |— С→ D теорема о дедукции;
2) В |—D→E теорема о дедукции;
3) B |—С→Е силлогизм из 1, 2;
4) |—В →(С→ Е) теорема о дедукции;
5) |—A→B теорема о дедукции;
6) |—А→ (С→ Е) с иллогизм из 4, 5.
Правило 3 (правило перестановки мест посылок).
Если |—А→ (В→ С), то и |—B→(А→ С).
1) А → (В→ С), В, A |—С МР;
2) А→(В→ С) |— В→ (А→ С) теорема о дедукции.
Читатель аналогично может доказать следующие два правила.
Правило 4 (правило объединения посылок).
Если |—A→(B→С), то |— А & В →С.
Правило 5 (правило разъединения посылок).
Если |—А & В →С. То |—A→(В →С).
Система аксиом исчисления высказываний обладает следующими тремя важными свойствами: полнотой, непротиворечивостью и независимостью. Тот факт, что любая теорема ФС, является общезначимой ППФ, вытекает из того, что все аксиомы — тавтологии и правила вывода, применённые к тавтологиям, всегда приводят к тавтологиям. Обратное утверждение и представляет собой теорему о полноте.
Теорема 1.4 (о полноте в широком смысле). Если ППФ А формальной системы ФС1 является общезначимой, то она есть теорема этой системы.
Кроме понятия полноты в широком смысле имеет место понятие полноты логического исчисления в узком смысле. Исчисление высказываний называется полным в узком смысле, если присоединение к его аксиомам какой-нибудь не выводимой в нем ППФ приводит к противоречию.
Перейдём ко второму свойству системы аксиом — непротиворечивости. Проблема непротиворечивости является одной из кардинальных проблем математической логики.
Любое логическое исчисление называется непротиворечивым, если в нем не выводимы никакие две ППФ, из которых одна является отрицанием другой. Если мы имеем противоречивую систему, то в ней мы могли бы вывести любые ППФ, что не представляло бы никакой ценности, так как в такой системе не было бы различий между истиной и ложью.
Например, известно, что следующая ППФ есть теорема, т. е. |— А→ (Ø А→В) и если в противоречивой системе некоторая ППФ А была бы выводима вместе со своим отрицанием Ø А, то по правилу МР была бы теоремой любая ППФ В.
Теорема 1.5 (о непротиворечивости). Исчисление высказывании непротиворечиво.
И наконец, третье свойство системы аксиом — независимость. Аксиома, не выводимая с помощью правил вывода из остальных аксиом, называется независимой от этих аксиом, а система аксиом, в которой ни одна аксиома не выводима из остальных, называется независимой системой аксиом.
Теорема 1.6 (о независимости). Каждая аксиома формальной системы ФC1 независима.
В заключение этого раздела заметим, что с помощью теоремы о полноте устанавливается факт равноценности понятия общезначимости и доказуемости. Так как вопрос об общезначимости может быть эффективно решён для произвольной ППФ, то понятие теоремы в исчислении высказываний эффективно.
1.4. Нормальные формы
В дальнейшем там, где мы не применяем понятие формальной системы, будем ППФ называть формулой. Любую формулу исчисления высказываний удобно представить в виде так называемой нормальной формы. Атом или его отрицание будем называть литерой.
Говорят, что формула В представлена в конъюнктивной нормальной форме (КНФ) тогда и только тогда, когда она имеет форму В = В1 & В2 & ... & Вm, где каждая из Вi ( (1 ≤ i ≤ m) есть дизъюнкция литер. Например, В = (Х1 ˅ Ø X2) & (ØX1 ˅ X2˅ ØX3) & X3.
Аналогично говорят, что формула В представлена в дизъюнктивной нормальной форме (ДНФ) тогда и только тогда, когда она имеет форму В = B1 ˅ В2 ˅ ... ˅ Вm, где каждая из Bi (1 ≤ i ≤ m) есть конъюнкция литер. Например, В = (Ø Х1 & X2 & X3) ˅ (Х1 & X2)˅ ØX3.
Любая формула исчисления высказываний может быть преобразована в нормальную форму с помощью следующего алгоритма.
Шаг 1. А В = (А→B) & (В→ А).
А→В= ØА ˅ В.
Шаг 2. ØØА=А.
Ø(A ˅ В) = Ø А & ØВ
Ø (А & В) = Ø А˅ ØB закон Де-Моргана
Шаг 3. A ˅ (В & C) = (А ˅ В) & (А ˅ С) (для КНФ).
А & (В ˅ С) =А & В ˅ А & С (для ДНФ).
Пример 1.4. Получим КНФ для формулы (А → (В ˅ Ø С)) → D.
(А→(В ˅ ØС))→D = (ØА ˅ В ˅ Ø|C) →D =
= Ø(ØА ˅ В ˅ Ø С) ˅ D = (А & Ø B & С) ˅ D =
= (D ˅ А) & (D ˅ (Ø В & С)) = (D ˅ А) & (D ˅ Ø В) & (D ˅ С).
Пример 1.5. Получим ДНФ для формулы Ø (А & В) & (A ˅ В).
Ø (А & В) & (А ˅ В) = (Ø А ˅ ØВ) & (А ˅ В) =
= ((Ø А ˅ Ø В) & А) ˅ ((ØA ˅ ØВ) & В) = (А &ØB) ˅ (B &ØA).
1.5. Логические следствия
Очень часто нам приходится иметь дело с утверждениями, которые выводятся механическим путём из начального списка рассуждений, фактов, посылок, аксиом. Этим занимается раздел математической логики — теория дедуктивного вывода. В соответствии с правилами, установленными в той или иной логической системе, заключительному утверждению — теореме, полученной из начальной системы утверждений — аксиом, посылок, приписывается истинностное значение И, если каждой аксиоме, посылке также приписывается значение И. Рассмотрим пример.
Пример 1.6. «Если я поеду автобусом, н автобус опоздает, то я опоздаю нa работу. Если я опоздаю на работу и стану огорчаться, то я не попадусь на глаза моему начальнику. Если я не сделаю в срок важную работу, то я начну огорчаться н попадусь на глаза моему начальнику. Следовательно, если я поеду автобусом, а автобус опоздает, то я сделаю в срок важную работу». Запишем все посылки и заключение в символическом виде:
1) А & В→С:
2) C & D→ØE;
3) ØK→D & E;
4) А & В → К.
Покажем, что заключение (4) истинно, когда истинны все три посылки. Представим посылки в КНФ.
(Ø(А& В) ˅ С) & (Ø(С & D) ˅ Ø Е) & (К ˅ D & Е) =
= (Ø А ˅ Ø В ˅ С) & (Ø С ˅ Ø D ˅ Ø Е) & (К ˅ D) & (К ˅ Е).
Аналогично заключение: Ø (А & В) ˅ К = Ø А ˅ Ø В ˅ К.
Задавая интерпретации, в которых истинны посылки, нетрудно обнаружить, что будет истинно и заключение. Желающие могут выписать истинностную таблицу, чтобы и этом убедиться.
Таким образом, если даны формулы F1, F2, ..., Fn и В, то говорят, что формула B является логическим следствием F1, F2, ..., Fn (или В логически следует из F1, F2, ..., Fn) тогда и только тогда, когда для любой интерпретации I, в которой F1 & F2 & ... & Fn— истинно, B также истинно.
Логически правильные рассуждения важны для образования новых истинных утверждений из истинных посылок. Убеждение в логической правильности конкретного рассуждения связано с актом обобщения, который заключается в переходе от этого конкретного рассуждения к его форме. Переход от конкретного рассуждения к его форме можно описать как замену имён, обозначающих конкретные отношения, функции и константы на неинтерпретированные имена для отношении, функций, констант. И наоборот, из любого формального рассуждения можно, интерпретируя входящие в это рассуждение неопределенные имена, получить конкретное рассуждение. Естественно, если формальное рассуждение логически правильно, то интерпретированное рассуждение будет истинным.
Для обозначения логического следования формул В из посылок F1, F2, ..., Fn будем писать F1, F2, …, Fn |= В. Символ |= есть некоторое отношение между формулами, причем, если посылки соединены знаком &. то имеет место двуместное отношение |=: F1 & F2& … & Fn |= В.
Теперь приведем две простые, но важные теоремы, связывающие понятия логического следования с понятиями общезначимости и противоречия.
Теорема 1.7. Даны формулы F1,F2, … ,Fn и В. Формула В является логическим следствием формул F1, F2, … ,Fn тогда и только тогда, когда формула F1 & F2 & ... & Fn→В общезначима, m. е. |=F1＆F2 &…&Fn→В.
Теорема 1.8. Даны формулы F1,F2, ..., Fn и В. Формула В является логическим следствием формул F1,F2, …, Fn тогда и только тогда, когда формула F1&F2&…＆Fn＆Ø:В противоречива.
Таким образом, факт, что данная формула является логическим следствием конечной последовательности формул, сводится к доказательству общезначимости или противоречивости некоторой формулы. Следовательно, имеется полная аналогия при выводе теоремы из множества аксиом или посылок в формальной системе, и многие проблемы в математике могут быть сформулированы как проблемы доказательства теорем.
Обозначим общезначимую формулу через ■, а противоречивую — через . Вернемся к примеру 1.6 и покажем, что формула
(Ø А ˅ Ø В ˅ С) & (ØC ˅ Ø D ˅ Ø Е) & (К ˅ D) &
&(K ˅ E) & Ø(ØA ˅ ØB ˅ K)
является противоречивой.
Действительно,
(ØA ˅ ØB ˅ С) &(ØC ˅ ØD ˅ ØE) &
& (К ˅ D) & (К ˅ Е) & А & В & ØK = А & В & Ø К&С &
&(А&В&ØК&ØС \/ A&B&ØK&ØD ˅ А &В&Ø K&ØE)&A&B&ØK&D&E=.
Аналогично можно показать обще значимость формулы
(ØА ˅ ØB ˅ C)&(ØC ˅ ØD ˅ ØЕ)&(К ˅ D)&(K ˅ Е)→
→(ØA ˅ ØB ˅ K) = ■.
Примененный здесь подход для получения противоречивой формулы, конечно, далек от практического применения. В дальнейшем будут даны более эффективные процедуры доказательства общезначимости или противоречивости формул.