Кузнецов О.П., Адельсон-Вельский Г.М. - Дискретная математика для инженеров (1048837), страница 48
Текст из файла (страница 48)
Прн доказательстве теоремы используются следующие производные п р а в и л а: 232 1) если [ — А В, то[ — А-«С В- С и С вЂ” А С- В; 2) если [ — А В, то [ — А~УС В'~~С и 1 — С~/А С УВ1 3) если [- А-В, то [ — АЬС-ВйС и 1 — СЬА СМВ; 4) если [ — А - В, то [ — ' ) А - 1В; 5) если [ — Р(х) -6(х), тотухР(х) ух6(х); б) если [ — Е(х) 6(х), то ВхР(х) -лх6(х). Первые четыре правила легко проверяются с помо щью таблиц истинности. Доказательство последних двух пра- вил можно найти, например, в [25). С помощью этих шести правил теорема 6.7 доказывается индукцией по построению формулы Г(А): показывается, что если А В, то эта эквивалентность сохраняется на всех шагах построения Р(А) из А и Р(В) из В. П Продемонстрируем это доказательство на примере.
Пусть Р(А) = )уу(Р,(ч)~/ ",.дхРз(х, у)), А=,ухРз(х, р). В качестве эквивалентности А — В возьмем эквивалент- ность ~дхРз(х, у) тух 1Рг(х, у), верную в логике преди- катов [см. соотношение (3.31)) и, следовательно, в силу тео- ремы 5.7 доказуемую в исчислении предикатов. 1, ')дхРз(х, у) т(х [Рз(х, у) (исходная эквивалент- ность 'А В), 2. (Р Ь)~/ )дхР (х, д))-(Р,(д)~~х-[Р,(,,~)) (пр,. вило 2). 3.
~гу(Р,(п) \/ ~ВхРз(х, у)) т)у(Р,(у)~/ух ) Рз(х у)) (правило 5). Формула из шага 3 и есть искомая эквивалентность Р(А) -Р(В). Приведем теперь без доказательства некоторые важные эквивалентности, выводимые в исчислении предикатов (в них А и  — формулы, не содержащие свободных вхож- дений х): А й т7хР (х) — тух(А сг Р (х)); А ',/ лхР(х) — дх(А ~/ Г(х)); А Ь лхР (х) — пх (А й Е (х)); А ',~ тгхГ (х) — тгх (А ~у Р (х)); А -«АР (х) — ух (А-«Р (х)); А-«дхР (х) — пх (А — «Р (х)); ь хР (х)-«В Вх (Р (х)-«В)); АР (х) —  — 1гх (Р (х) — «В)).
Эквивалентности (6.5) — (6.12), а также полученные ранее эквивалентности (З.ЗЗ) и (3.34) позволяют выносить кванторы вперед. Используя при этом соотношения (3.31) и (3.32), позволяющие заменять один квантор другим и «спускать» отрицание внутрь области действия квантора, а также правила переименования переменных (примеры 6.3, а, б), кванторы можно вынести вперед для любой формулы.
Формула, имеющая вид Я,хД,хь..Я„х„Р, где Яь ... ..., Я, — кванторы, а Р— формула, не имеющая кванторов (н являющаяся областью действия всех и кванторов), называется предвареиной формой, или формулой в предвареиной форме, В исчислении предикатов для любой формулы Р существует эквивалентная ей предваренная форма Е', т. е. [ — Р-Р'. Пример 6.4. а. Приведем к предваренной форме формулу, которой была проиллюстрирована теорема 6.7: 1.
гу(Р, (у) ~/ ~дхР,(х, у) ); 2. туу(Р,(у) ~/ух ~Р,(х, у)) [по соотношению (3.31)1; 3. МУг(х(Р,(У) '/ ~Р,(х, У)) [по соотношению (68)1. б. Проделаем то же самое с несколько более сложной формулой: 1, УхР, (х) — ь. ~)~х(Р~(У)'/ВУРз(х, У)) 2. тгхР,(х)- ~ 4х(Р,(г)'»гВУР,(х, У)) (переименование свободной переменной); 3. мхР, (х)-+. -дхВУ(Р,(х) ~/Р,(х, У)) [соотношение (6.6)1; 4, 5.
мхР,(х) — »пх)(У ', (Р,(х)УР,(х, У)) [здесь объединены два шага вывода: применение (3.31), а затем (3.32)1; 6. миР,(и) — »дх1уу ) (Р,(г)~/Р,(х, У)) (переименование связанной переменной); 7, 8, 9 дхпитгу(Р,(и) — ) (Р,(г)'»гР,(х, У)) [здесь объединены три шага вывода: применения (6.10), (6.11), (6.9)1. Теории первого порядка (прикладные исчисления предикатов). Исчисления с равенством. Формальная арифметика, Построенное ранее исчисление предикатов называется исчислением предикатов первого порядка. В исчислениях второго порядка возможны кванторы по предикатам, т. е.
выражения вида тгР(Р(х) ). Приложения таких исчислений встречаются гораздо реже; в этой книге исчисления второго порядка рассматриваться не будут. Исчисление предикатов, не содержащее функциональных букв и предметных констант, называется чистым исчислени- 234 ем предикатов. Па существу до сих пор рассматривалось именно чистое исчисление предикатов, хотя язык исчисле- ния (т. е. формулы) был определен с учетом его использо- вания в прикладных исчислениях. Прикладные исчисления (теории первого порядка) ха- рактеризуются тем, что в них к чисто логическим аксиомам добавляются собственные аксиомы, в которых, как правило, участвуют конкретные (индивидуальные) предикатиые бук- Вы и предметные константы.
Типичные примеры индивиду- альных предикатных букв — предикаты =, (, функцио- нальных букв — знаки арифметических операций, предмет- ных констант — натуральные числа, единица в теории групп, пустое множество в теории множеств. Другая важная особенность прикладных исчислений за- ключается в том, что в схемах аксиом Р1 и Р2 участвуют уже не предметные переменные, а произвольные термы. Бо- лее точна эти схемы аксиом принимают следующий внд: РГ ЪхР (х) Г ()! Р2'. Е (!) — э-ВхР (х), 'где г(!) — результат подстановки терма ! в г(х) вместо всех свободных вхождений х, причем все переменные ! должны быть свободными в г'(!) . Большинство прикладных исчислений содержит преди- кат равенства = и определяющие его аксиомы. Аксиомами для равенства могут служить следующие.
Е1. тгх(х=х) (конкретная аксиома); Е2, (х=у)- (е(х„х)- г(х, у) ) (схема аксиом), где г (х, у) получается из г'(х, х) заменой некоторых (не обязательно всех) вхождений х на у прп условии, что у в этих вхождениях также остается свободным, Всякая тео- рия, в которой Е! и Е2 являются теоремами или аксиомами, называется теорией (или исчислением) с равенством. Дела в том, что из Е! и Е2 выводимы основные свойства равенст- ва — рефлексивность, симметричность и транзитивность, Теорема 6.8.
В любой теории с равенством: 1) ) — (=! для любого терма (; 2) ! — х=у — эу х; 3) )-х=у '(у=г-~х=я) Доказательство. 1. Непосредственно следует из аксиом Е! и Р1' (где Р(х) имеет вид х=х) по правилу заключения. 2. Из Е2 имеем (х=у)- (х=х-+у=х), Отсюда х=у, х = х! — у = х (двойное применение правила заключения). Но так как [ — х=х, то х=у[ — у=х и, следовательно, по теореме дедукции' х=у- у=х. 3. Поменяем местами в Е2 х н у, в качестве Р(у, у) возьмем у=г, а в качестве Р(у, х) возьмем х=г.
Получим у=х-+(у=г х=г) и по правилу заключения у=х)-(у= =г — х=г). Но так как в силу п. 2 х=у[-у=х, то по транзитивпости выводимости (см. 5 6.1) получаем х=у~ — (У= =г- х=г) и по теореме дедукции х=у-м(у=г- х=г). П Три свойства равенства, полученные этой теоремой, верны, как известно, для любого отношения (и, следовательно, соответствующего предиката) эквивалентности (см, гл. 1). Схема аксиом Е2 выражает более сильное свойство, присущее лишь равенству: неотличнмость элементов, для которых выполняется равенство. Другой пример прикладного исчисления — теория частичного строгого порядка, содержащая две конкретные аксиомы для предиката ХЕ1. Тсх ", (х<х); КЕ2.
)ухтуутгг (х е., у-+-(у ( г — х ( г)), Читателя может удивить, что два сходных утверждения о транзитивности даются в разной форме: и. 3 теоремы 6.8 без кванторов, в открытой форме, а ХЕ2 — с кванторами, в замкнутой форме, В действительности эти два способа задания аксиом равносильны: от первого ко второму переходим по правилу обобщения, а от второго к первому — по аксиоме Р!' и правилу заключения, Если к ХЕ1 и ХЕ2 добавить аксиому с предметной константой КЕЗ~тх ] (х(а), то получим теорию частичного порядка с минимальным элементом а, Пожалуй, наиболее изученной формальной теорией, которая играет фундаментальную роль в основаниях математики, является формальная арифметика, Ее схемы аксиом (см.
[36] ): А1, Р(0) Ь (гх(Р(х)-ьР(х'))- Р(х) (принцип индукции); А2. 11 — — 1я-эдит = )а; АЗ, ~[1~ = О]; ' Теорема дедукции доказывалась ранее только для исчисления высказывания (для исчнсления прсдикатов она верна лишь прн некоторык ограничениях). Но данные формучы не содержат кнанторов, позтому зта теорема применима. 236 А4. 1 = 0 ~И, = !»~1, =- 1,); Аб.
1, = !» — «-1~ = !»; Аб, 1,+0=1,; А7. !» + !» (!» + !») ! А8. 1,0=0; А9. 1» 4г = 1,' !» + !ь В этих аксиомах использованы три функциональных сим. вола +, , ', один индивидуальный предикат (предикатная буква) и одна предметная константа О. Они придают схемам А2 — А9 вполне конкретный вид: все предикатные и функциональные буквы в них зафиксированы, и единственный способ их варьировать — это подставлять различные термы вместо метапеременных 1„1,. В частности, схемы Аб — А9 — это просто предикат равенства, в который подставлены термы определенного вида. Схема А1 имеет обычный вид: Р(х) — метаобозначение, употребляемое в том же смысле, в каком оно использовалось в чистом исчислении предикатов.