Элементы математической логики. Исчисление высказываний, его полнота
Чтобы задать логическое исчисление нужно задать :
1) множество символов исчисления Х;
2) множество выражений Х* (конечная последовательность символов)
3) множество формул исчисления ;
4) множество аксиом исчисления ;
5) множество правил вывода исчисления. Это есть формальные процедуры (алгоритмы), которые по произвольным формулам и формуле А определяют выводима ли непосредственна формула А из формул . В случае, если формула А выводима из непосредственно, этот факт записывают .
Формула А выводима в логическом исчислении, если существует последовательность формул , что последняя формула , и все формулы этой последовательности есть либо аксиомы логического исчисления, либо непосредственно следуют из предыдущих формул по правилам вывода данного исчисления. В этом случае говорят, что формула А является теоремой исчисления и записывают |-A.
Будем говорить, что А является следствием формул (гипотез) и записывать |-A, если существует последовательность формул что последняя формула есть А и каждая формула в этой последовательности есть либо аксиома, либо одна из гипотез , либо непосредственное следствие предыдущих формул .
Свойства выводимости:
1) пусть из множества гипотез Г выводится формула А, множество Г Δ есть подмножество множества Δ, тогда формула А есть следствие множества формул Δ |-A . Утверждение следует из того факта, что вывод формулы А из множества Г является выводом А из множества Δ, т. к. Δ .
2) пусть Г|-А , тогда конечное подмножество Г’ множества Г такое, что Г’|-А . Это следует из того, что для формулы А по определению вывод конечен, поэтому кол-во используемых гипотез Г в этом выводе конечно, это множество и есть то конечное множество Г’ из которого следует формула А.
3) пусть Г|-А и каждая F из Г есть следствие формул Δ. Δ |-F , следовательно А есть следствие формул Δ : Δ |-A . Это следует из того, что в выводе формулы А из множества Г каждую гипотезу Г можно заменить их выводами из формул Δ , тогда получим вывод А из множества гипотез Δ.
Теперь рассмотрим конкретное исчисление- исчисление высказываний.
1) символы исчисления высказываний есть счетная последовательность , бинарная связка ® (семантически это фукция следствия) ; унарная связка (семантически это отрицание переменной); скобки (;).
2) выражения есть любые конечные последовательности символов исчисления
3) формулы (правильно построенные выражения).
Индуктивное Определение
пусть - переменная, тогда - есть формула..
Пусть - формулы, тогда выражения вида- , также являются формулами.
4) аксиомы исчисления:
для любых формул A,B,L
6) правила вывода:
Modus ponens (MP): , для любых формул .
Построенное исчисление будет задавать множество тавтологий. Т.е. множество теорем ИВ и множество тождественно истинных в логическом смысле формул в базисе - есть одно и тоже множество.
Каждой построенной формуле нашего исчисления будет соответствовать логическая функция в базисе .
Тавтологией назовем функцию, которая на всех наборах принимает значение 1.
Утверждение
Каждая теорема ИВ является тавтологией.
Доказательство
Чтобы это показать, докажем вначале, что каждая аксиома тавтология. Затем покажем, что правило вывода сохраняет свойство тавтологии (т.е. непосредственное следсвие двух тавтологий- есть тавтология).
Каждая аксиома исчисления высказываний является тавтологией.
Допустим противное: существует набор, при котором
тогда
противоречие . Покажем, что a2 тавтология, допустим противное
Правило МР сохраняет свойство формулы быть тавтологией, то есть непосредственное следствие двух тавтологий есть тавтология.
|-B
Доказательство:
Рассмотрим тавтологию А и , покажем что формула В - есть тавтология. Допустим противное:
, т.к. А тавтология, не является тавтологией, получили противоречие, что и требовалось доказать.
Теоремы исчисления высказываний есть тавтологии. Аксиомы- есть тавтологии, а следствия из этих аксиом тогда также будут тавтологией в силу того, что МР сохраняет свойство тавтологии. Утверждение доказано.
Справедливо обратное утверждение.
Утверждение
Любая тавтология в базисе - есть теорема исчисления высказывания.
Перед доказательством этого утверждения необходимы некоторые рассуждения. Построим вывод некоторых теорем.
Аксиомы:
1) В исчислении высказываний выводима . Запишем аксиому а2 в виде
, заменив L на А и В на , тогда видно, что левая часть данной формулы (посылка) есть аксиома а1 ( вместо В подставлена ). Тогда по правилу вывода из этих двух формул- аксиом воводима правая часть (следствие):
,
Левая часть выведенной формулы есть аксиома а1, где вместо В стоит А, поэтому из предыдущей формулы по правилу МР выводима правая часть формулы.
Это и есть требуемая теорема.
Предложение 1:
Из формулы А для любой формулы В выводима В®А
Доказательство:
и а1, по правилу МР выводима правая часть.
Из формулы А выводима любая формула, где А стоит в правой части.
Теорема дедукции:
Из множества гипотез и формулы А выводима В , тогда из множества выводима .
Доказательство:
Пусть вывод формулы В из множества гипотез . Индукцией по докажем, что из множества гипотез выводима формула :
При В1 есть либо одна из гипотез Г либо аксиома, либо формула А. В первых двух случаях данное утверждение следует из предложения. В оставшемся случае выводимая формула принимает вид . Но эта теорема в исчислении, следовательно доказательство при j=1 завершено.
Пусть утверждение верно для всех . Докажем утверждение для : Вk есть либо одна из гипотез Г , либо аксиома, либо формула А, либо следуетпо правилу вывода из некоторых предыдущих формул Вj, Bs, где Bs имеет вид по правилу вывода . В первых трех случаях доказательство такое же, как и для j=1 . В оставшемся случае применим предположение индукции и аксиому а2: а именно: из предположения индукции следует, что из гипотез выводятся формулы и , т.е. .
Рассмотрим аксиому а2 в виде , тогда в силу того, что из множества гипотез выводится левая часть этой аксиомы, то тогда в силу МР выводится и правая часть этой аксиомы. В силу того, что из множества гипотез выводится левая часть полученной правой части, то выводится и правая часть:
Т.о. из множества гипотез выводится формула . Теорема дедукции.
Семь теорем.
2) . Запишем аксиому а3 в следующем виде: вместо В подставим формулу А, а вместо А подставим
1. примем двойное отрицание А за гипотезу, тогда по предположению выводится
2. Теперь из пунктов 1 и 2 выводится правая часть формулы
3. (теорема 1)
4. следовательно по т1 и 3 выводится
5. по теореме дедукции
3) Запишем аксиому а3, подставив вместо В , тогда а3=
1. по 2) и 1 выводится правая часть
2.
3. принимаем А за гипотезу, тогда по пр. из пунктов 2, 3 по МР
4.
5.
4) запишем третью аксиому а3
1.
2.
3.
4. (пр.)
5.
6.
7. применяя ТД второй раз получаем
5) запишем аксиому а3
1.
2.
3.
4.
5.
6. применяя ТД дважды, получаем требуемую формулу
6)
1. Запишем предыдущую теорему в виде гипотеза
Примем за гипотезу, и выведем из нее посылку . Тогда
вывод теоремы непосредственно следует из теоремы дедукции и теоремы 5.
Чтобы реализовать указанную цель, принимаем за гипотезу.
Тогда
2. ,
3
4 из пунктов 2,3 получаем , |-
Тогда цель выполнима по теореме дедукции из предыдущегопункта 4.
7) запишем а3
1.
2. запишем 6) в следующем виде:
3. по МР, следовательно по ТД из
4.
5. по ТД
8) запишем а3
1.
2. покажем предыдущие
3.
4.
5. , таким образом второй пункт доказан
6.
7.
8. ТД первый раз
ТД второй раз