1611678200-36438fb4f1ee6f855c93dc4a315ea8eb (826633), страница 10
Текст из файла (страница 10)
Приведем новые определениялогических операций, соответствующих правиламПравило1.1-10.Конъюнкция определяется как тождественноложнаяфункция.Правило2.Значениеконъюнкциих/\уравнозначениювторогоконъюнкциих/\уравнозначениюпервогодизъюнкцииxVyравнозначениювторогочлена у.Правило3.Значениечленах.Правило4.Значениечлена у.1)См. также упражнение 1 к § 1.8.Гл.461.Исчисление высказыванийПравило5.Значение дизъюнкции х V у равно значению первогоПравило6.Дизъюнкция определяется как тождественно истиннаячленах.функция.ПравилоИмпликация определяется как тождественно ложная7.функция.ПравилоИмпликация определяется как тождественно истинная8.функция.ПравилоОтрицание9.определяетсякактождественноложнаяфункция.Правило10.Отрицание определяется как тождественно истиннаяфункция.Правило11.Характеристическое свойство секвенции Гв следующем: если ГФ1Правило12.f-= Ф1, ...
, Фn,п;;,,l,Ф состоитf-то секвенцияФ доказуема в ИВ.Характеристическое свойство секвенции ГФ состоитf-в том, что Г одноэлементно или пусто.ОУпражненияl.Пусть формула Ф ИВ находится в д. н. ф. и Х-множествоее пропозициональных переменных. Для того чтобы Ф была доказуемой в ИВ,необходимо и достаточно, чтобы для любогоразбиения множества Х на два множества: Х1, Х2, существовала бы формула Ф Е D(Ф),K(w)~ {Рчто выполнялось бы включениеI РЕ Х1} u {~Р I РЕ Х2}.(Указание.
Применитьтеорему о полноте ИВ.)2.Провестинеобходимуюпроверкув доказательстве предложения§ 1.8.характеристическихсвойствl. 7.4.Исчисление высказываний гильбертовскоготипаВ этом параграфе мы рассмотрим другую, так называемую гильбертовскую, аксиоматизацию исчисления высказыванийОпределение. Понятие формулы в ИВ,-ИВ 1 .то же, что и в ИВ, заисключением того, что в алфавите ИВ 1 нет символа логической константы; секвенций в ИВ, также нет. Аксиомы ИВ,следующих10схем подстановкойпеременных Ф, Ф, Х:l.2.получаются изконкретных формул ИВ,Ф----. (Ф----.
Ф),(Ф----. Ф)----. ((Ф----. (Ф----. Х))----. (Ф----. Х)),вместо§ 1.8.3.4.5.6.7.8.9.10.(ФА Ф)Исчисление гильбертовского типа47Ф,-(ФАФ)-Ф,Ф -(Ф -(ФА Ф)),Ф-(ФVФ),Ф- (Ф V Ф),(Ф - Х) (Ф ~~ФФ)((Ф - Х) -((Ф V Ф) - Х)),- ((Ф - ~w) - ~Ф),Ф.-Правило вывода в ИВ 1 одно:Ф,Ф-ФwОпределение. Доказательством в ИВ1 формулы Фп называетсятакая последовательность Фо,i ::::; п, либоj, k < i, по...
, ФпформулИВ1, что каждая Фi,является аксиомой, либо получена из некоторых Фj, Фk,правилу вывода. Если существует доказательство в ИВ1формулы Ф, то Ф называется доказуемой в ИВ1 и обозначается этотак: 1> Ф. Выводом в ИВ1 формулы Фп из множества Н формулИВ~ называется такая последовательность Фо,каждая Фi,i::::; п,... , Фпформул ИВ~, чтолибо является аксиомой, либо принадлежит Н, либополучается из некоторых Фj, Фk,j, k < i, по правилу вывода. Еслисуществует вывод формулы Ф из Н, то Ф называем выводимой в ИВ1из Ни пишем Н 1> Ф, при этом Н называется множеством гипотез.Очевидно, что доказуемость Ф в ИВ~ равносильна выводимости Ф вИВ~ из пустого множества гипотез.
Отметим, что множество гипотез Нне обязано быть конечным, но если Н1> Ф, то в силу конечностивывода Ф из Н существует конечное множество Н1 ~ Н, для которогоН 1 1> Ф. Очевидно также, что если Н ~ Н' и Н 1> Ф, то Н' 1> Ф.Основной целью данного параграфа является доказательство следующей теоремы, которая показывает в определенном смысле равносильность ИВ и ИВ~.Теорема. . .
Фп} 1> ФФ1, ... , Wn f--1.8.1. Дляформул Ф~,... Фп, ФИВ~ выводимость {Ф1,...имеет место тогда и только тогда, когда секвенцияФ доказуема в ИВ.Прежде чем приступить к доказательству теоремыl .8. l,мы разовьем некоторую теорию выводимости в ИВ~.Пример1.8.2. Пусть Ф - формула ИВ~. Последовательность из5 формул будет доказательством формулы Ф - Ф в ИВ1:l) Ф - (Ф - Ф) - аксиома,2) Ф - ((Ф - Ф) - Ф) - аксиома,следующихГл.483)4)5)1.Исчисление высказываний(Ф--.
(Ф--. Ф))--. ((Ф--. ((Ф--. Ф)--. Ф))--. (Ф--. Ф))- аксиома,- правило вывода к 1) и 3)(Ф--. ((Ф--. Ф)--. Ф))--. (Ф--. Ф)Ф--. Фправило вывода к-2)и4).Правило выводаФо,... , Фkwназывается допустимым в ИВ1, если его добавление к исчислениюИВ 1 не увеличивает семейство выводимых из Н формул для любогомножества гипотез Н.Квазивыводом вИВ1формулы Фпиз множества гипотез Нназывается такая последовательность формул Фо,Фi,i : :;_;... , Фп,что каждаяп, либо выводима в ИВ 1 из Н, либо получается из некоторыхпредыдущих по допустимому в ИВ1 правилу вывода.
Очевидно, чтоесли имеется квазивывод в ИВ1 формулы Ф из множества Н, то Фвыводима в ИВ1 из Н.Теорема1.8.3(о дедукции вИВ1).ЕслиНU {Ф}[> Ф,тоН [> Ф--. Ф.Д о к аз ат ель ст в о проведем индукцией по минимальному п, длякоторого существует вывод Фо,п=О, то либо1) Ф=В первом случае, в силу... , Wn формулы Ф из Н U { Ф }. Если2) Ф - аксиома или входит в Н.примера 1.8.2, формула Ф --. Ф выводима из Н.Ф, либоВо втором случае последовательностьw, w--.
(Ф--. Ф),Ф--. Фбудет выводом в ИВ 1 из Н. Пусть п > О. Из минимальности п имеем,что Ф получается из Фi и Wj(wi--. Ф) для i,j < п по правилу=вывода. Тогда в силу индукционного предложения последовательностьФ--.(Ф - wi) (Ф--.будет квазивыводом Фwi,Ф--.(wi--.
w),((Ф - (wi -(wi--.--.Ф)) -(Ф - Ф)),Ф))--. (Ф--. Ф), Ф--. ФоФ из Н.Теорема о дедукции существенно облегчает для многих формул ИВ1установление их доказуемости в ИВ1.Следствие--. ...(Фп--. Ф)1.8.4. { Фо, ... , Фп}... ).[> Фравносильно [> ФоДо к аз ат ель ст в о. В одну сторону по дедукции. В другую п+ 1 раз+ 1 раз--. ( Ф1 --.применяем теоремуприменяем правило вывода.О§ 1.8. Исчисление гильбертовского типа49Доказательствотеоремы l.8.l.
В силу правил 7 и 8 ИВ... , Ф n f- Ф доказуема в ИВ тогда и только тогда, когдадоказуема f- Ф1 --+ (Ф2 --+ ... (Фn --+ Ф) ... ). Тогда из следствия l.8.4секвенция Ф 1,получаем, что для доказательства необходимости можно ограничитьсяслучаем Г=121.Легкопроверить,что аксиомы ИВ 1тождественноистинны, а правила вывода ИВ1 сохраняют тождественную истинность.Поэтому необходимость следует из теоремы о полноте ИВ.Достаточность. Пусть деревоции Гf-Ф. Если ГФf-D -доказательство в ИВ секвен- аксиома ИВ, то Г=Фи утверждение{ Ф}Ф[>D1 получается из D заменой логической константы Jна формулу Qo /\ ·Qo. Ясно, что начальные секвенции в D1 останутсяочевидно.
Пустьаксиомами, а переходы по правилам, отличным от9ипереходами по тем же правилам. Переходы по правилам10, останутся9 и l О станутпереходами по правилам9,.Г, ·ФlO'. Г f- Ф; Г f- ·Ф.Г f- Qo /\ ·Qof- Qo /\ ·Qof- ф'гПоэтому осталось показать, что если в правилах вывода l -8 и l l,12 исчисления ИВ и правилах 9' и 10' заменить выражения 0 f- Ф на{ 0} [> Ф, то из истинности утверждений над чертой будет следоватьистинность утверждения под чертой. Что касается применений правилl -5,то сохранение истинности соответствующих утверждений легкополучить, используя аксиомы{Г, Ф2} [> Ф; {Г} [> Ф1{Г} [> Ф2--+3-7исчисления ИВ1. Пусть {Г, Ф1}V Ф2. По теореме о дедукции {Г}[>Ф;[> Ф1Ф.
Применяя три раза правило вывода ИВ1 к--+ Ф иаксиоме 8,получаем {Г} [> Ф. Следовательно, переход, полученный из примененияправила6,сохраняет выводимость. Правилоо дедукции, правило8 -7соответствует теоремеправилу вывода ИВ1.Докажем сохранение выводимости переходом, полученным из применения правилачаем {Г, ·ф} [>{Г} [> ·ф9'.Qo--+ Qo иПусть {Г, ·ф} [>Qo /\ ·Qo. Из аксиом 3·Qo. По теореме о дедукции--+ ·Qo. Тогда из аксиомы 9и4полуи {Г, ·ф} [>получаем{Г} [> ·фполучаем{Г} [> "Ф и по аксиомеРассмотрим правило1010'.и правилу вывода получаем {Г} [> Ф.Пусть {Г} [> Ф и {Г} [> ·Ф. Из аксиомыполучаем{Г} [> Ф--+('(Qo /\ 'Qo)--+ Ф)и{Г}[>'Ф--+('(Qo /\ 'Qo)--+ 'Ф).По правилу вывода получаем{Г} [> • ( Qo/\ ·Qo) --+ФlГл.501.Исчисление высказыванийи{Г}Из аксиоми910~(Qo /\ ~Qo)-+1>~Ф.тогда получаем выводимость {Г} 1>l 1 и 12Сохранение выводимости правиламиQo /\ ~Qo.следует непосредственноиз определения вывода в ИВ1.ОУпражненияДоказать независимость ИВ1.
(Указание. Использовать тот жеl.метод, что и для ИВ. Для доказательства независимости схеми2логические связки определяются на множестве {О,l, 2},l связки определяются так: п /\ т = min{n, m}, п V m = max{n, m}, ~о= ~1 == 2, ~2 = О, (п-+ т) = 2, если п ~ т, и (п-+ т) = О, еслип > т. Для схемы 2 имеем (0/\m) = (m/\0) = l, (OVO) = l,~2 = l, (О-+ О)= (2-+ О)= (2-+ l) = l, (l-+ О)= 2, а остальные значения связок как для схемы l. Характеристическоеlа схем3- l О -на множестве{ О, l}.Для схемысвойство формул при доказательстве независимости схемтождественное равенство2.иl2-2.)Рассмотрим исчисление ИВ2, отличающееся от ИВ1 тем, что в егоформулы может входить логическая константаиJ,а аксиомы910 заменены на следующие:9'. СФ -+ J) -+ Ф,10'.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
