Верещагин Н.К., Шень А. - Языки и исчисления

ЛЕКЦИИ ПО МАТЕМАТИЧЕСКОЙ ЛОГИКЕИ ТЕОРИИ АЛГОРИТМОВН. К. Верещагин, А. ШеньЯЗЫКИ И ИСЧИСЛЕНИЯИздание четвёртое, исправленноеМоскваИздательство МЦНМО, 2012УДК 510.6ББК 22.12В31В31Верещагин Н. К., Шень А.Лекции по математической логике и теории алгоритмов.Часть 2. Языки и исчисления. — 4-е изд., испр. — М.: МЦНМО,2012.

— 240 c.ISBN 978-5-4439-0013-1Книга написана по материалам лекций и семинаров, проводившихсяавторами для студентов младших курсов мехмата МГУ. В ней рассказывается об основных понятиях математической логики (логика высказываний, языки первого порядка, выразимость, исчисление высказываний,разрешимые теории, теорема о полноте, начала теории моделей). Изложение рассчитано на учеников математических школ, студентов-математиков и всех интересующихся математической логикой.

Книга содержитоколо 200 задач различной трудности.Предыдущее издание книги вышло в 2008 г.ББК 22.12Тексты, составляющие книгу, являются свободнораспространяемыми и доступны по адресуftp://ftp.mccme.ru/users/shen/logic/firstordНиколай Константинович ВерещагинАлександр ШеньЛекции по математической логике и теории алгоритмов.Часть 2. Языки и исчисленияПодписано в печать 11.04.2012 г. Формат 60 × 90 1/16. Бумага офсетная.Печать офсетная. Печ. л. 15,0. Тираж 1000 экз. Заказ №Издательство Московского центранепрерывного математического образования.119002, Москва, Б. Власьевский пер., 11.

Тел. (499) 241–74–83.Отпечатано с готовых диапозитивов в ППП «Типография Наука“ ».”121099, Москва, Шубинский пер., 6.ISBN 978-5-4439-0013-1c Верещагин Н. К.,Шень А., 2000, 2012ОглавлениеПредисловие51. Логика высказываний81.1. Высказывания и операции . . . . . . . . . . . . . . .

. . 81.2. Полные системы связок . . . . . . . . . . . . . . . . . . 151.3. Схемы из функциональных элементов . . . . . . . . . . 222. Исчисление высказываний2.1.2.2.2.3.2.4.40Исчисление высказываний (ИВ) . . . . . . . . .Второе доказательство теоремы о полноте . . .Поиск контрпримера и исчисление секвенций .Интуиционистская пропозициональная логика....................3. Языки первого порядка723.1. Формулы и интерпретации .

. . . . . . . .3.2. Определение истинности . . . . . . . . . .3.3. Выразимые предикаты . . . . . . . . . . .3.4. Выразимость в арифметике . . . . . . . .3.5. Невыразимые предикаты: автоморфизмы3.6. Элиминация кванторов . . . . . . . . . . .3.7. Арифметика Пресбургера . . . . . . . .

.3.8. Теорема Тарского – Зайденберга . . . . . .3.9. Элементарная эквивалентность . . . . . .3.10. Игра Эренфойхта . . . . . . . . . . . . . .3.11. Понижение мощности . . . . . . . . . . . .........................................................................................4. Исчисление предикатов4.1.4.2.4.3.4.4.4.5.4.6.4.7.4.8.4.9.Общезначимые формулы . .

. . . . . .Аксиомы и правила вывода . . . . . .Корректность исчисления предикатовВыводы в исчислении предикатов . . .Полнота исчисления предикатов . . .Переименование переменных . . . . . .Предварённая нормальная форма . . .Теорема Эрбрана . . . . . . . . . . . .Сколемовские функции . . . . . . . .

.4048535872768082868998101111116122128..........................................................................................1281301361391461541571601634Оглавление5. Теории и модели5.1. Аксиомы равенства . . . . . . . . .5.2. Повышение мощности . . . . . . . .5.3. Полные теории . . . . . . . . . . . .5.4. Неполные и неразрешимые теории5.5. Диаграммы и расширения . . . . .5.6. Ультрафильтры и компактность .5.7.

Нестандартный анализ . . . . . . .....................................................................................167167170174185194201209Литература224Предметный указатель228Указатель имён237ПредисловиеНашему учителю,ВЛАДИМИРУ АНДРЕЕВИЧУ УСПЕНСКОМУПредлагаемая вашему вниманию книга написана по материаламлекций для младшекурсников, которые читались авторами в разные годы на механико-математическом факультете МГУ. (В эту серию также входят книги «Начала теории множеств» и «Вычислимыефункции».)Центральная идея математической логики восходит ещё к Лейбницу и состоит в том, чтобы записывать математические утверждения в виде последовательностей символов и оперировать с ними поформальным правилам.

При этом правильность рассуждений можнопроверять механически, не вникая в их смысл.Усилиями большого числа математиков и логиков второй половины XIX и первой половины XX века (Буль, Кантор, Фреге, Пеано, Рассел, Уайтхед, Цермело, Френкель, Гильберт, фон Нейман,Гёдель и другие) эта программа была в основном выполнена. Принято считать, что всякое точно сформулированное математическоеутверждение можно записать формулой теории множеств (одной изнаиболее общих формальных теорий), а всякое строгое математическое доказательство преобразовать в формальный вывод в этой теории (последовательность формул теории множеств, подчиняющуюсянекоторым простым правилам). В каком-то смысле это даже сталоопределением: математически строгим считается такое рассуждение,которое можно перевести на язык теории множеств.Так что же, теперь математики могут дружно уйти на пенсию,поскольку можно открывать математические теоремы с помощьюкомпьютеров, запрограммированных в соответствии с формальнымиправилами теории множеств? Конечно, нет, причём сразу по нескольким причинам.Начнём с того, что машина, выдающая с большой скоростью математические теоремы (и их доказательства), хотя и возможна, нобесполезна.

Дело в том, что среди этих верных утверждений почтивсе будут неинтересными. Формальная логика говорит, какие правила надо соблюдать, чтобы получать верные результаты, но не говорит, в каком порядке их надо применять, чтобы получить что-тоинтересное.6ПредисловиеКазалось бы, мы можем запустить машину и ждать, пока она недокажет интересующее нас утверждение (пропуская все остальные).Проблема в том, что формальное доказательство сколько-нибудь содержательной теоремы настолько длинно, что прочесть его человекне в состоянии. Представьте себе доказательство, которое состоитиз миллионов формально правильных шагов, в котором мы можемпроверить каждый отдельный шаг, но так и не понимаем, что происходит — много ли в нём проку?На самом деле прок всё-таки есть: мы узнаём, что доказываемоеутверждение верно, хотя так и не понимаем, почему. Так что и такаямашина была бы полезна.

Увы, и этого сделать не удаётся, посколькуна поиск доказательства сколько-нибудь сложного утверждения известными сейчас методами требуется астрономически большое время (даже если представить себе, что машина работает с предельновозможной по законам физики скоростью).Можно умерить амбиции и поставить задачу попроще: пусть машина проверяет доказательства, записанные человеком по правиламформальной логики. Если машина не может помочь нам что-то открыть, пусть она хотя бы проверит, не пропустили ли мы какого-тошага рассуждения.Из всех перечисленных задач эта выглядит наиболее реалистичной. К сожалению, пока что работы и в этом направлении не ушлидалеко: формальная запись доказательства в виде, пригодном длямашинной проверки, является долгим и скучным делом, на котороеу большинства математиков не хватает энтузиазма и терпения.

Аразработать удобные средства такой записи пока не удалось.Короче говоря, революционная программа Лейбница построенияформальных оснований математики осуществилась, но незаметно:под здание математики подвели новый (и довольно прочный) фундамент, но большинство жильцов про это до сих пор не знают.Так что же, математическая логика бесполезна? Ни в коем случае: она не только удовлетворяет естественный философский интерес к основаниям математики, но и содержит множество красивыхрезультатов, которые важны не только для математики, но и дляcomputer science.В этой книжке мы расскажем об одном из центральных понятийматематической логики — языках и исчислениях первого порядка.В этих языках используются логические связки «и», «или», «если.

. .то. . . », а также кванторы «для всех» и «существует». Оказывается, что этих средств достаточно для формализации математическихПредисловие7теорий и что можно построить простые формальные правила, полностью отражающие смысл этих логических средств.Авторы пользуются случаем ещё раз поблагодарить своего учителя, Владимира Андреевича Успенского, лекции, тексты и высказывания которого повлияли на них (и на содержание этой книги),вероятно, даже в большей степени, чем авторы это осознают.При подготовке текста использованы записи А. Евфимьевскогои А. Ромащенко (который также прочёл предварительный варианткниги и нашёл там немало ошибок).Оригинал-макет книги был подготовлен В. В. Шуваловым; без егонастойчивости (вплоть до готовности разделить ответственность заошибки) оригинал-макет вряд ли появился бы к какому-либо сроку.Он же вместе с М.

А. Ушаковым (нашедшим несколько существенных ошибок) подготовил предметный указатель. Мы признательнытакже К. С. Макарычеву и Ю. С. Макарычеву, которые внимательнопрочли вёрстку книги и нашли там немало опечаток.Авторы признательны École Normale Supérieure de Lyon (Франция) за поддержку и гостеприимство во время написания этой книги.Первое издание книги стало возможным благодаря Российскомуфонду фундаментальных исследований, а также И. В. Ященко, который уговорил авторов подать туда заявку.Наконец, мы благодарим сотрудников, аспирантов и студентовкафедры математической логики мехмата МГУ (особая благодарность — М. Р. Пентусу, указавшему два десятка опечаток), а такжевсех участников наших лекций и семинаров и читателей предварительных вариантов этой книги.В третьем издании добавлены формулировка и доказательствотеоремы Чёрча о неразрешимости исчисления предикатов (по ошибке отсутствовашие в предыдущих изданиях), а также дополнена информация в именном указателе.

В четвёртом издании, помимо изменения формата вёрстки и использования шрифтов LH, исправленынекоторые опечатки (на которые нам любезно указали Н. Маслов,А. Гусаков, В. Патков).Просим сообщать о всех ошибках и опечатках авторам (электронные адреса ver at mccme dot ru, nikolay dot vereshchagin at gmaildot com; sasha dot shen at gmail dot com, alexander dot shen at lirmmdot fr; почтовый адрес: Москва, 119002, Большой Власьевский пер.,11, Московский центр непрерывного математического образования).Н.

К. Верещагин, А. Шень1. Логика высказываний1.1. Высказывания и операции«Если число π рационально, то π — алгебраическое число. Нооно не алгебраическое. Значит, π не рационально.» Мы не обязанызнать, что такое число π, какие числа называют рациональными икакие алгебраическими, чтобы признать, что это рассуждение правильно — в том смысле, что из двух сформулированных посылокдействительно вытекает заключение. Такого рода ситуации — когданекоторое утверждение верно независимо от смысла входящих в неговысказываний — составляют предмет логики высказываний.Такое начало (особенно если учесть, что курс логики входил впрограмму философского факультета, где также изучалась «диалектическая логика») настораживает, но на самом деле наши рассмотрения будут иметь вполне точный математический характер, хотямы начнём с неформальных мотивировок.Высказывания могут быть истинными и ложными.