Часовой пояс: UTC + 3 часа [ Летнее время ]

Свойства формализованного исчисления предикатов
Онлайн-сервисы Нахождение НОД и НОК Разложение числа на простые множители Сравнения по модулю Операции над множествами Операции над векторами Разложение вектора по базису. Доказательство, что векторы образуют базис Чертёж треугольника по координатам вершин Решение треугольника Решение Пирамиды Построение Пирамиды по координатам вершин Чертёж многоугольника по координатам вершин Решение систем методом Крамера и Матричным Онлайн построение графика кривой 2-го порядка Определение вида кривой или поверхности 2-го порядка по инвариантам МНК и регрессионный анализ Онлайн + графики Онлайн число, сумма и дата прописью Алгоритмы JavaScript Алгоритмы поиска Алгоритмы сортировки Уникальные элементы массива Объединение, пересечение и разность массивов НОД и НОК Операции над матрицами Дата прописью Введение в анализ Функции: понятие, определение, графики Непрерывность функции Исследование функции и построение графика Теория множеств Множества: понятие, определение, примеры Точечные множества Замкнутые и открытые множества Мера множества Группы, кольца, поля в математике Поле комплексных чисел Кольцо многочленов Основная теорема алгебры и ее следствия Математическая логика Алгебра высказываний Аксиоматика и логические рассуждения Методы доказательств теорем Алгебра высказываний и операции над ними Формулы алгебры высказываний Тавтологии алгебры высказываний Логическая равносильность формул Нормальные формы для формул высказываний Логическое следование формул Приложение алгебры высказываний для теорем Дедуктивные и индуктивные умозаключения Решение логических задач Принцип полной дизъюнкции Булевы функции Множества, отношения и функции в логике Булевы функции от одного и двух аргументов Булевы функции от n аргументов Системы булевых функций Применение булевых функций к релейно-контактным схемам Релейно-контактные схемы в ЭВМ Практическое применение булевых функций Теория формального Формализованное исчисление высказываний Полнота и другие свойства формализованного исчисления высказываний Независимость системы аксиом формализованного исчисления высказываний Логика предикатов Логика предикатов Логические операции над предикатами Кванторные операции над предикатами Формулы логики предикатов Тавтологии логики предикатов Преобразования формул и следование их предикатов Проблемы разрешения для общезначимости и выполнимости формул Применение логики предикатов в математике Строение математических теорем Аристотелева силлогистика и методы рассуждений Принцип полной дизъюнкции в предикатной форме Метод полной математической индукции Необходимые и достаточные условия Логика предикатов и алгебра множеств Формализованное исчисление предикатов Неформальные и формаль- ные аксиоматические теории Неформальные аксиоматические теории Свойства аксиоматических теорий Формальные аксиоматические теории Формализация теории аристотелевых силлогизмов Свойства формализованного исчисления предикатов Формальные теории первого порядка Формализация математической теории Теория алгоритмов Интуитивное представление об алгоритмах Машины Тьюринга и тезис Рекурсивные функции Нормальные алгоритмы Маркова Разрешимость и перечислимость множеств Неразрешимые алгоритмические проблемы Теорема Гёделя о неполноте формальной арифметики Математическая логика и компьютеры Математическая логика и языки программирования Применение компьютеров для доказательства теорем математической логики Математическая логика и логическое программирование Математическая логика и информатика Математическая логика и искусственный интеллект Дискретная математика Множества и отношения Теория множеств: понятия и определения Операции над множествами Кортеж и декартово произведение множеств Соответствия и бинарные отношения на множествах Операции над соответствиями на множествах Семейства множеств Специальные свойства бинарных отношений Отношения эквивалентности на множестве Упорядоченные множества Теорема о неподвижной точке Мощность множества Парадокс Рассела Метод характеристических функций Группы и кольца Алгебраические структуры и операции Группоиды, полугруппы, группы Кольца, тела, поля Области целостности в теории колец Модули и линейные пространства Подгруппы и подкольца Теорема Лагранжа о порядке конечной группы Гомоморфизмы групп и нормальные делители Гомоморфизмы и изоморфизмы колец Алгебра кватернионов Полукольца и булевы алгебры Полукольца: определение, аксиомы, примеры Замкнутые полукольца Полукольца и системы линейных уравнений Булевы алгебры и полукольца Решетки и полурешетки Алгебраические системы Алгебраические системы: модели и алгебры Подсистемы алгебраических систем Конгруэнции и фактор-системы Гомоморфизмы алгебраических систем Прямые произведения алгебраических систем Конечные булевы алгебры Многосортные алгебры Теория графов Теория графов: основные понятия и определения Способы представления графов Неориентированные и ориентированные деревья Остовное дерево и алгоритм Краскала Методы систематического обхода вершин графа Алгоритмы поиска в глубину и ширину в графах Задача о путях во взвешенных ориентированных графах Изоморфизм, гомоморфизм и автоморфизм графов Топологическая сортировка вершин графа Элементы цикломатики в теории графов Булева алгебра и функции Булевы функции и булев куб Таблицы булевых функций и булев оператор Равенство булевых функций. Фиктивные переменные Формулы и суперпозиции булевых функций Дизъюнктивные и конъюнктивные нормальные формы Построение минимальных ДНФ Теорема Поста и классы Критерий Поста Схемы из функциональных элементов Конечные автоматы и регулярные языки Конечные автоматы и регулярные языки Алфавит, слово, язык в программировании Порождающие грамматики (грамматики Хомского) Классификация грамматик и языков Регулярные языки и регулярные выражения Конечные автоматы Допустимость языка конечным автоматом Теорема Клини Детерминизация конечных автоматов Минимизация конечных автоматов Лемма о разрастании для регулярных языков Обоснование алгоритма детерминизации автоматов Конечные автоматы с выходом Морфизмы и конечные подстановки Машины Тьюринга Контекстно-свободные языки Контекстно-свободные языки и грамматики Приведенная форма КС-грамматики Лемма о разрастании для КС-языков Магазинные автоматы (автомат с магазинной памятью) Алгоритм построения МП-автомата по КС-грамматике Алгоритм построения КС-грамматики по МП-автомату Алгебраические свойства КС-языков Основное свойство суперпозиции КС-языков Пересечение контекстно-свободных языков Методы синтаксического анализа КС-языков Восходящий синтаксический анализ и LR(k)-грамматики Семантика формальных языков Принцип индукции по неподвижной точке Графовое представление МП-автоматов Интегральное исчисление Неопределённый и определённый Неопределенный и определенный интегралы Свойства интегралов Интегрирование по частям Интегрирование методом замены переменной Интегрирование различных рациональных функций Интегрирование различных иррациональных функций Интегрирование различных тригонометрических функций Определенный интеграл и его основные свойства Необходимое и достаточное условие интегрируемости Теоремы существования первообразной Свойства определенных интегралов Несобственные интегралы Интегральное определение логарифмической функции Приложения интегралов Вычисление площадей плоских фигур Площади фигур в различных координатах Вычисление объемов тел с помощью интегралов Объём тела вращения Вычисление длин дуг кривых Формулы длины дуги регулярной кривой Кривизна плоской кривой Площадь поверхности вращения тела Интегралы в физике Статические моменты и координаты центра тяжести Теоремы Гульдина–Паппа Вычисление моментов инерции Другие приложения интегралов в физике Основные интегралы Интеграл Ньютона-Лейбница Интеграл Римана Интеграл Лебега Вариационное исчисление Примеры вариационных задач Дифференциальное уравнение Эйлера Функционалы, зависящие от нескольких функций Задача о минимуме кратного интеграла Финансовый анализ Анализ эффективности Критерии и показатели эффективности предприятия Методы анализа эффективности деятельности Факторный анализ прибыли от операционной деятельности Анализ безубыточности предприятия Операционный рычаг и эффект финансового рычага Анализ и оценка состава, структуры и динамики доходов и расходов Анализ рентабельности и резервов устойчивого роста капитала Анализ распределения прибыли предприятия Анализ и оценка чувствительности показателей эффективности Анализ устойчивости Финансовая устойчивость и долгосрочная платежеспособность Характеристика типов финансовой устойчивости Рыночная активность Финансовый анализ рыночной активности Методика анализа рыночной активности Анализ и оценка дивидендного дохода на одну акцию Инвестиционная деятельность Инвестиции: экономическая сущность и классификация Государственное регулирование инвестиционной деятельности Источники финансовых ресурсов на капитальные вложения Инвестиции в основные фонды Оценка состояния основных фондов Амортизация основных фондов Капитальное строительство в инвестиционном процессе Планирование инвестиций в форме капитальных вложений Экономическая эффективность инвестиций Финансирование капитальных вложений Кредитование капитальных вложений Кредитоспособность Финансирование и кредитование затрат Финансирование и кредитование инвестиционной деятельности потребительской кооперации Финансирование и кредитование капитальных вложений потребительской кооперации Инвестиционное строительное проектирование Анализ инвестиций Инвестиции и инвестиционная деятельность предприятия Задачи финансового анализа инвестиций предприятия Учет фактора времени в инвестиционной деятельности Аннуитет и финансовая рента в инвестициях Учет фактора инфляции при инвестировании Оценка фактора риска инвестиционного проекта Методы оценки эффективности инвестиций Показатели эффективности инвестиционного проекта Стоимость компании Концепция построения международных стандартов финансовой отчетности (МСФО) Экономическое содержание международных стандартов финансовой отчётности Цели и принципы оценки стоимости акций и активов компании Оценка акций и активов предприятия по справедливой стоимости Методы оценки справедливой стоимости акций предприятия Затратный подход к оценки стоимости компаний и акций Сравнительный подход к оценки стоимости предприятий и акций Доходный подход к оценке стоимости компании и акций Выбор ставки дисконтирования при инвестировании в акции Метод капитализации прибыли Сравнение подходов к оценке стоимости компаний и пакетов акций Форвардные контракты Форвардный контракт и цена Форвардная цена акции на бирже Цена форвардного контракта инвестора Форвардная цена акции с учетом величины дивиденда Форвардная цена акции с учетом ставки дивиденда Форвардная цена валюты на рынке форекс Форвардный валютный курс и инфляция на рынке Форвардная цена товара и спотовый рынок Форвардная цена при различии ставок по кредитам и депозитам Синтетический форвардный контракт на акции и валюту Теория вероятностей Основные понятия теории вероятностей Зависимые и независимые случайные события Повторные независимые испытания Формула Бернулли Одномерные случайные величины Многомерные случайные величины Функции случайных величин Законы распределения целочисленных случайных величин Законы распределения непрерывных случайных величин Предельные теоремы теории вероятностей Закон больших чисел и предельные теоремы Вероятностные закономерности Математическая статистика Элементы математической статистики Выборочный метод Оценки параметров генеральной совокупности Статистические гипотезы Критерии согласия Теоретические и эмпирические частоты Теория очередей (СМО) Определение системы массового обслуживания Уравнения Колмогорова Предельные вероятности состояний Определение СМО с отказами Определение СМО с ожиданием (очередью) Аналитическая геометрия Векторная алгебра Метрические понятия и аксиомы геометрии Равенство и подобие геометрических фигур Бинарные отношения Вектор, его направление и длина Линейные операции над векторами Линейная зависимость и независимость векторов Отношение коллинеарных векторов Проекции векторов на прямую и на плоскость Угол между векторами Ортогональные проекции векторов Координата вектора на прямой и базис Координаты вектора на плоскости и базис Координаты вектора в пространстве и базис Операции над векторами в координатной форме Ортогональный и ортонормированный базисы Cкалярное произведение векторов и его свойства Выражение скалярного произведения через координаты векторов Векторное произведение векторов и его свойства Смешанное произведение векторов и его свойства Ориентированные площади и объемы Двойное векторное произведение и его свойства Применение векторов в задачах на аффинные свойства фигур Применение произведений векторов при решении геометрических задач Применение векторной алгебры в механике Системы координат Прямоугольные координаты Преобразования прямоугольных координат Полярная система координат Цилиндрическая система координат Сферические координаты Аффинные координаты Аффинные преобразования координат Аффинные преобразования плоскости Примеры аффинных преобразований плоскости Аффинные преобразования пространства Многомерное координатное пространство Линейные и аффинные подпространства Скалярное произведение n-мерных векторов Преобразования систем координат Геометрия на плоскости Алгебраические линии на плоскости Общие уравнения геометрических мест точек Алгебраические уравнения линий на плоскости Уравнения прямой, проходящей через точку перпендикулярно вектору Уравнения прямой, проходящей через точку коллинеарно вектору Уравнения прямой, проходящей через две точки Уравнения прямой с угловым коэффициентом Взаимное расположение прямых Примеры задач с прямыми на плоскости Системы неравенств с двумя неизвестными Системы линейных уравнений с двумя неизвестными Линии 2-го порядка Канонические уравнения линий второго порядка Порядок приведения уравнения линии к каноническому виду Эллипс Гипербола Парабола Квадратичные неравенства с двумя неизвестными Применение линий 1-го и 2-го порядков в задачах на экстремум функций Инварианты линий Классификация линий 2-го порядка по инвариантам Приведение уравнения линии к каноническому виду по инвариантам Геометрия в пространстве Способы задания ГМТ в пространстве Алгебраические уравнения поверхностей Уравнения плоскости, проходящей через точку перпендикулярно вектору Уравнения плоскости, компланарной двум неколлинеарным векторам Уравнения плоскости, проходящей через три точки Взаимное расположение плоскостей Типовые задачи с плоскостями Уравнения прямых в пространстве Взаимное расположение прямых в пространстве Типовые задачи с прямыми в пространстве Поверхности 2-го порядка Канонические уравнения поверхностей Порядок приведения уравнения поверхности к каноническому виду Поверхности второго порядка Эллипсоиды Гиперболоиды Конусы Параболоиды Применение поверхностей 1-го и 2-го порядков в задачах на экстремум функций Инварианты поверхностей Классификация поверхностей 2-го порядка по инвариантам Квадратичные неравенства с тремя неизвестными Приведение уравнения поверхности к канониче-скому виду по инвариантам Линейная алгебра Матрицы и операции Линейные операции над матрицами Умножение матриц Возведение матриц в степень Многочлены от матриц Транспонирование и сопряжение матриц Блочные матрицы Произведение и сумма матриц Кронекера Метод Гаусса приведения матрицы к ступенчатому виду Элементарные преобразования матриц Определители Определители матриц и их основные свойства Формула полного разложения определителя Формула Лапласа полного разложения определителя Определитель произведения матриц Методы вычисления определителей Ранг матрицы Линейная зависимость и линейная независимость строк (столбцов) матрицы Ранг матрицы и базисный минор матрицы Методы вычисления ранга матрицы Ранг системы столбцов (строк) Обратная матрица Обратные матрицы и их свойства Ортогональные и унитарные матрицы Способы нахождения обратной матрицы Матричные уравнения Односторонние обратные матрицы Скелетное разложение матрицы Полуобратная матрица Псевдообратная матрица Системы уравнений Системы линейных алгебраических уравнений Метод Гаусса решения систем линейных уравнений Структура общего решения системы уравнений Решение систем с помощью полуобратных матриц Псевдорешения системы линейных уравнений Функциональные матрицы Функциональные матрицы скалярного аргумента Производные матриц по векторному аргументу Линейные и квадратичные формы и их преобразования Приведение форм к каноническому виду Закон инерции вещественных квадратичных форм Знакоопределенность форм вещественных квадратичных Формы и исследование функций на экстремум Многочленные матрицы Многочленные матрицы (лямбда-матрицы) Операции над лямбда-матрицами Простые преобразования многочленных матриц Инвариантные множители многочленной матрицы Функции от матриц Собственные векторы и значения матрицы Подобие числовых матриц Характеристический многочлен матрицы Минимальный многочлен матрицы Теорема Гамильтона-Кэли Жорданова форма матрицы Приведение матрицы к жордановой форме Многочлены от матриц Применение многочленов от матриц Функции от матриц Линейные пространства Линейные пространства: определение и примеры Линейная зависимость и независимость n-мерных векторов Размерность и базис линейного пространства Преобразования координат в линейном пространстве Изоморфизм линейных пространств Подпространства Подпространства линейного пространства Пересечение и сумма подпространств Способы описания подпространств Нахождение дополнения и суммы подпространств Нахождение пересечения подпространств Линейные отображения Линейные многообразия Линейные отображения Матрица линейного отображения Ядро и образ линейного отображения Линейные операторы Линейные операторы (преобразования) Инвариантные подпространства Собственные векторы и значения оператора Свойства собственных векторов операторов Канонический вид линейного оператора Методика приведения линейного преобразования к каноническому виду Евклидовы пространства Евклидовы пространства Ортогональные векторы евклидова пространства Ортогональный базис евклидова пространства Ортонормированный базис евклидова пространства Ортогональные дополнения в евклидовом пространстве Задача о перпендикуляре Матрица и определитель Грама и его свойства Линейные преобразования евклидовых пространств Канонический вид ортогонального оператора евклидова пространства Сопряженные операторы евклидова пространства Самосопряженные операторы евклидова пространства Приведение квадратичной формы к главным осям Унитарные пространства и их линейные преобразования Комплексный анализ Комплексные числа Комплексные числа в алгебраической форме Комплексные числа в тригонометрической и показательной формах Множества на комплексной плоскости Последовательности и ряды комплексных чисел Комплексные функции Функции комплексного переменного. Предел, непрерывность и производная Элементарные функции комплексного переменного Дифференцирование функций комплексного переменного Аналитические функции и их свойства Конформные отображения и их свойства Интегрирование функций комплексного переменного Функциональные ряды в комплексной области Функциональные ряды и последовательности Степенные ряды и их свойства Разложение функций в степенные ряды Нули аналитических функций Ряд Лорана и разложение функций по целым степеням Особые точки, Вычеты Изолированные особые точки функций и полюсы Вычеты и их применение Вычисление интегралов с помощью вычетов Вычеты и расположение нулей многочлена Операционное исчисление Преобразование Лапласа и его свойства Решение ДУ операционным методом Анализ выходных процессов линейных стационарных систем Z-преобразование и его свойства Дифференциальные уравнения ДУ первого порядка Основные понятия и определения ДУ Метод изоклин для ДУ 1-го порядка Метод последовательных приближений ДУ с разделяющимися переменными Однородные ДУ Линейные ДУ 1-го порядка Дифференциальное уравнение Бернулли ДУ в полных дифференциалах Интегрирующий множитель ДУ, не разрешенные относительно производной Дифференциальное уравнение Риккати Составление ДУ семейств линий Задачи на траектории Особые решения ДУ ДУ высших порядков Понятия и определения ДУ высших порядков ДУ, допускающие понижение порядка Линейная независимость функций Определители Вронского и Грама Однородные и неоднородные дифференциальные уравнения Задача Коши и Уравнение Эйлера Линейные ДУ с переменными коэффициентами Метод Лагранжа решения ДУ Краевые задачи для ДУ высших порядков Разложение решения ДУ в степенной ряд Разложение решения ДУ в обобщенный степенной ряд Нахождение периодических решений ДУ Асимптотическое интегрирование ДУ Системы ДУ Системы ДУ: понятия и определения Сведение системы ДУ к одному уравнению Нахождение интегрируемых комбинаций Интегрирование однородных линейных систем ДУ Методы интегрирования неоднородных систем ДУ Преобразование Лапласа и решение ДУ и систем Теория устойчивости Устойчивость решений ДУ по Ляпунову Простейшие типы точек покоя Метод функций Ляпунова Устойчивость решений ДУ по первому приближению Критерии устойчивости Рауса–Гурвица и Михайлова ДУ с малым параметром при производной Численные методы Методы алгебры Численные методы линейной алгебры Численные методы решения СЛАУ Итерационный метод Шульца обратной матрицы Методы решения задач о собственных значениях и векторах матрицы Методы решения нелинейных уравнений Методы решения систем нелинейных уравнений Методы теории приближений Методы приближения сеточных функций Методы функциональной интерполяции Методы интегрально-дифференциальной интерполяции Методы интегрального сглаживания Методы интерполяции и сглаживания сплайнами Методы численного дифференцирования и интегрирования Методы численного дифференцирования Методы численного интегрирования Методы решения обыкновенных ДУ Численные методы решения задачи Коши Разностные схемы для решения задачи Коши Составные схемы для решения задачи Коши Экстраполяционные методы решения задачи Коши Непрерывно-дискретные методы решения задачи Коши Численные методы решения краевых задач Методы решения ДУ в частных производных Численные методы решения уравнений математической физики с двумя переменными Принципы построения разностных схем для уравнений в частных производных Разностные схемы решения уравнений в частных производных 1-го порядка Разностные схемы решения уравнений в частных производных 2-го порядка Численные методы решения уравнений в частных производных Численные методы решения уравнений математической физики с тремя переменными	Свойства формализованного исчисления предикатов Содержание 1. Оправданность аксиоматизации 2. Непротиворечивость формализо-ванного исчисления предикатов 3. Теорема Гёделя о существовании модели 4. Теоремы о непротиворечивости формул предикатов 5. Полнота и адекватность формализо-ванного исчисления предикатов 6. Неполнота формализованного исчисления предикатов в абсолютном и узком смыслах[ 7. Теорема компактности Формализованное исчисление предикатов (ФИП) развито достаточно глубоко, и теперь, как и в случае формализованного исчисления высказываний, надлежит рассмотреть свойства (или метатеорию) этого исчисления. Но теперь в области предикатов логика достигает такой выразительной силы, что становится логическим основанием конкретных математических теорий, и теоремы (по сути, метатеоремы) о логике рассуждений достигают поистине философской глубины. Оправданность аксиоматизации Теорема оправданности аксиоматизации утверждает, что если $\Phi\vdash F$ , то $\Phi\vDash F$ , т.е. из синтаксической выводимости следует семантическая выводимость. Ее очевидным следствием будет утверждение о том, что всякая теорема ФИП является общезначимой формулой (тавтологией) логики предикатов. Смысл этой теоремы состоит в утверждении фактически того, что мы не были "излишне щедры" в выборе аксиом и правил вывода для нашего формального исчисления и не включили в их число ничего лишнего, ибо доказуемыми в этом исчислении оказываются лишь общезначимые формулы логики предикатов. Доказательство этой теоремы не очень сложное, и мы получим ее в качестве следствия несколько более общей теоремы. Обратное же утверждение "если $\Phi\vDash F$ , то $\Phi\vdash F$ (т.е. при выборе аксиом и правил вывода мы не проявили и "излишней скромности", и для всякой общезначимой формулы логики предикатов в нашем ФИП вполне достаточно формальных средств, чтобы доказать ее), уже не столь очевидно, и доказательство его, приводимое дальше, потребует от нас значительно больших усилий. Теорема оправданности имеет глубокий смысл: она оправдывает наши занятия математикой, убеждая в том, что наши логические рассуждения и умопостроения не уводят нас от смысла и от практики. Теорема 29.1. Если в алгебраической системе $\mathbf{M}$ выполняются все формулы из множества $\Phi$ и из $\Phi$ синтаксически выводима формула $F$ , то $F$ также выполняется в $\mathbf{M}\colon \mathbf{M}\vDash \Phi$ и $\Phi\vdash F \Rightarrow \mathbf{M}\vDash F$ . Доказательство разделим на три этапа. На первом этапе отметим, что каждая аксиома ФИП есть тождественно истинная формула. Что касается аксиом $A1,\,A2,\,A3$ исчисления высказываний, то их тождественная истинность установлена нами в алгебре высказываний (см. теоремы 3.1 з, 3.3, а, л). Общезначимость аксиом $\mathsf{PA1}$ и $\mathsf{PA2}$ установлена в теореме 21.13. На втором этапе покажем, что все три правила вывода, используемые в ФИП, обладают следующим семантическим свойством. Если алгебраическая система $\mathbf{M}$ служит моделью для всех посылок правила вывода, то $\mathbf{M}$ будет моделью и для формулы, получаемой из данных формул с помощью данного правила вывода. Докажем это утверждение для трех из правил вывода. Правило MP. Допустим, что $\mathbf{M}\vDash F\to G$ и $\mathbf{M}\vDash F$ . Докажем, что тогда $\mathbf{M}\vDash G$ . Возьмем любую подстановку $\alpha$ констант из $\mathbf{M}$ . Тогда, по условию, каждое из высказываний $F(\alpha)\to G(\alpha)$ и $F(\alpha)$ , получаемых соответственно из формул $F\to G$ и $F$ в результате подстановки предметных констант $\alpha$ , будет истинным. Тогда истинным будет и высказывание $F(\alpha)$ , то есть $\mathbf{M}\vDash_{\alpha}G$ . Это и означает, что $\mathbf{M}\vDash G$ . $\forall$ -правило. Допустим, что $\mathbf{M}\vDash G(y)\to F(x,y)$ , где $x$ не входит свободно в формулу $G$ , а $y$ обозначает все свободные предметные переменные в формулах $F$ и $G$ (в $F$ — кроме $x$ ). Тогда сделанное допущение означает, что для любых элементов $a,b\in M$ (где $M$ — носитель алгебраической системы $\mathbf{M}$ ) высказывание $G(b)\to F(a,b)$ истинно в $\mathbf{M}$ . Рассмотрим теперь высказывание $G(b)\to (\forall x)(F(x,b))$ и покажем, что оно истинно в $\mathbf{M}$ при любом $b\in M$ . В самом деле, если $G(b)$ ложно, то рассматриваемое высказывание истинно. Если же $G(b)$ истинно, то, по отмеченному выше, истинным будет и высказывание $F(a,b)$ . Поскольку оно будет истинным при любом $a\in M$ , то отсюда вытекает истинность для таких $b\in M$ высказывания $(\forall x)(F(x,b))$ . Это, в свою очередь, влечет истинность высказывания $G(b)\to (\forall x)(F(x,b))$ для тех $b\in M$ , для которых $G(b)$ истинно. Итак, высказывание $G(b)\to (\forall x)(F(x,b))$ истинно для любых $b\in M$ . Это и означает, что $\mathbf{M}\vDash G(y)\to (\forall x)(F(x,y))$ . $\exists$ -правило. Подобно предыдущему правилу, доказывается, что если $\mathbf{M}\vDash F(x)\to G$ , то $\mathbf{M}\vDash (\exists x)(F(x))\to G$ . Наконец, на третьем этапе докажем утверждение самой теоремы. Пусть $\mathbf{M}\vDash \Phi$ и $\Phi\vdash F$ . Последнее означает, что имеется вывод $B_1,B_2,\ldots,B_m$ формулы $F$ из множества формул $\Phi$ (в частности, $B_m\equiv F$ ). Покажем, что каждый элемент этой последовательности является формулой, выполняющейся в $\mathbf{M}$ . Доказательство проведем индукцией по номеру $k$ формулы в рассматриваемом выводе. При $k=1$ , если $B_1\in\Phi$ , то, по условию, $\mathbf{M}\vDash B_1$ . Если $B_1$ — аксиома, то она общезначима и, в частности, $\mathbf{M}\vDash B_1$ . Предположим теперь, что при всех $k<n~(n\geqslant2)$ все формулы $B_k$ выполняются в $\mathbf{M}$ , то есть $\mathbf{M}\vDash B_k$ . Рассмотрим формулу $B_n$ . Если $B_n\in\Phi$ или $B_n$ — аксиома, то, как отмечено выше, $\mathbf{M}\vDash B_n$ . Если же $B_n$ получена из предыдущих формул последовательности по одному из трех правил вывода, то (на основании выполнимости всех предыдущих формул в $\mathbf{M}$ ) в силу утверждений (см. второй этап) заключаем, что и $B_n$ выполняется в $\mathbf{M}$ , то есть $\mathbf{M}\vDash B_n$ . Окончательно заключаем, что все формулы последовательности $B_1,B_2,\ldots,B_m$ истинны в $\mathbf{M}$ , в частности $\mathbf{M}\vDash F$ . Теорема полностью доказана. Следствие 29.2 (теорема оправданности). Из синтаксической выводимости следует семантическая выводимость, т. е. если $\Phi\vdash F$ , то $\Phi\vDash F$ . Доказательство. Пусть $\Phi\vdash F$ и пусть $\mathbf{M}$ — любая алгебраическая система, в которой выполняются все формулы из $\Phi$ , то есть $\mathbf{M}\vDash\Phi$ . Тогда по доказанной теореме $\mathbf{M}\vDash F$ . По определению семантического следствия это и означает, что $\Phi\vDash F$ . Следствие 29.3. Всякая доказуемая формула является общезначимой (т.е. любая теорема истинна): если $\vdash F$ , то $\vDash F$ . Доказательство получается из предыдущего следствия при $\Phi=\varnothing$ . Непротиворечивость формализованного исчисления предикатов Важнейшим компонентом критерия оправданности всякой математической теории является ее непротиворечивость, т.е. невозможность доказательства в ней некоторого утверждения и его отрицания одновременно. Трудности, связанные с доказательством этого свойства математических теорий (а одной из причин этих трудностей, несомненно, было отсутствие в содержательных математических теориях точного понятия доказательства), привели к тому, что в математике более естественным стал другой признак непротиворечивости теории, основанный на возможностях реализации этой теории, ее моделируемости. Но в то же время этот подход и привел к возникновению парадоксов в математике, которые, в свою очередь, привели к возникновению науки об основаниях математики и к концепциям формального подхода к понятиям доказательства и математической (аксиоматической) теории. Одной из задач этого подхода была выработка такого формального понятия доказательства, при котором для конкретной математической теории понятие ее формальной непротиворечивости совпало бы с понятием ее содержательной непротиворечивости. Факт такого совпадения, в силу точности определения доказательства, становится математической теоремой (точнее, метатеоремой). Отметим, что привыкание в математике к эквивалентности этих двух понятий непротиворечивости было непростым. В частности, неприятие современниками неевклидовых геометрий Лобачевского–Бояи объясняется также и тем, что законность этих теорий обосновывалась отсутствием в них противоречий — аргументом, совпадающим по существу с современным понятием формальной непротиворечивости. Геометрические модели для этих теорий, доказывающие их содержательную непротиворечивость, были найдены позднее. Наша задача состоит в том, чтобы в рамках формализованного (узкого) исчисления предикатов дать точные определения двух понятий непротиворечивости и установить их эквивалентность. Напомним, что формула логики предикатов называется общезначимой, если она истинна в любой интерпретации, и противоречивой, если она ложна в любой интерпретации, т.е. если ее отрицание общезначимо. Эти семантические понятия, связывающие непротиворечивость с истинностью, позволяют сформулировать понятие семантически непротиворечивой теории. Определение 29.4. Формальная теория называется семантически непротиворечивой, если ни одна из ее теорем (формул) не является противоречивой, т. е. ложной при любой ее интерпретации. Аналогично, множество $\Phi$ формул называется семантически непротиворечивым, если ни одна формула, выводимая из $\Phi$ , не является противоречивой. В теореме 16.1 доказано, что всякая теорема формализованного исчисления высказываний общезначима (тождественно истинна), а потому не является противоречивой. Это означает, что формализованное исчисление высказываний семантически непротиворечиво. Аналогичная теорема доказана и для формализованного исчисления предикатов (см. следствие 29.3 из теоремы 29.1 выше). Значит, и ФИП семантически непротиворечиво. Семантическая непротиворечивость ФИВ и ФИП означает, что эти формальные теории пригодны для описания любых классов алгебраических систем, т.е. они войдут в теории этих классов составными частями, что вполне соответствует общенаучному принципу универсальности законов логики (Лейбниц формулировал его как выполнимость логических законов "во всех мыслимых мирах"). Произвольная формальная теория $T$ есть теория множества $M(T)$ всех своих моделей, а значит, теория $T$ семантически непротиворечива, если и только если $\mathbf{M}(T)\ne \varnothing$ , т.е. для теории $T$ существует модель. Если отождествить пригодность математической теории, ее целесообразность с ее семантической непротиворечивостью, то можно сказать, что сформулированный критерий пригодности теории известен уже давно. Отыскание модели для теории до возникновения оснований математики было единственным общепризнанным методом доказательства "законности" теории. Математическая логика выработала аналог этого критерия, не опирающийся на наличие модели теории — внешний фактор по отношению к теории, а опирающийся на внутренние свойства самой теории, — понятие синтаксической непротиворечивости теории. Определение 29.5. Формальная теория $T$ называется синтаксически (или дедуктивно, или формально) непротиворечивой, если не существует такой формулы $F$ , что $F$ и $\lnot F$ являются теоремами теории $T$ , т.е. в $T$ невыводимыми являются одновременно формула и ее отрицание. Аналогичное определение можно сформулировать и для произвольного множества $\Phi$ формул: $\Phi$ называется синтаксически непротиворечивым, если из $\Phi$ невыводимы одновременно формула и ее отрицание. В теореме 16.9 доказана синтаксическая непротиворечивость формализованного исчисления высказываний. Аналогично доказывается следующая теорема. Теорема 29.6. Формализованное исчисление предикатов синтаксически непротиворечиво. Доказательство. Допустим противное, т.е. предположим, что ФИП синтаксически противоречиво. Значит, найдется такая формула $F$ , что $F$ и $\lnot F$ будут теоремами ФИП. Тогда по следствию 29.3 из теоремы 29.1 формулы Fa -,Fбудут общезначимыми, что невозможно на основании определения общезначимости. Теперь перейдем к установлению взаимосвязей между понятиями семантической и синтаксической непротиворечивости. Наша задача состоит в том, чтобы доказать их эквивалентность. Начнем с достаточно простой, но важной леммы. Лемма 29.7. Если множество формул имеет модель, то это множество семантически непротиворечиво. Доказательство. Если множество $\Phi$ формул имеет модель $\mathbf{M}$ , то ни одна формула, выводимая из $\Phi$ , не является противоречивой, т.е. ложной во всякой интерпретации, ибо в противном случае она была бы ложна и в $\mathbf{M}$ (что невозможно в силу теоремы 29.1). Это и означает, что $\Phi$ семантически непротиворечиво. Теорема 29.8. Если множество формул семантически непротиворечиво, то оно синтаксически непротиворечиво. Доказательство. Допустим, что некоторое множество $\Phi$ формул узкого исчисления предикатов семантически непротиворечиво, но противоречиво синтаксически. Следовательно, из него выводима некоторая формула $F$ и ее отрицание $\lnot F$ . Но тогда из $\Phi$ выводима и их конъюнкция (по правилу введения конъюнкции) $F\land\lnot F$ . Но эта формула ложна в любой интерпретации, что означает, что множество $\Phi$ семантически противоречиво. Получаем противоречие, доказывающее, что $\Phi$ синтаксически непротиворечиво. Непосредственно из предыдущих леммы и теоремы вытекает такое следствие. Следствие 29.9. Если множество формул имеет модель, то оно синтаксически непротиворечиво. Теорема Гёделя о существовании модели Утверждение, обратное следствию, также оказывается справедливым. Но с конструктивной точки зрения оно оказывается более глубоким. Смысл его состоит в том, что всякое множество формул не только имеет модель, но эту модель можно конструктивно построить. Доказательство этого факта как раз и заключается в изложении метода такого построения. Это еще одна из замечательных теорем Гёделя (теорема о существовании модели), относящаяся к важнейшим теоремам математической логики. Она доказана Гёделем в 1930 г. Теорема 29.10 (теорема Гёделя о существовании модели). Любое синтаксически непротиворечивое множество $\Sigma$ замкнутых формул узкого исчисления предикатов сигнатуры $\sigma$ имеет модель. Доказательство Пусть сигнатура $\sigma= \bigl\{a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots\bigr\}$ . Требуется построить модель $\mathbf{M}= <M;\, a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots>$ , такую, что $\mathbf{M}\vDash\Sigma$ (т.е. в алгебраической системе $\mathbf{M}$ выполняются все формулы из $\Sigma$ ). Эта модель будет строиться из слов некоторого алфавита. Под непротиворечивостью всюду в этом доказательстве будем понимать синтаксическую непротиворечивость. Прежде всего расширим данную сигнатуру $\sigma$ до $\sigma'$ введением новых индивидных констант: $\sigma'= \sigma\cup\{c_0,c_1,\ldots,c_n,\ldots\}$ , где все $c_i$ отличны от всех символов из $\sigma$ . Далее будем работать с формулами расширенной сигнатуры $\sigma'$ . Поскольку все такие (замкнутые) формулы являются конечными словами некоторого счетного алфавита, то множество всех таких формул имеет счетную мощность и мы можем все их расположить в последовательность (т.е. занумеровать натуральными числами). Итак, пусть $A_0,A_1,\ldots,A_n,\ldots$ — множество всех предложений (замкнутых формул) сигнатуры $\sigma'$ . Построим далее последовательность (цепочку) $\Sigma_0\subseteq \Sigma_1\subseteq \ldots\subseteq \Sigma_n\subseteq\ldots$ (1) множеств замкнутых формул следующим образом: а) $\Sigma_0=\Sigma$ ; б) если $\Sigma_n\cup\{A_n\}$ противоречиво, то $\Sigma_{n+1}= \Sigma_n\cup \{\lnot A_n\}$ ; в) если $\Sigma_n\cup\{A_n\}$ непротиворечиво и $A_n$ не начинается с квантора существования, то $\Sigma_{n+1}= \Sigma_n\cup\{A_n\}$ ; г) если $\Sigma_n\cup\{A_n\}$ непротиворечиво и $A_n\equiv (\exists x)(B(x))$ , то $\Sigma_{n+1}= \Sigma_n\cup\{A_n, B(c_k)\}$ , где $c_k\in \sigma'\setminus \sigma$ — новая константа с наименьшим номером $k$ , не встречающаяся в формуле $A_n$ и во всех формулах множества $\Sigma_n$ . 1) Докажем сначала, что каждое множество $\Sigma_n$ построенной последовательности будет непротиворечивым множеством формул исчисления предикатов сигнатуры $\sigma'$ . Доказательство будем вести индукцией по $n$ . с) База индукции: $n=0$ . Так как $\Sigma_0=\Sigma$ , то по условию $\Sigma_0$ непротиворечиво в исчислении предикатов сигнатуры $\sigma$ . Докажем, что оно непротиворечиво и в исчислении сигнатуры $\sigma'$ . Допустим противное, т.е. $\Sigma_0\vdash F$ и $\Sigma_0\vdash\lnot F$ , где $F$ — формула сигнатуры $\sigma'$ . Следовательно, $\Sigma\vdash F$ и $\Sigma\vdash\lnot F$ . Это означает, что в $\Sigma$ имеется такое конечное подмножество формул $G_1,G_2,\ldots,G_m$ , что $G_1,G_2,\ldots,G_m\vdash F,\lnot F$ . Пусть $B_1,B_2,\ldots,B_s\equiv F$ — вывод формулы $F$ из гипотез $G_1,G_2,\ldots,G_m$ в исчислении предикатов сигнатуры $\sigma'$ . Допустим, что $c_{i_1},c_{i_2},\ldots,c_{i_p}$ — все те новые константы, которые входят в формулы этого вывода. Поскольку $\forall$ - и $\exists$ -правила вывода к константам не применяются, то, заменив все новые константы $c_{i_1},c_{i_2},\ldots,c_{i_p}$ предметными переменными, не входящими в формулы $B_1,B_2,\ldots,B_s$ , получим новую последовательность формул $\widetilde{B}_1, \widetilde{B}_2,\ldots, \widetilde{B}_s$ исчисления предикатов уже сигнатуры $\sigma$ , представляющую собой вывод в этом исчислении ее последней формулы $\widetilde{B}_s\equiv \widetilde{F}$ . Аналогично доказывается, что в исчислении сигнатуры $\sigma$ из множества $\Sigma$ выводима формула $\lnot \widetilde{F}$ . Получается противоречие с условием, согласно которому $\Sigma$ — непротиворечиво в исчислении сигнатуры $\sigma$ . Таким образом, $\Sigma_0$ непротиворечиво в исчислении сигнатуры $\sigma$ . Шаг индукции. Предположим, что $\Sigma_n$ непротиворечиво в исчислении предикатов сигнатуры $\sigma'$ . Покажем, что тогда таким же свойством обладает и множество $\Sigma_{n+1}$ . Согласно определению для него возможны следующие случаи: б) $\Sigma_{n}\cup\{A_n\}$ противоречиво. В этом случае $\Sigma_{n+1}= \Sigma_{n}\cup\{\lnot A_n\}$ . Допустим, что последнее множество противоречиво. Тогда $\Sigma_{n},\lnot A_n\vdash F$ и $\Sigma_{n},\lnot A_n\vdash\lnot F$ для некоторой формулы $F$ . Тогда для некоторого конечного подмножества $\Gamma\subset \Sigma_{n}\colon \Gamma,\lnot A_n\vdash F$ и $\Gamma,\lnot A_n\vdash\lnot F$ . Отсюда по производному правилу вывода $\lnot$ –вв получим $\Gamma\vdash\lnot\lnot A_n$ , то есть $\Gamma\vdash A_n$ , а значит, $\Sigma_n\vdash A_n$ . В то же время из условия противоречивости множества $\Sigma_n\cup\{A_n\}$ аналогичные рассуждения приведут к заключению: $\Sigma_n\vdash\lnot A_n$ . Эти два заключения говорят о противоречивости множества $\Sigma_n$ , что противоречит предположению индукции; в) $\Sigma_n\cup\{A_n\}$ непротиворечиво и $A_n$ не начинаются с квантора существования. В этом случае по определению $\Sigma_{n+1}= \Sigma_n\cup \{A_n\}$ , а значит, $\Sigma_{n+1}$ — непротиворечиво; г) $\Sigma_n\cup\{A_n\}$ непротиворечиво и $A_n$ начинается с квантора существования: $A_n\equiv (\exists x)(B(x))$ . В этом случае $\Sigma_{n+1}$ получается добавлением к $\Sigma_n$ двух формул $A_n$ и $B(c_k)$ , где $B(c_k)$ получена из $B(x)$ подстановкой константы $c_k$ (первой из $c_0,c_1,\ldots$ , не входящей в $A_n$ и все формулы из $\Sigma_{n}$ ) вместо предметной переменной $x\colon\, \Sigma_{n+1}= \Sigma_{n}\cup\{A_n,B(c_k)\}$ . Допустим, что $\Sigma_{n+1}$ противоречиво, т.е. $\Sigma_{n+1}\vdash F,\lnot F$ . Тогда найдется такое конечное подмножество $\Gamma\subset\Sigma_{n}$ , что $\Gamma, (\exists x)(B(x)),\, B(c_k)\vdash F$ и $\Gamma,(\exists x)(B(x)),\,B(c_k)\vdash\lnot F$ . Поскольку в выводах этих формул $\forall$ -правило и $\exists$ -правило вывода не применяются к константе $c_k$ , то, заменив в них эту константу новой переменной $y$ , не участвующей в выводах этих формул, получим выводы, доказывающие, что $\Gamma,\,(\exists x)(B(x)),\, B(y_k)\vdash \widetilde{F}$ и $\Gamma,\, (\exists x)(B(x)),\, B(y_k)\vdash\lnot \widetilde{F}$ , где $\widetilde{F}$ , получена из $F$ заменой константы $c_k$ на предметную переменную $y$ ( $y$ — фиксированная переменная в этих выводах). Из двух последних выводимостей по производному правилу вывода (введения отрицания $\lnot$ -вв) получаем: $\Gamma,\,(\exists x)(B(x))\vdash\lnot B(y)$ . Отсюда по правилу введения квантора общности получаем $\Gamma,~ (\exists x) \bigl(B(x)\bigr)\vdash (\forall y)\bigl(\lnot B(y)\bigr).$ (2) Кроме того, легко получается выводимость $(\forall y)(\lnot B(y))\vdash\lnot (\exists y)(B(y))$ . Наконец, в силу выбора переменной $y$ , которая свободна для $x$ в формуле $B(x)$ , и на основании правила переименования связанных переменных из последней выводимости заключаем, что $(\forall y)\bigl(\lnot B(y)\bigr)\vdash\lnot (\exists x)\bigl(B(x)\bigr).$ (3) Из выводимостей (2) и (3), в силу транзитивности отношения выводимости (см. теорему 15.3, в), получаем: $\Gamma,~ (\exists x)\bigl(B(x)\bigr)\vdash\lnot (\exists x) \bigl(B(x)\bigr).$ Учитывая, что $(\exists x)(B(x))\equiv A_n$ , можно заключить, что множество $\Gamma\cup\{A_n\}$ противоречиво. Поскольку $\Gamma\subset\Sigma_n$ , то $\Gamma\cup\{A_n\}\subset \Sigma_n\subset \{A_n\}$ , а значит, множество $\Sigma_n\cup\{A_n\}$ также противоречиво, что противоречит исходному условию. Следовательно, и в этом случае множество $\Sigma_{n+1}$ непротиворечиво. 2) Рассмотрим теперь множество $\Sigma^{\ast}=\cup\Sigma_{n}$ (объединение берется по $n$ от 0 до $\infty$ ). Отметим два свойства этого множества формул. Во-первых, множество $\Sigma^{\ast}$ непротиворечиво. В самом деле, если бы из $\Sigma^{\ast}$ выводились формулы $F$ и $\lnot F$ , то они выводились бы из конечного подмножества множества $\Sigma^{\ast}$ , которое включалось бы в некоторое $\Sigma_{n}$ которое, следовательно, было бы противоречивым. Но это не так в силу предыдущего п. 1 доказательства. Во-вторых, для любой формулы $A$ исчисления предикатов сигнатуры $\sigma'~A\in \Sigma^{\ast}$ или $\lnot A\in \Sigma^{\ast}$ (свойство полноты множества $\Sigma^{\ast}$ ). Это вытекает непосредственно из построения $\Sigma^{\ast}$ , так как $A=A_n$ для некоторого натурального $n$ . Последнее свойство можно сформулировать несколько в ином виде. Сначала отметим, что $A\in \Sigma^{\ast}\Leftrightarrow \Sigma^{\ast}\vdash A$ . В самом деле, импликация слева направо очевидна. Предположив, что $\Sigma^{\ast}\vdash A$ и $A\notin \Sigma^{\ast}$ , в силу отмеченного свойства получим $\lnot A\in\Sigma^{\ast}$ . В итоге получаем, что $\Sigma^{\ast}$ противоречиво, что противоречит первому отмеченному выше свойству. Следовательно, второе отмечаемое утверждение принимает вид: $\Sigma^{\ast}\vdash A$ или $\Sigma^{\ast}\vdash\lnot A$ для любой формулы $A$ . 3) Построим теперь саму модель $\mathbf{M}$ . Напомним, что ее сигнатура $\sigma= \bigl\{a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots\bigr\}$ . Рассмотрим всевозможные термы расширенной сигнатуры $\sigma'$ , не содержащие предметных переменных, а содержащие лишь предметные константы $a_0,a_1,\ldots,\, c_0,c_1,\ldots$ . Напомним, что термы представляют собой либо сами эти константы, либо выражения вида $f_i(t_1,\ldots,t_{n_i})$ , где $f_i$ — функциональный символ из $\sigma$ , a $t_1,\ldots,t_{n_i}$ — термы. Множество всех этих термов и есть базисное множество $M$ модели $\mathbf{M}$ . Сигнатурные операции на этом множестве зададим следующим образом: $a_{i}^{M}= a_i,~ f_{i}^{M}(t_1,\ldots,t_{n_i})= f_i(t_1,\ldots,t_{n_i}),\quad i=0,1,2, \ldots$ Наконец, выполнимость на $\mathbf{M}$ соответствующего сигнатурного отношения определим следующим образом: $\mathbf{M}\vDash P_{j}^{M}(t_1,\ldots,t_{n_i})~ \Leftrightarrow~ \Sigma^{\ast}\vdash P_{j}(t_1,\ldots,t_{n_i}).$ (4) 4) Проверим, что алгебраическая система $\mathbf{M}$ сигнатуры о действительно является моделью исходного множества $\Sigma$ формул исчисления предикатов сигнатуры $\sigma$ , то есть $\mathbf{M}\vDash\Sigma$ . Для этого докажем сначала, что для всякой формулы $F(x_1,\ldots,x_n)$ сигнатуры $\sigma'$ и любых термов $t_1,\ldots,t_n\in M$ имеет место-следующее утверждение: $\mathbf{M}\vDash F(t_1,\ldots,t_n)~ \Leftrightarrow~ \Sigma^{\ast}\vdash F(t_1,\ldots,t_n).$ (5) Доказательство будем вести индукцией по числу $k$ логических знаков, используемых при построении формулы $F$ . База индукции: $k=0$ . Тогда $F$ — атомарная формула, имеющая вид $P_j(t_1,\ldots,t_{m_j})$ , а для нее утверждение (5) верно по определению (4). Шаг индукции. Предположим, что для всех формул, в записи которых число логических символов $\leqslant k$ , утверждение (5) верно. Пусть $F$ — произвольная формула, в записи которой участвует $k+1$ логический символ. Покажем, что тогда утверждение (5) будет справедливо и для нее. На основании определения (формулы) формула F имеет один из следующих видов: $\lnot A,\,A\to B,\, (\forall x)(B(x)),\, (\exists x)(B(x))$ . Рассмотрим последовательно каждый из этих случаев. а) $F\equiv\lnot A$ . Предположим, что $\mathbf{M}\vDash\lnot A(t_1,\ldots, t_n)$ . Тогда по определению отрицания это означает, что $A(t_1,\ldots, t_n)$ не выполняется на $\mathbf{M}\colon\, \mathbf{M}\nvDash A(t_1,\ldots, t_n)$ . Отсюда по предположению индукции заключаем, что $\Sigma^{\ast}\nvdash A(t_1,\ldots, t_n)$ . Следовательно, по свойству полноты множества $\Sigma^{\ast}$ , отмеченному в п. 2 настоящего доказательства, $\Sigma^{\ast}\vdash\lnot A(t_1,\ldots, t_n)$ . Легко видеть, что каждое утверждение настоящего рассуждения допускает обращение, так что $\mathbf{M}\vDash\lnot A(t_1,\ldots, t_n)~ \Leftrightarrow~ \Sigma^{\ast}\vdash\lnot A(t_1,\ldots, t_n).$ б) $F\equiv A\to B$ . Предположим, что $\mathbf{M}\vDash A(t_1,\ldots, t_n)\to B(t_1,\ldots, t_n)$ . Используя определения импликации, конъюнкции и отрицания, определение (4), полноту $\Sigma^{\ast}$ и предположение индукции для формул $A$ и $B$ , проводим следующее рассуждение: $\mathbf{M}\vDash A\to B \Leftrightarrow \mathbf{M}\vDash\lnot(A\land\lnot B) \Leftrightarrow \mathbf{M}\nvDash A\land\lnot B \Leftrightarrow \mathbf{M}\nvDash A$ , или $\mathbf{M}\nvDash\lnot B \Leftrightarrow \mathbf{M}\nvDash A$ , или $\mathbf{M}\vDash B \Leftrightarrow \Sigma^{\ast}\nvdash A$ , или $\Sigma^{\ast}\vdash B \Leftrightarrow \Sigma^{\ast}\vdash\lnot A$ , или $\Sigma^{\ast}\vdash B$ . Теперь мы находимся в области формализованного исчисления высказываний. Дальнейшие рассуждения таковы. Из каждого из утверждений $\Sigma^{\ast}\vdash\lnot A$ и $\Sigma^{\ast}\vdash B$ по правилу $\lor$ -вв следует $\Sigma^{\ast} \vdash\lnot A\lor B$ , то есть $\Sigma^{\ast}\vdash A\to B$ . Теперь нужно проделать обратное рассуждение. Предположим, что $\Sigma^{\ast}\vdash A\to B$ и $\Sigma^{\ast}\vdash\lnot A$ . Следовательно, по второму свойству множества $\Sigma^{\ast}$ из п. 2 настоящего доказательства $\Sigma^{\ast}\vdash A$ . Тогда из выводимостей $\Sigma^{\ast}\vdash A\to B$ и $\Sigma^{\ast}\vdash A$ и правила MP $(A\to B,~ A\vdash B)$ следует, что $\Sigma^{\ast}\vdash B$ . Итак, мы доказали, что $\mathbf{M}\vDash A\to B \Leftrightarrow \Sigma^{\ast}\vdash A\to B$ . в) $F\equiv (\forall x)(B(x,t_1,\ldots,t_n))$ . Предположим, что $\mathbf{M}= (\forall x)(B(x,t_1,\ldots,t_n))$ . По определению квантора общности это означает, что $\mathbf{M}\vDash B(t,t_1,\ldots,t_n)$ для каждого элемента $t\in M$ . Таким образом, по предположению индукции (5) получим, что $\Sigma^{\ast}\vdash B(t,t_1,\ldots,t_n)$ . Отсюда, в силу правила введения квантора общности, заключаем, что $\Sigma^{\ast}\vdash (\forall x)(B(x,t_1,\ldots,t_n))$ . Обратно, пусть $\Sigma^{\ast}\vdash (\forall x)(B(x,t_1,\ldots,t_n))$ . Вместе с аксиомой $\mathsf{PA1}\colon (\forall x)(B(x,t_1,\ldots,t_n))\to B(t,t_1,\ldots,t_n)$ , в силу правила MP, это дает: $\Sigma^{\ast}\vdash B(t,t_1,\ldots,t_n)$ . На основании предположения индукции (5) отсюда следует, что $\mathbf{M}\vDash B(t,t_1,\ldots,t_n)$ . Поскольку данная выполнимость на модели $\mathbf{M}$ имеет место для любого элемента $t\in M$ , поэтому на основании определения квантора общности отсюда следует, что $\mathbf{M}\vDash (\forall x)(B(x,t_1,\ldots,t_n))$ . г) $F\equiv (\exists x)(B(x,t_1,\ldots,t_n))$ . Предположим, что $\mathbf{M}\vDash (\exists x)(B(x,t_1,\ldots,t_n))$ . Тогда по определению квантора существования $\mathbf{M}\vDash B(a_0,t_1,\ldots,t_n)$ для некоторого элемента $a_0\in M$ . В силу предположения индукции (5) отсюда получаем $\Sigma^{\ast}\vdash B(a_0,t_1,\ldots, t_n)$ . Вместе с аксиомой $\mathsf{PA2}\colon B(a_0,t_1,\ldots,t_n)\to (\exists x)(B(x,t_1, \ldots,t_n))$ , в силу правила MP, это дает: $\Sigma^{\ast}\vdash (\exists x)(B(x,t_1,\ldots,t_n))$ . Обратно, пусть $\Sigma^{\ast}\vdash (\exists x)(B(x,t_1,\ldots,t_n))$ . Поскольку $(\exists x)(B(x,t_1,\ldots,t_n))$ — замкнутая формула сигнатуры $\sigma'$ , то она содержится в последовательности $A_1,A_2,\ldots,A_n,\ldots$ всех таких формул. Предположим, что это формула $A_m$ . Тогда множество $\Sigma_m\cup \{A_m\}$ непротиворечиво. (Если бы оно было противоречиво, то $\Sigma_{m+1}$ равнялось бы $\Sigma_m\cup \{\lnot A_m\}$ , т.е. формула $\lnot A_m$ входила бы в множество $\Sigma^{\ast}$ и последнее было бы противоречивым, что не так в силу п. 2 настоящего доказательства.) Поскольку, кроме того, $A_m$ начинается с квантора существования, то в этом случае $\Sigma_{m+1}= \Sigma_{m}\cup \bigl\{A_m,\, B(c_k,t_1,\ldots,t_n)\bigr\}$ и, значит, $B(c_k,t_1,\ldots,t_n)\in \Sigma^{\ast}$ . Следовательно, для формулы $B(c_k,t_1,\ldots,t_n)$ по предположению индукции имеем $\mathbf{M}\vDash B(c_k,t_1,\ldots,t_n)$ для некоторой константы $c_k\in M$ . Тогда по определению квантора существования $\mathbf{M}\vDash (\exists x)(B(x,t_1,\ldots,t_n))$ . Итак, мы доказали, что всякая формула, выводимая из $\Sigma^{\ast}$ (и, в частности, принадлежащая $\Sigma^{\ast}$ ), истинна (выполнима) на модели $\mathbf{M}$ . В частности, на $\mathbf{M}$ выполняются и все формулы исходной совокупности $\Sigma= \Sigma_0\subset \Sigma^{\ast}$ , то есть $\mathbf{M}$ — действительно модель непротиворечивого множества формул £. Теорема полностью доказана. Теоремы о непротиворечивости формул предикатов Теорема Гёделя о существовании модели позволяет доказать теорему, обратную к теореме 29.8, и они вместе образуют следующую важную метатеорему. Теорема 29.11 (о непротиворечивости). Множество формул узкого исчисления предикатов семантически непротиворечиво тогда и только тогда, когда оно синтаксически непротиворечиво. Доказательство. Необходимость есть теорема 29.8. Обратно, если множество формул синтаксически непротиворечиво, то по теореме 29.10 оно имеет модель, а тогда по лемме 29.7 оно семантически непротиворечиво. Наконец, объединим в одну метатеорему следствие из теоремы 29.8 и теорему 29.10. Получим следующее. Теорема 29.12 (о непротиворечивости). Множество формул узкого исчисления предикатов синтаксически (дедуктивно) непротиворечиво тогда и только тогда, когда оно имеет модель. Приведем интересный комментарий, который дает теореме о непротиворечивости известный логик Р. Линдон, по мнению которого доказательства (дедуктивной) непротиворечивости какой-либо теории посредством указания ее модели широко распространены в абстрактной математике. Менее очевидное из утверждений теоремы о непротиворечивости — о существовании модели у каждой дедуктивно непротиворечивой теории — используется далеко не так часто. Возможно, это объясняется тем, что математики не слишком-то большое значение придают понятию существования; теорему о непротиворечивости можно как раз и рассматривать как скромное, но зато точное выражение довольно-таки расплывчатого мнения, что существование в математике — это не что иное, как непротиворечивость. Возможности применения теоремы о непротиворечивости к проблемам установления непротиворечивости конкретных теорий весьма ограниченны: дело в том, что построение модели обычно требует принятия в метаязыке допущений, значительно более сильных, нежели те, которые выражаются предметной теорией. Другой путь установления непротиворечивости какой-нибудь аксиоматической теории состоит в том, чтобы с помощью чисто синтаксических рассмотрений показать, что в данной теории нельзя доказать тождественно ложную формулу. Область применения этого метода, однако, также невелика. Теорема Гёделя не позволяет надеяться на получение доказательства непротиворечивости теории, если не допускать в теории, предназначенной для такого доказательства на метаязыке, по меньшей мере столь же сильных средств, что и в рассматриваемой предметной теории. Убеждение в непротиворечивости достаточно сложных математических теорий базируется в конечном счете на интуиции и опыте. Полнота и адекватность формализованного исчисления предикатов Доказав теорему Гёделя о существовании модели (теорема 29.10), можно доказать теорему, обратную теореме оправданности (следствие 29.2 из теоремы 29.1), т.е. утверждение о том, что из семантической выводимости следует синтаксическая выводимость. В самом деле, пусть $\Phi\vDash F$ . Покажем, что тогда множество формул $\Phi\cup\{\lnot F\}$ противоречиво. Допустим на время, что это не так. Тогда по теореме 29.10 это множество имеет модель $\mathbf{M}$ , т.е. на $\mathbf{M}$ выполняется формула $\lnot F$ и все формулы из $\Phi$ . Из последнего, ввиду условия $\Phi\vDash F$ , следует, что на $\mathbf{M}$ выполняется и формула $F$ . Получаем противоречие. Итак, множество $\Phi\cup\{\lnot F\}$ противоречиво. Значит, из него выводима любая формула, в частности $\Phi\cup\{\lnot F\}\vdash F$ . Тогда по теореме о дедукции имеем $\Phi\vdash\lnot F\to F$ . Учитывая, что, кроме того, формула $(\lnot F\to F)\to F$ является теоремой ФИВ, по правилу MP заключаем, что $\Phi\vdash F$ . Итак, мы доказали, что если $\Phi\vDash F$ , то $\Phi\vdash F$ . Объединив это утверждение со следствием 29.1 из теоремы 29.2, приходим к следующей важной метатеореме. Теорема 29.13 (теорема адекватности). Формула $F$ синтаксически выводима из множества формул $\Phi$ тогда и только тогда, когда она семантически выводима из $\Phi\colon\, \Phi\vdash F \Leftrightarrow \Phi\vDash F$ . Если теорема оправданности означала, что при выборе аксиом и правил вывода мы не были слишком щедры (настолько, что сможем доказать лишь общезначимые формулы), то обратная теорема — теорема адекватности — означает, что при этом выборе мы не были и излишне скупы (ровно настолько, что сможем доказать всякую общезначимую формулу). Заметим, что нетрудно показать, что теорема о существовании модели вытекает из теоремы адекватности. В самом деле, предположим, что $\Phi$ — непротиворечивое множество формул, не имеющее модели. Тогда ясно, что для любой формулы $F$ справедливо семантическое следование $\Phi\vDash F$ . В силу теоремы адекватности отсюда следует, что $\Phi\vdash F$ для любой $F$ , что означает противоречивость множества $\Phi$ , в противоречие с условием. Теорема 29.14 (теорема Гёделя о полноте ФИП). Класс доказуемых замкнутых формул совпадает с классом общезначимых (или тождественно истинных) формул: $\vdash F \Leftrightarrow\vDash F$ . Доказательство. Эта теорема непосредственно вытекает из предыдущей при $\Phi= \varnothing$ . Справедлива она и для открытых формул. В самом деле, если $\vDash F(x_1,\ldots,x_n)$ , где $x_1,\ldots,x_n$ — свободные предметные переменные в формуле $F$ , то в силу определения квантора общности это будет равносильно тому, что $\vDash(\forall x_1)\ldots (\forall x_n) \bigl(F(x_1,\ldots,x_n)\bigr)$ . По теореме 29.14 это равносильно тому, что $\vdash(\forall x_1)\ldots (\forall x_n) \bigl(F(x_1,\ldots,x_n)\bigr)$ . В силу свойств выводимости последнее утверждение равносильно тому, что $\vdash F(x_1,\ldots,x_n)$ . Неполнота формализованного исчисления предикатов в абсолютном и узком смыслах В учебнике обсуждаются два понятия полноты аксиоматической теории: абсолютная полнота и полнота в узком смысле (см. определение 27.6). Доказанная теорема 29.14 может быть истолкована как некая внешняя полнота формализованного исчисления предикатов, его полнота относительно логики предикатов: в этой теории могут быть формально доказаны все общезначимые формулы логики предикатов. Рассмотрим вопросы внутренней полноты формализованного исчисления предикатов, т.е. выясним, будет ли эта теория абсолютно полной и полной в узком смысле (см. определения 27.5 и 27.6). Поскольку на основании теоремы 29.14 множество теорем формализованного исчисления предикатов совпадает с множеством тавтологий (общезначимых формул) логики предикатов, а в логике предикатов существуют выполнимые, но не общезначимые формулы, формализованное исчисление предикатов не является абсолютно полной теорией. Здесь ситуация аналогична соответствующей ситуации в формализованном исчислении высказываний. Что же касается полноты формализованного исчисления предикатов в узком смысле, то исчисление предикатов (в отличие от исчисления высказываний, см. теорему 28.4) таким свойством не обладает. Для доказательства приведем пример формулы, не являющейся теоремой формализованного исчисления предикатов, добавление которой к аксиомам исчисления предикатов (с сохранением правил вывода) приводит к непротиворечивой формальной аксиоматической теории. Пример 29.15. Рассмотрим формулу $(\exists x)(F(x))\to (\forall x)(F(x))$ . Нетрудно убедиться в том, что она не является общезначимой (приведите пример конкретного одноместного предиката, превращающего эту формулу в ложное высказывание). Поэтому на основании теоремы К. Гёделя о полноте она не доказуема в формализованном исчислении предикатов. С другой стороны, добавив к аксиомам формализованного исчисления предикатов рассматриваемую формулу, получим непротиворечивую формальную теорию $T$ . Ее непротиворечивость можно доказать следующим образом. Рассмотрим модель этой теории на одноэлементном множестве $M=\{a\}$ . Ясно, что данная формула тождественно истинна на $M$ . Далее, учитывая, что на $M$ можно определить для каждого натурального $n$ лишь два n-местных предиката $P_1^n$ и $P_2^n$ , причем $\lambda(P_1^n(a,\ldots,a))=0$ и $\lambda(P_2^n(a,\ldots,a))=1$ , нетрудно доказать, что все аксиомы новой теории $T$ тождественно истинны на этой модели и правила вывода от тождественно истинных на $M$ формул приводят к тождественно истинным на $M$ формулам. Таким образом, доказывается утверждение: всякая теорема теории $T$ тождественно истинна на одноэлементном множестве $M$ . Следовательно, если бы для некоторой формулы $F$ обе формулы $F$ и $\lnot F$ были теоремами теории $T$ , то они были бы тождественно истинны на одноэлементном множестве $M$ , что невозможно. Поэтому расширенная теория $T$ непротиворечива, что и доказывает неполноту в узком смысле формализованного исчисления предикатов. Теорема компактности Мы уже отмечали (см. теорему 15.3, б) и неоднократно использовали тот простой факт, непосредственно вытекающий из определения понятия вывода, что $\Phi\vdash F$ тогда и только тогда, когда $\Phi_0\vdash F$ , где $\Phi_0$ — некоторое конечное подмножество множества $\Phi$ формул. Теорема адекватности, установленная на основании выдающейся теоремы Гёделя о существовании модели, позволяет получить из этого тривиального соображения аналогичную теорему семантического содержания, уже отнюдь не столь очевидную. Теорема 29.16 (теорема К. Гёделя–А. И. Мальцева). Если $\Phi\vDash F$ , то для некоторого конечного подмножества $\Phi_0\subset\Phi$ имеет место $\Phi_0\vDash F$ . Доказательство. Если $\Phi\vDash F$ , то по теореме 29.13 (теорема адекватности) $\Phi\vdash F$ . В силу сделанного перед настоящей теоремой замечания найдется такое конечное подмножество $\Phi_0\subset\Phi$ , что $\Phi_0\vdash F$ . Отсюда по теореме оправданности (следствие 29.2 из теоремы 29.1) заключаем, что $\Phi_0\vDash F$ . Следствие 29.17(локальная теорема К. Гёделя—А. И. Мальцева). Множество $\Sigma$ замкнутых формул узкого исчисления предикатов сигнатуры $\sigma$ имеет модель тогда и только тогда, когда каждое его конечное подмножество имеет модель. Доказательство. Необходимость очевидна. Обратно, пусть каждое конечное подмножество множества $\Sigma$ имеет модель. Тогда $\Sigma$ — синтаксически непротиворечиво. (Если бы это было не так, то для некоторой формулы $F$ имелись бы выводимости $\Sigma\vdash F$ и $\Sigma\vdash\lnot F$ , а значит, нашлось бы такое конечное подмножество $\Sigma_0\subset \Sigma$ , что $\Sigma_0\vdash F$ и $\Sigma_0\vdash\lnot F$ , то есть $\Sigma_0$ было бы синтаксически противоречиво, а значит, по теореме 29.12 не имело бы модели, что противоречило бы условию.) Следовательно, по теореме 29.10 о существовании модели множество $\Sigma$ имеет модель. Следствие доказано. В заключение приведем еще одну теорему о формулах узкого исчисления предикатов и их моделях. Теорема 29.18 (Лёвенгейм–Сколем). Пусть $\sigma$ — счетная сигнатура и $\Sigma$ — множество замкнутых формул узкого исчисления предикатов сигнатуры $\sigma$ . Если $\Sigma$ имеет модель, то $\Sigma$ имеет счетную модель. Доказательство. Пусть $\sigma= \bigl\{a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots \bigr\}$ и множество $\Sigma$ формул имеет модель. Тогда (по теореме 29.12) $\Sigma$ синтаксически непротиворечиво и модель этого множества формул может быть построена, как в доказательстве теоремы 29.10. Построенная таким образом модель будет счетной: она состоит из элементов $a_0,a_1,\ldots;\, c_0,c_1,\ldots$ и всех термов (не содержащих переменных), построенных из констант $a_i,\,c_j$ . Эти термы можно занумеровать, например, по следующему правилу: $\nu(a_i)=4i+1,\quad \nu(c_i)=4i+3,\quad \nu\bigl(f_i(t_1,\ldots,t_{n_i})\bigr)= 2^{n_{n_i}+1}\cdot 3^{\nu(t_1)}\cdot 5^{\nu(t_2)}\cdot \ldots\cdot p_{n_i}^{\nu(t_{ni})},$ где $p_0=2,\,p_1=3,\,p_2=5,\,\ldots,\,p_{n_i},\,\ldots$ — последовательность простых чисел. Эта теорема может быть доказана и в более общей мощностной формулировке: если множество $\Sigma$ формул имеет бесконечную модель и мощность множества всех букв, из которых составлены формулы из $\Sigma$ , равна $n$ , то для любой бесконечной мощности $m\geqslant n$ существует модель множества $\Sigma$ мощности $m$ . Укажем два следствия этой теоремы: 1) если $\Sigma$ — множество формул мощности $n$ , имеющее бесконечную модель, то $\Sigma$ имеет бесконечные модели любых мощностей, превышающих $n$ ; 2) всякое конечное множество или счетное непротиворечивое множество формул либо имеет только конечные модели, либо имеет бесконечные модели любых мощностей. Теорема Лёвенгейма–Сколема дает ряд поразительных следствий двух типов: одни из них гласят, что некоторая теория имеет неожиданно обширные модели, другие — что теория имеет неожиданно узкие модели. Дальнейшее развитие эта мысль получит в следующей лекции. Математический форум (помощь с решением задач, обсуждение вопросов по математике). Если заметили ошибку, опечатку или есть предложения, напишите в комментариях.

Свойства формализованного исчисления предикатов

Онлайн-сервисы

Нахождение НОД и НОК Разложение числа на простые множители Сравнения по модулю Операции над множествами Операции над векторами Разложение вектора по базису. Доказательство, что векторы образуют базис Чертёж треугольника по координатам вершин Решение треугольника Решение Пирамиды Построение Пирамиды по координатам вершин Чертёж многоугольника по координатам вершин Решение систем методом Крамера и Матричным Онлайн построение графика кривой 2-го порядка Определение вида кривой или поверхности 2-го порядка по инвариантам МНК и регрессионный анализ Онлайн + графики Онлайн число, сумма и дата прописью

Алгоритмы JavaScript

Алгоритмы поиска Алгоритмы сортировки Уникальные элементы массива Объединение, пересечение и разность массивов НОД и НОК Операции над матрицами Дата прописью

Введение в анализ

Функции: понятие, определение, графики Непрерывность функции Исследование функции и построение графика

Теория множеств

Множества: понятие, определение, примеры Точечные множества Замкнутые и открытые множества Мера множества Группы, кольца, поля в математике Поле комплексных чисел Кольцо многочленов Основная теорема алгебры и ее следствия

Математическая логика

Алгебра высказываний

Аксиоматика и логические рассуждения Методы доказательств теорем Алгебра высказываний и операции над ними Формулы алгебры высказываний Тавтологии алгебры высказываний Логическая равносильность формул Нормальные формы для формул высказываний Логическое следование формул Приложение алгебры высказываний для теорем Дедуктивные и индуктивные умозаключения Решение логических задач Принцип полной дизъюнкции

Булевы функции

Множества, отношения и функции в логике Булевы функции от одного и двух аргументов Булевы функции от n аргументов Системы булевых функций Применение булевых функций к релейно-контактным схемам Релейно-контактные схемы в ЭВМ Практическое применение булевых функций

Теория формального

Формализованное исчисление высказываний Полнота и другие свойства формализованного исчисления высказываний Независимость системы аксиом формализованного исчисления высказываний

Логика предикатов

Логика предикатов Логические операции над предикатами Кванторные операции над предикатами Формулы логики предикатов Тавтологии логики предикатов Преобразования формул и следование их предикатов Проблемы разрешения для общезначимости и выполнимости формул Применение логики предикатов в математике Строение математических теорем Аристотелева силлогистика и методы рассуждений Принцип полной дизъюнкции в предикатной форме Метод полной математической индукции Необходимые и достаточные условия Логика предикатов и алгебра множеств Формализованное исчисление предикатов

Неформальные и формаль-
ные аксиоматические теории

Неформальные аксиоматические теории Свойства аксиоматических теорий Формальные аксиоматические теории Формализация теории аристотелевых силлогизмов Свойства формализованного исчисления предикатов Формальные теории первого порядка Формализация математической теории

Теория алгоритмов

Интуитивное представление об алгоритмах Машины Тьюринга и тезис Рекурсивные функции Нормальные алгоритмы Маркова Разрешимость и перечислимость множеств Неразрешимые алгоритмические проблемы Теорема Гёделя о неполноте формальной арифметики

Математическая логика и компьютеры

Математическая логика и языки программирования Применение компьютеров для доказательства теорем математической логики Математическая логика и логическое программирование Математическая логика и информатика Математическая логика и искусственный интеллект

Дискретная математика

Множества и отношения

Теория множеств: понятия и определения Операции над множествами Кортеж и декартово произведение множеств Соответствия и бинарные отношения на множествах Операции над соответствиями на множествах Семейства множеств Специальные свойства бинарных отношений Отношения эквивалентности на множестве Упорядоченные множества Теорема о неподвижной точке Мощность множества Парадокс Рассела Метод характеристических функций

Группы и кольца

Алгебраические структуры и операции Группоиды, полугруппы, группы Кольца, тела, поля Области целостности в теории колец Модули и линейные пространства Подгруппы и подкольца Теорема Лагранжа о порядке конечной группы Гомоморфизмы групп и нормальные делители Гомоморфизмы и изоморфизмы колец Алгебра кватернионов

Полукольца и булевы алгебры

Полукольца: определение, аксиомы, примеры Замкнутые полукольца Полукольца и системы линейных уравнений Булевы алгебры и полукольца Решетки и полурешетки

Алгебраические системы

Алгебраические системы: модели и алгебры Подсистемы алгебраических систем Конгруэнции и фактор-системы Гомоморфизмы алгебраических систем Прямые произведения алгебраических систем Конечные булевы алгебры Многосортные алгебры

Теория графов

Теория графов: основные понятия и определения Способы представления графов Неориентированные и ориентированные деревья Остовное дерево и алгоритм Краскала Методы систематического обхода вершин графа Алгоритмы поиска в глубину и ширину в графах Задача о путях во взвешенных ориентированных графах Изоморфизм, гомоморфизм и автоморфизм графов Топологическая сортировка вершин графа Элементы цикломатики в теории графов

Булева алгебра и функции

Булевы функции и булев куб Таблицы булевых функций и булев оператор Равенство булевых функций. Фиктивные переменные Формулы и суперпозиции булевых функций Дизъюнктивные и конъюнктивные нормальные формы Построение минимальных ДНФ Теорема Поста и классы Критерий Поста Схемы из функциональных элементов

Конечные автоматы и регулярные языки

Конечные автоматы и регулярные языки Алфавит, слово, язык в программировании Порождающие грамматики (грамматики Хомского) Классификация грамматик и языков Регулярные языки и регулярные выражения Конечные автоматы Допустимость языка конечным автоматом Теорема Клини Детерминизация конечных автоматов Минимизация конечных автоматов Лемма о разрастании для регулярных языков Обоснование алгоритма детерминизации автоматов Конечные автоматы с выходом Морфизмы и конечные подстановки Машины Тьюринга

Контекстно-свободные языки

Контекстно-свободные языки и грамматики Приведенная форма КС-грамматики Лемма о разрастании для КС-языков Магазинные автоматы (автомат с магазинной памятью) Алгоритм построения МП-автомата по КС-грамматике Алгоритм построения КС-грамматики по МП-автомату Алгебраические свойства КС-языков Основное свойство суперпозиции КС-языков Пересечение контекстно-свободных языков Методы синтаксического анализа КС-языков Восходящий синтаксический анализ и LR(k)-грамматики Семантика формальных языков Принцип индукции по неподвижной точке Графовое представление МП-автоматов

Интегральное исчисление

Неопределённый и определённый

Неопределенный и определенный интегралы Свойства интегралов Интегрирование по частям Интегрирование методом замены переменной Интегрирование различных рациональных функций Интегрирование различных иррациональных функций Интегрирование различных тригонометрических функций Определенный интеграл и его основные свойства Необходимое и достаточное условие интегрируемости Теоремы существования первообразной Свойства определенных интегралов Несобственные интегралы Интегральное определение логарифмической функции

Приложения интегралов

Вычисление площадей плоских фигур Площади фигур в различных координатах Вычисление объемов тел с помощью интегралов Объём тела вращения Вычисление длин дуг кривых Формулы длины дуги регулярной кривой Кривизна плоской кривой Площадь поверхности вращения тела

Интегралы в физике

Статические моменты и координаты центра тяжести Теоремы Гульдина–Паппа Вычисление моментов инерции Другие приложения интегралов в физике

Основные интегралы

Интеграл Ньютона-Лейбница Интеграл Римана Интеграл Лебега

Вариационное исчисление

Примеры вариационных задач Дифференциальное уравнение Эйлера Функционалы, зависящие от нескольких функций Задача о минимуме кратного интеграла

Финансовый анализ

Анализ эффективности

Критерии и показатели эффективности предприятия Методы анализа эффективности деятельности Факторный анализ прибыли от операционной деятельности Анализ безубыточности предприятия Операционный рычаг и эффект финансового рычага Анализ и оценка состава, структуры и динамики доходов и расходов Анализ рентабельности и резервов устойчивого роста капитала Анализ распределения прибыли предприятия Анализ и оценка чувствительности показателей эффективности

Анализ устойчивости

Финансовая устойчивость и долгосрочная платежеспособность Характеристика типов финансовой устойчивости

Рыночная активность

Финансовый анализ рыночной активности Методика анализа рыночной активности Анализ и оценка дивидендного дохода на одну акцию

Инвестиционная деятельность

Инвестиции: экономическая сущность и классификация Государственное регулирование инвестиционной деятельности Источники финансовых ресурсов на капитальные вложения Инвестиции в основные фонды Оценка состояния основных фондов Амортизация основных фондов Капитальное строительство в инвестиционном процессе Планирование инвестиций в форме капитальных вложений Экономическая эффективность инвестиций Финансирование капитальных вложений Кредитование капитальных вложений Кредитоспособность Финансирование и кредитование затрат Финансирование и кредитование инвестиционной деятельности потребительской кооперации Финансирование и кредитование капитальных вложений потребительской кооперации Инвестиционное строительное проектирование

Анализ инвестиций

Инвестиции и инвестиционная деятельность предприятия Задачи финансового анализа инвестиций предприятия Учет фактора времени в инвестиционной деятельности Аннуитет и финансовая рента в инвестициях Учет фактора инфляции при инвестировании Оценка фактора риска инвестиционного проекта Методы оценки эффективности инвестиций Показатели эффективности инвестиционного проекта

Стоимость компании

Концепция построения международных стандартов финансовой отчетности (МСФО) Экономическое содержание международных стандартов финансовой отчётности Цели и принципы оценки стоимости акций и активов компании Оценка акций и активов предприятия по справедливой стоимости Методы оценки справедливой стоимости акций предприятия Затратный подход к оценки стоимости компаний и акций Сравнительный подход к оценки стоимости предприятий и акций Доходный подход к оценке стоимости компании и акций Выбор ставки дисконтирования при инвестировании в акции Метод капитализации прибыли Сравнение подходов к оценке стоимости компаний и пакетов акций

Форвардные контракты

Форвардный контракт и цена Форвардная цена акции на бирже Цена форвардного контракта инвестора Форвардная цена акции с учетом величины дивиденда Форвардная цена акции с учетом ставки дивиденда Форвардная цена валюты на рынке форекс Форвардный валютный курс и инфляция на рынке Форвардная цена товара и спотовый рынок Форвардная цена при различии ставок по кредитам и депозитам Синтетический форвардный контракт на акции и валюту

Теория вероятностей

Основные понятия теории вероятностей Зависимые и независимые случайные события Повторные независимые испытания Формула Бернулли Одномерные случайные величины Многомерные случайные величины Функции случайных величин Законы распределения целочисленных случайных величин Законы распределения непрерывных случайных величин Предельные теоремы теории вероятностей Закон больших чисел и предельные теоремы Вероятностные закономерности

Математическая статистика

Элементы математической статистики Выборочный метод Оценки параметров генеральной совокупности Статистические гипотезы Критерии согласия Теоретические и эмпирические частоты

Теория очередей (СМО)

Определение системы массового обслуживания Уравнения Колмогорова Предельные вероятности состояний Определение СМО с отказами Определение СМО с ожиданием (очередью)

Аналитическая геометрия

Векторная алгебра

Метрические понятия и аксиомы геометрии Равенство и подобие геометрических фигур Бинарные отношения Вектор, его направление и длина Линейные операции над векторами Линейная зависимость и независимость векторов Отношение коллинеарных векторов Проекции векторов на прямую и на плоскость Угол между векторами Ортогональные проекции векторов Координата вектора на прямой и базис Координаты вектора на плоскости и базис Координаты вектора в пространстве и базис Операции над векторами в координатной форме Ортогональный и ортонормированный базисы Cкалярное произведение векторов и его свойства Выражение скалярного произведения через координаты векторов Векторное произведение векторов и его свойства Смешанное произведение векторов и его свойства Ориентированные площади и объемы Двойное векторное произведение и его свойства Применение векторов в задачах на аффинные свойства фигур Применение произведений векторов при решении геометрических задач Применение векторной алгебры в механике

Системы координат

Прямоугольные координаты Преобразования прямоугольных координат Полярная система координат Цилиндрическая система координат Сферические координаты Аффинные координаты Аффинные преобразования координат Аффинные преобразования плоскости Примеры аффинных преобразований плоскости Аффинные преобразования пространства Многомерное координатное пространство Линейные и аффинные подпространства Скалярное произведение n-мерных векторов Преобразования систем координат

Геометрия на плоскости

Алгебраические линии на плоскости Общие уравнения геометрических мест точек Алгебраические уравнения линий на плоскости Уравнения прямой, проходящей через точку перпендикулярно вектору Уравнения прямой, проходящей через точку коллинеарно вектору Уравнения прямой, проходящей через две точки Уравнения прямой с угловым коэффициентом Взаимное расположение прямых Примеры задач с прямыми на плоскости Системы неравенств с двумя неизвестными Системы линейных уравнений с двумя неизвестными

Линии 2-го порядка

Канонические уравнения линий второго порядка Порядок приведения уравнения линии к каноническому виду Эллипс Гипербола Парабола Квадратичные неравенства с двумя неизвестными Применение линий 1-го и 2-го порядков в задачах на экстремум функций

Инварианты линий

Классификация линий 2-го порядка по инвариантам Приведение уравнения линии к каноническому виду по инвариантам

Геометрия в пространстве

Способы задания ГМТ в пространстве Алгебраические уравнения поверхностей Уравнения плоскости, проходящей через точку перпендикулярно вектору Уравнения плоскости, компланарной двум неколлинеарным векторам Уравнения плоскости, проходящей через три точки Взаимное расположение плоскостей Типовые задачи с плоскостями Уравнения прямых в пространстве Взаимное расположение прямых в пространстве Типовые задачи с прямыми в пространстве

Поверхности 2-го порядка

Канонические уравнения поверхностей Порядок приведения уравнения поверхности к каноническому виду Поверхности второго порядка Эллипсоиды Гиперболоиды Конусы Параболоиды Применение поверхностей 1-го и 2-го порядков в задачах на экстремум функций

Инварианты поверхностей

Классификация поверхностей 2-го порядка по инвариантам Квадратичные неравенства с тремя неизвестными Приведение уравнения поверхности к канониче-скому виду по инвариантам

Линейная алгебра

Матрицы и операции

Линейные операции над матрицами Умножение матриц Возведение матриц в степень Многочлены от матриц Транспонирование и сопряжение матриц Блочные матрицы Произведение и сумма матриц Кронекера Метод Гаусса приведения матрицы к ступенчатому виду Элементарные преобразования матриц

Определители

Определители матриц и их основные свойства Формула полного разложения определителя Формула Лапласа полного разложения определителя Определитель произведения матриц Методы вычисления определителей

Ранг матрицы

Линейная зависимость и линейная независимость строк (столбцов) матрицы Ранг матрицы и базисный минор матрицы Методы вычисления ранга матрицы Ранг системы столбцов (строк)

Обратная матрица

Обратные матрицы и их свойства Ортогональные и унитарные матрицы Способы нахождения обратной матрицы Матричные уравнения Односторонние обратные матрицы Скелетное разложение матрицы Полуобратная матрица Псевдообратная матрица

Системы уравнений

Системы линейных алгебраических уравнений Метод Гаусса решения систем линейных уравнений Структура общего решения системы уравнений Решение систем с помощью полуобратных матриц Псевдорешения системы линейных уравнений

Функциональные матрицы

Функциональные матрицы скалярного аргумента Производные матриц по векторному аргументу Линейные и квадратичные формы и их преобразования Приведение форм к каноническому виду Закон инерции вещественных квадратичных форм Знакоопределенность форм вещественных квадратичных Формы и исследование функций на экстремум

Многочленные матрицы

Многочленные матрицы (лямбда-матрицы) Операции над лямбда-матрицами Простые преобразования многочленных матриц Инвариантные множители многочленной матрицы

Функции от матриц

Собственные векторы и значения матрицы Подобие числовых матриц Характеристический многочлен матрицы Минимальный многочлен матрицы Теорема Гамильтона-Кэли Жорданова форма матрицы Приведение матрицы к жордановой форме Многочлены от матриц Применение многочленов от матриц Функции от матриц

Линейные пространства

Линейные пространства: определение и примеры Линейная зависимость и независимость n-мерных векторов Размерность и базис линейного пространства Преобразования координат в линейном пространстве Изоморфизм линейных пространств

Подпространства

Подпространства линейного пространства Пересечение и сумма подпространств Способы описания подпространств Нахождение дополнения и суммы подпространств Нахождение пересечения подпространств

Линейные отображения

Линейные многообразия Линейные отображения Матрица линейного отображения Ядро и образ линейного отображения

Линейные операторы

Линейные операторы (преобразования) Инвариантные подпространства Собственные векторы и значения оператора Свойства собственных векторов операторов Канонический вид линейного оператора Методика приведения линейного преобразования к каноническому виду

Евклидовы пространства

Комплексный анализ

Комплексные числа

Комплексные числа в алгебраической форме Комплексные числа в тригонометрической и показательной формах Множества на комплексной плоскости Последовательности и ряды комплексных чисел

Комплексные функции

Функции комплексного переменного. Предел, непрерывность и производная Элементарные функции комплексного переменного Дифференцирование функций комплексного переменного Аналитические функции и их свойства Конформные отображения
и их свойства Интегрирование функций комплексного переменного

Функциональные ряды в комплексной области

Функциональные ряды и последовательности Степенные ряды и их свойства Разложение функций в степенные ряды Нули аналитических функций Ряд Лорана и разложение функций по целым степеням

Особые точки, Вычеты

Изолированные особые точки функций и полюсы Вычеты и их применение Вычисление интегралов с помощью вычетов Вычеты и расположение нулей многочлена

Операционное исчисление

Преобразование Лапласа и его свойства Решение ДУ операционным методом Анализ выходных процессов линейных стационарных систем Z-преобразование и его свойства

Дифференциальные уравнения

ДУ первого порядка

Основные понятия и определения ДУ Метод изоклин для ДУ 1-го порядка Метод последовательных приближений ДУ с разделяющимися переменными Однородные ДУ Линейные ДУ 1-го порядка Дифференциальное уравнение Бернулли ДУ в полных дифференциалах Интегрирующий множитель ДУ, не разрешенные относительно производной Дифференциальное уравнение Риккати Составление ДУ семейств линий Задачи на траектории Особые решения ДУ

ДУ высших порядков

Понятия и определения ДУ высших порядков ДУ, допускающие понижение порядка Линейная независимость функций Определители Вронского и Грама Однородные и неоднородные дифференциальные уравнения Задача Коши и Уравнение Эйлера Линейные ДУ с переменными коэффициентами Метод Лагранжа решения ДУ Краевые задачи для ДУ высших порядков Разложение решения ДУ в степенной ряд Разложение решения ДУ в обобщенный степенной ряд Нахождение периодических решений ДУ Асимптотическое интегрирование ДУ

Системы ДУ

Системы ДУ: понятия и определения Сведение системы ДУ к одному уравнению Нахождение интегрируемых комбинаций Интегрирование однородных линейных систем ДУ Методы интегрирования неоднородных систем ДУ Преобразование Лапласа и решение ДУ и систем

Теория устойчивости

Устойчивость решений ДУ по Ляпунову Простейшие типы точек покоя Метод функций Ляпунова Устойчивость решений ДУ по первому приближению Критерии устойчивости Рауса–Гурвица и Михайлова ДУ с малым параметром при производной

Численные методы

Методы алгебры

Численные методы линейной алгебры Численные методы решения СЛАУ Итерационный метод Шульца обратной матрицы Методы решения задач о собственных значениях и векторах матрицы Методы решения нелинейных уравнений Методы решения систем нелинейных уравнений

Методы теории приближений

Методы приближения сеточных функций Методы функциональной интерполяции Методы интегрально-дифференциальной интерполяции Методы интегрального сглаживания Методы интерполяции и сглаживания сплайнами Методы численного дифференцирования и интегрирования Методы численного дифференцирования Методы численного интегрирования

Методы решения обыкновенных ДУ

Численные методы решения задачи Коши Разностные схемы для решения задачи Коши Составные схемы для решения задачи Коши Экстраполяционные методы решения задачи Коши Непрерывно-дискретные методы решения задачи Коши Численные методы решения краевых задач

Методы решения ДУ в частных производных

Численные методы решения уравнений математической физики с двумя переменными Принципы построения разностных схем для уравнений в частных производных Разностные схемы решения уравнений в частных производных 1-го порядка Разностные схемы решения уравнений в частных производных 2-го порядка Численные методы решения уравнений в частных производных Численные методы решения уравнений математической физики с тремя переменными

Свойства формализованного исчисления предикатов

Формализованное исчисление предикатов (ФИП) развито достаточно глубоко, и теперь, как и в случае формализованного исчисления высказываний, надлежит рассмотреть свойства (или метатеорию) этого исчисления. Но теперь в области предикатов логика достигает такой выразительной силы, что становится логическим основанием конкретных математических теорий, и теоремы (по сути, метатеоремы) о логике рассуждений достигают поистине философской глубины.

Оправданность аксиоматизации

Теорема оправданности аксиоматизации утверждает, что если $\Phi\vdash F$ , то $\Phi\vDash F$ , т.е. из синтаксической выводимости следует семантическая выводимость. Ее очевидным следствием будет утверждение о том, что всякая теорема ФИП является общезначимой формулой (тавтологией) логики предикатов. Смысл этой теоремы состоит в утверждении фактически того, что мы не были "излишне щедры" в выборе аксиом и правил вывода для нашего формального исчисления и не включили в их число ничего лишнего, ибо доказуемыми в этом исчислении оказываются лишь общезначимые формулы логики предикатов. Доказательство этой теоремы не очень сложное, и мы получим ее в качестве следствия несколько более общей теоремы. Обратное же утверждение "если $\Phi\vDash F$ , то $\Phi\vdash F$ (т.е. при выборе аксиом и правил вывода мы не проявили и "излишней скромности", и для всякой общезначимой формулы логики предикатов в нашем ФИП вполне достаточно формальных средств, чтобы доказать ее), уже не столь очевидно, и доказательство его, приводимое дальше, потребует от нас значительно больших усилий.

Теорема оправданности имеет глубокий смысл: она оправдывает наши занятия математикой, убеждая в том, что наши логические рассуждения и умопостроения не уводят нас от смысла и от практики.

Теорема 29.1. Если в алгебраической системе $\mathbf{M}$ выполняются все формулы из множества $\Phi$ и из $\Phi$ синтаксически выводима формула $F$ , то $F$ также выполняется в $\mathbf{M}\colon \mathbf{M}\vDash \Phi$ и $\Phi\vdash F \Rightarrow \mathbf{M}\vDash F$ .

Доказательство разделим на три этапа. На первом этапе отметим, что каждая аксиома ФИП есть тождественно истинная формула. Что касается аксиом $A1,\,A2,\,A3$ исчисления высказываний, то их тождественная истинность установлена нами в алгебре высказываний (см. теоремы 3.1 з, 3.3, а, л). Общезначимость аксиом $\mathsf{PA1}$ и $\mathsf{PA2}$ установлена в теореме 21.13.

На втором этапе покажем, что все три правила вывода, используемые в ФИП, обладают следующим семантическим свойством. Если алгебраическая система $\mathbf{M}$ служит моделью для всех посылок правила вывода, то $\mathbf{M}$ будет моделью и для формулы, получаемой из данных формул с помощью данного правила вывода. Докажем это утверждение для трех из правил вывода.

Правило MP. Допустим, что $\mathbf{M}\vDash F\to G$ и $\mathbf{M}\vDash F$ . Докажем, что тогда $\mathbf{M}\vDash G$ . Возьмем любую подстановку $\alpha$ констант из $\mathbf{M}$ . Тогда, по условию, каждое из высказываний $F(\alpha)\to G(\alpha)$ и $F(\alpha)$ , получаемых соответственно из формул $F\to G$ и $F$ в результате подстановки предметных констант $\alpha$ , будет истинным. Тогда истинным будет и высказывание $F(\alpha)$ , то есть $\mathbf{M}\vDash_{\alpha}G$ . Это и означает, что $\mathbf{M}\vDash G$ .

$\forall$ -правило. Допустим, что $\mathbf{M}\vDash G(y)\to F(x,y)$ , где $x$ не входит свободно в формулу $G$ , а $y$ обозначает все свободные предметные переменные в формулах $F$ и $G$ (в $F$ — кроме $x$ ). Тогда сделанное допущение означает, что для любых элементов $a,b\in M$ (где $M$ — носитель алгебраической системы $\mathbf{M}$ ) высказывание $G(b)\to F(a,b)$ истинно в $\mathbf{M}$ . Рассмотрим теперь высказывание $G(b)\to (\forall x)(F(x,b))$ и покажем, что оно истинно в $\mathbf{M}$ при любом $b\in M$ . В самом деле, если $G(b)$ ложно, то рассматриваемое высказывание истинно. Если же $G(b)$ истинно, то, по отмеченному выше, истинным будет и высказывание $F(a,b)$ . Поскольку оно будет истинным при любом $a\in M$ , то отсюда вытекает истинность для таких $b\in M$ высказывания $(\forall x)(F(x,b))$ . Это, в свою очередь, влечет истинность высказывания $G(b)\to (\forall x)(F(x,b))$ для тех $b\in M$ , для которых $G(b)$ истинно. Итак, высказывание $G(b)\to (\forall x)(F(x,b))$ истинно для любых $b\in M$ . Это и означает, что $\mathbf{M}\vDash G(y)\to (\forall x)(F(x,y))$ .

$\exists$ -правило. Подобно предыдущему правилу, доказывается, что если $\mathbf{M}\vDash F(x)\to G$ , то $\mathbf{M}\vDash (\exists x)(F(x))\to G$ .

Наконец, на третьем этапе докажем утверждение самой теоремы. Пусть $\mathbf{M}\vDash \Phi$ и $\Phi\vdash F$ . Последнее означает, что имеется вывод $B_1,B_2,\ldots,B_m$ формулы $F$ из множества формул $\Phi$ (в частности, $B_m\equiv F$ ). Покажем, что каждый элемент этой последовательности является формулой, выполняющейся в $\mathbf{M}$ . Доказательство проведем индукцией по номеру $k$ формулы в рассматриваемом выводе. При $k=1$ , если $B_1\in\Phi$ , то, по условию, $\mathbf{M}\vDash B_1$ . Если $B_1$ — аксиома, то она общезначима и, в частности, $\mathbf{M}\vDash B_1$ . Предположим теперь, что при всех $k<n~(n\geqslant2)$ все формулы $B_k$ выполняются в $\mathbf{M}$ , то есть $\mathbf{M}\vDash B_k$ . Рассмотрим формулу $B_n$ . Если $B_n\in\Phi$ или $B_n$ — аксиома, то, как отмечено выше, $\mathbf{M}\vDash B_n$ . Если же $B_n$ получена из предыдущих формул последовательности по одному из трех правил вывода, то (на основании выполнимости всех предыдущих формул в $\mathbf{M}$ ) в силу утверждений (см. второй этап) заключаем, что и $B_n$ выполняется в $\mathbf{M}$ , то есть $\mathbf{M}\vDash B_n$ . Окончательно заключаем, что все формулы последовательности $B_1,B_2,\ldots,B_m$ истинны в $\mathbf{M}$ , в частности $\mathbf{M}\vDash F$ . Теорема полностью доказана.

Следствие 29.2 (теорема оправданности). Из синтаксической выводимости следует семантическая выводимость, т. е. если $\Phi\vdash F$ , то $\Phi\vDash F$ .

Доказательство. Пусть $\Phi\vdash F$ и пусть $\mathbf{M}$ — любая алгебраическая система, в которой выполняются все формулы из $\Phi$ , то есть $\mathbf{M}\vDash\Phi$ . Тогда по доказанной теореме $\mathbf{M}\vDash F$ . По определению семантического следствия это и означает, что $\Phi\vDash F$ .

Следствие 29.3. Всякая доказуемая формула является общезначимой (т.е. любая теорема истинна): если $\vdash F$ , то $\vDash F$ .

Доказательство получается из предыдущего следствия при $\Phi=\varnothing$ .

Непротиворечивость формализованного исчисления предикатов

Важнейшим компонентом критерия оправданности всякой математической теории является ее непротиворечивость, т.е. невозможность доказательства в ней некоторого утверждения и его отрицания одновременно. Трудности, связанные с доказательством этого свойства математических теорий (а одной из причин этих трудностей, несомненно, было отсутствие в содержательных математических теориях точного понятия доказательства), привели к тому, что в математике более естественным стал другой признак непротиворечивости теории, основанный на возможностях реализации этой теории, ее моделируемости. Но в то же время этот подход и привел к возникновению парадоксов в математике, которые, в свою очередь, привели к возникновению науки об основаниях математики и к концепциям формального подхода к понятиям доказательства и математической (аксиоматической) теории. Одной из задач этого подхода была выработка такого формального понятия доказательства, при котором для конкретной математической теории понятие ее формальной непротиворечивости совпало бы с понятием ее содержательной непротиворечивости. Факт такого совпадения, в силу точности определения доказательства, становится математической теоремой (точнее, метатеоремой). Отметим, что привыкание в математике к эквивалентности этих двух понятий непротиворечивости было непростым. В частности, неприятие современниками неевклидовых геометрий Лобачевского–Бояи объясняется также и тем, что законность этих теорий обосновывалась отсутствием в них противоречий — аргументом, совпадающим по существу с современным понятием формальной непротиворечивости. Геометрические модели для этих теорий, доказывающие их содержательную непротиворечивость, были найдены позднее.

Наша задача состоит в том, чтобы в рамках формализованного (узкого) исчисления предикатов дать точные определения двух понятий непротиворечивости и установить их эквивалентность.

Напомним, что формула логики предикатов называется общезначимой, если она истинна в любой интерпретации, и противоречивой, если она ложна в любой интерпретации, т.е. если ее отрицание общезначимо. Эти семантические понятия, связывающие непротиворечивость с истинностью, позволяют сформулировать понятие семантически непротиворечивой теории.

Определение 29.4. Формальная теория называется семантически непротиворечивой, если ни одна из ее теорем (формул) не является противоречивой, т. е. ложной при любой ее интерпретации. Аналогично, множество $\Phi$ формул называется семантически непротиворечивым, если ни одна формула, выводимая из $\Phi$ , не является противоречивой.

В теореме 16.1 доказано, что всякая теорема формализованного исчисления высказываний общезначима (тождественно истинна), а потому не является противоречивой. Это означает, что формализованное исчисление высказываний семантически непротиворечиво. Аналогичная теорема доказана и для формализованного исчисления предикатов (см. следствие 29.3 из теоремы 29.1 выше). Значит, и ФИП семантически непротиворечиво. Семантическая непротиворечивость ФИВ и ФИП означает, что эти формальные теории пригодны для описания любых классов алгебраических систем, т.е. они войдут в теории этих классов составными частями, что вполне соответствует общенаучному принципу универсальности законов логики (Лейбниц формулировал его как выполнимость логических законов "во всех мыслимых мирах").

Произвольная формальная теория $T$ есть теория множества $M(T)$ всех своих моделей, а значит, теория $T$ семантически непротиворечива, если и только если $\mathbf{M}(T)\ne \varnothing$ , т.е. для теории $T$ существует модель. Если отождествить пригодность математической теории, ее целесообразность с ее семантической непротиворечивостью, то можно сказать, что сформулированный критерий пригодности теории известен уже давно. Отыскание модели для теории до возникновения оснований математики было единственным общепризнанным методом доказательства "законности" теории. Математическая логика выработала аналог этого критерия, не опирающийся на наличие модели теории — внешний фактор по отношению к теории, а опирающийся на внутренние свойства самой теории, — понятие синтаксической непротиворечивости теории.

Определение 29.5. Формальная теория $T$ называется синтаксически (или дедуктивно, или формально) непротиворечивой, если не существует такой формулы $F$ , что $F$ и $\lnot F$ являются теоремами теории $T$ , т.е. в $T$ невыводимыми являются одновременно формула и ее отрицание. Аналогичное определение можно сформулировать и для произвольного множества $\Phi$ формул: $\Phi$ называется синтаксически непротиворечивым, если из $\Phi$ невыводимы одновременно формула и ее отрицание.

В теореме 16.9 доказана синтаксическая непротиворечивость формализованного исчисления высказываний. Аналогично доказывается следующая теорема.

Теорема 29.6. Формализованное исчисление предикатов синтаксически непротиворечиво.

Доказательство. Допустим противное, т.е. предположим, что ФИП синтаксически противоречиво. Значит, найдется такая формула $F$ , что $F$ и $\lnot F$ будут теоремами ФИП. Тогда по следствию 29.3 из теоремы 29.1 формулы Fa -,Fбудут общезначимыми, что невозможно на основании определения общезначимости.

Теперь перейдем к установлению взаимосвязей между понятиями семантической и синтаксической непротиворечивости. Наша задача состоит в том, чтобы доказать их эквивалентность. Начнем с достаточно простой, но важной леммы.

Лемма 29.7. Если множество формул имеет модель, то это множество семантически непротиворечиво.

Доказательство. Если множество $\Phi$ формул имеет модель $\mathbf{M}$ , то ни одна формула, выводимая из $\Phi$ , не является противоречивой, т.е. ложной во всякой интерпретации, ибо в противном случае она была бы ложна и в $\mathbf{M}$ (что невозможно в силу теоремы 29.1). Это и означает, что $\Phi$ семантически непротиворечиво.

Теорема 29.8. Если множество формул семантически непротиворечиво, то оно синтаксически непротиворечиво.

Доказательство. Допустим, что некоторое множество $\Phi$ формул узкого исчисления предикатов семантически непротиворечиво, но противоречиво синтаксически. Следовательно, из него выводима некоторая формула $F$ и ее отрицание $\lnot F$ . Но тогда из $\Phi$ выводима и их конъюнкция (по правилу введения конъюнкции) $F\land\lnot F$ . Но эта формула ложна в любой интерпретации, что означает, что множество $\Phi$ семантически противоречиво. Получаем противоречие, доказывающее, что $\Phi$ синтаксически непротиворечиво.

Непосредственно из предыдущих леммы и теоремы вытекает такое следствие.

Следствие 29.9. Если множество формул имеет модель, то оно синтаксически непротиворечиво.

Теорема Гёделя о существовании модели

Утверждение, обратное следствию, также оказывается справедливым. Но с конструктивной точки зрения оно оказывается более глубоким. Смысл его состоит в том, что всякое множество формул не только имеет модель, но эту модель можно конструктивно построить. Доказательство этого факта как раз и заключается в изложении метода такого построения. Это еще одна из замечательных теорем Гёделя (теорема о существовании модели), относящаяся к важнейшим теоремам математической логики. Она доказана Гёделем в 1930 г.

Теорема 29.10 (теорема Гёделя о существовании модели). Любое синтаксически непротиворечивое множество $\Sigma$ замкнутых формул узкого исчисления предикатов сигнатуры $\sigma$ имеет модель.

Доказательство

Пусть сигнатура $\sigma= \bigl\{a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots\bigr\}$ . Требуется построить модель $\mathbf{M}= <M;\, a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots>$ , такую, что $\mathbf{M}\vDash\Sigma$ (т.е. в алгебраической системе $\mathbf{M}$ выполняются все формулы из $\Sigma$ ). Эта модель будет строиться из слов некоторого алфавита. Под непротиворечивостью всюду в этом доказательстве будем понимать синтаксическую непротиворечивость.

Прежде всего расширим данную сигнатуру $\sigma$ до $\sigma'$ введением новых индивидных констант: $\sigma'= \sigma\cup\{c_0,c_1,\ldots,c_n,\ldots\}$ , где все $c_i$ отличны от всех символов из $\sigma$ . Далее будем работать с формулами расширенной сигнатуры $\sigma'$ . Поскольку все такие (замкнутые) формулы являются конечными словами некоторого счетного алфавита, то множество всех таких формул имеет счетную мощность и мы можем все их расположить в последовательность (т.е. занумеровать натуральными числами). Итак, пусть $A_0,A_1,\ldots,A_n,\ldots$ — множество всех предложений (замкнутых формул) сигнатуры $\sigma'$ .

Построим далее последовательность (цепочку)

$\Sigma_0\subseteq \Sigma_1\subseteq \ldots\subseteq \Sigma_n\subseteq\ldots$

(1)

множеств замкнутых формул следующим образом:

а) $\Sigma_0=\Sigma$ ;

б) если $\Sigma_n\cup\{A_n\}$ противоречиво, то $\Sigma_{n+1}= \Sigma_n\cup \{\lnot A_n\}$ ;

в) если $\Sigma_n\cup\{A_n\}$ непротиворечиво и $A_n$ не начинается с квантора существования, то $\Sigma_{n+1}= \Sigma_n\cup\{A_n\}$ ;

г) если $\Sigma_n\cup\{A_n\}$ непротиворечиво и $A_n\equiv (\exists x)(B(x))$ , то $\Sigma_{n+1}= \Sigma_n\cup\{A_n, B(c_k)\}$ , где $c_k\in \sigma'\setminus \sigma$ — новая константа с наименьшим номером $k$ , не встречающаяся в формуле $A_n$ и во всех формулах множества $\Sigma_n$ .

1) Докажем сначала, что каждое множество $\Sigma_n$ построенной последовательности будет непротиворечивым множеством формул исчисления предикатов сигнатуры $\sigma'$ . Доказательство будем вести индукцией по $n$ .

с) База индукции: $n=0$ . Так как $\Sigma_0=\Sigma$ , то по условию $\Sigma_0$ непротиворечиво в исчислении предикатов сигнатуры $\sigma$ . Докажем, что оно непротиворечиво и в исчислении сигнатуры $\sigma'$ . Допустим противное, т.е. $\Sigma_0\vdash F$ и $\Sigma_0\vdash\lnot F$ , где $F$ — формула сигнатуры $\sigma'$ . Следовательно, $\Sigma\vdash F$ и $\Sigma\vdash\lnot F$ . Это означает, что в $\Sigma$ имеется такое конечное подмножество формул $G_1,G_2,\ldots,G_m$ , что $G_1,G_2,\ldots,G_m\vdash F,\lnot F$ . Пусть $B_1,B_2,\ldots,B_s\equiv F$ — вывод формулы $F$ из гипотез $G_1,G_2,\ldots,G_m$ в исчислении предикатов сигнатуры $\sigma'$ . Допустим, что $c_{i_1},c_{i_2},\ldots,c_{i_p}$ — все те новые константы, которые входят в формулы этого вывода.

Поскольку $\forall$ - и $\exists$ -правила вывода к константам не применяются, то, заменив все новые константы $c_{i_1},c_{i_2},\ldots,c_{i_p}$ предметными переменными, не входящими в формулы $B_1,B_2,\ldots,B_s$ , получим новую последовательность формул $\widetilde{B}_1, \widetilde{B}_2,\ldots, \widetilde{B}_s$ исчисления предикатов уже сигнатуры $\sigma$ , представляющую собой вывод в этом исчислении ее последней формулы $\widetilde{B}_s\equiv \widetilde{F}$ . Аналогично доказывается, что в исчислении сигнатуры $\sigma$ из множества $\Sigma$ выводима формула $\lnot \widetilde{F}$ . Получается противоречие с условием, согласно которому $\Sigma$ — непротиворечиво в исчислении сигнатуры $\sigma$ .

Таким образом, $\Sigma_0$ непротиворечиво в исчислении сигнатуры $\sigma$ .

Шаг индукции. Предположим, что $\Sigma_n$ непротиворечиво в исчислении предикатов сигнатуры $\sigma'$ . Покажем, что тогда таким же свойством обладает и множество $\Sigma_{n+1}$ . Согласно определению для него возможны следующие случаи:

б) $\Sigma_{n}\cup\{A_n\}$ противоречиво. В этом случае $\Sigma_{n+1}= \Sigma_{n}\cup\{\lnot A_n\}$ . Допустим, что последнее множество противоречиво. Тогда $\Sigma_{n},\lnot A_n\vdash F$ и $\Sigma_{n},\lnot A_n\vdash\lnot F$ для некоторой формулы $F$ . Тогда для некоторого конечного подмножества $\Gamma\subset \Sigma_{n}\colon \Gamma,\lnot A_n\vdash F$ и $\Gamma,\lnot A_n\vdash\lnot F$ . Отсюда по производному правилу вывода $\lnot$ –вв получим $\Gamma\vdash\lnot\lnot A_n$ , то есть $\Gamma\vdash A_n$ , а значит, $\Sigma_n\vdash A_n$ .

В то же время из условия противоречивости множества $\Sigma_n\cup\{A_n\}$ аналогичные рассуждения приведут к заключению: $\Sigma_n\vdash\lnot A_n$ .

Эти два заключения говорят о противоречивости множества $\Sigma_n$ , что противоречит предположению индукции;

в) $\Sigma_n\cup\{A_n\}$ непротиворечиво и $A_n$ не начинаются с квантора существования. В этом случае по определению $\Sigma_{n+1}= \Sigma_n\cup \{A_n\}$ , а значит, $\Sigma_{n+1}$ — непротиворечиво;

г) $\Sigma_n\cup\{A_n\}$ непротиворечиво и $A_n$ начинается с квантора существования: $A_n\equiv (\exists x)(B(x))$ . В этом случае $\Sigma_{n+1}$ получается добавлением к $\Sigma_n$ двух формул $A_n$ и $B(c_k)$ , где $B(c_k)$ получена из $B(x)$ подстановкой константы $c_k$ (первой из $c_0,c_1,\ldots$ , не входящей в $A_n$ и все формулы из $\Sigma_{n}$ ) вместо предметной переменной $x\colon\, \Sigma_{n+1}= \Sigma_{n}\cup\{A_n,B(c_k)\}$ . Допустим, что $\Sigma_{n+1}$ противоречиво, т.е. $\Sigma_{n+1}\vdash F,\lnot F$ . Тогда найдется такое конечное подмножество $\Gamma\subset\Sigma_{n}$ , что $\Gamma, (\exists x)(B(x)),\, B(c_k)\vdash F$ и $\Gamma,(\exists x)(B(x)),\,B(c_k)\vdash\lnot F$ .

Поскольку в выводах этих формул $\forall$ -правило и $\exists$ -правило вывода не применяются к константе $c_k$ , то, заменив в них эту константу новой переменной $y$ , не участвующей в выводах этих формул, получим выводы, доказывающие, что $\Gamma,\,(\exists x)(B(x)),\, B(y_k)\vdash \widetilde{F}$ и $\Gamma,\, (\exists x)(B(x)),\, B(y_k)\vdash\lnot \widetilde{F}$ , где $\widetilde{F}$ , получена из $F$ заменой константы $c_k$ на предметную переменную $y$ ( $y$ — фиксированная переменная в этих выводах). Из двух последних выводимостей по производному правилу вывода (введения отрицания $\lnot$ -вв) получаем: $\Gamma,\,(\exists x)(B(x))\vdash\lnot B(y)$ . Отсюда по правилу введения квантора общности получаем

$\Gamma,~ (\exists x) \bigl(B(x)\bigr)\vdash (\forall y)\bigl(\lnot B(y)\bigr).$

(2)

Кроме того, легко получается выводимость $(\forall y)(\lnot B(y))\vdash\lnot (\exists y)(B(y))$ . Наконец, в силу выбора переменной $y$ , которая свободна для $x$ в формуле $B(x)$ , и на основании правила переименования связанных переменных из последней выводимости заключаем, что

$(\forall y)\bigl(\lnot B(y)\bigr)\vdash\lnot (\exists x)\bigl(B(x)\bigr).$

(3)

Из выводимостей (2) и (3), в силу транзитивности отношения выводимости (см. теорему 15.3, в), получаем:

$\Gamma,~ (\exists x)\bigl(B(x)\bigr)\vdash\lnot (\exists x) \bigl(B(x)\bigr).$

Учитывая, что $(\exists x)(B(x))\equiv A_n$ , можно заключить, что множество $\Gamma\cup\{A_n\}$ противоречиво. Поскольку $\Gamma\subset\Sigma_n$ , то $\Gamma\cup\{A_n\}\subset \Sigma_n\subset \{A_n\}$ , а значит, множество $\Sigma_n\cup\{A_n\}$ также противоречиво, что противоречит исходному условию.

Следовательно, и в этом случае множество $\Sigma_{n+1}$ непротиворечиво.

2) Рассмотрим теперь множество $\Sigma^{\ast}=\cup\Sigma_{n}$ (объединение берется по $n$ от 0 до $\infty$ ). Отметим два свойства этого множества формул. Во-первых, множество $\Sigma^{\ast}$ непротиворечиво. В самом деле, если бы из $\Sigma^{\ast}$ выводились формулы $F$ и $\lnot F$ , то они выводились бы из конечного подмножества множества $\Sigma^{\ast}$ , которое включалось бы в некоторое $\Sigma_{n}$ которое, следовательно, было бы противоречивым. Но это не так в силу предыдущего п. 1 доказательства. Во-вторых, для любой формулы $A$ исчисления предикатов сигнатуры $\sigma'~A\in \Sigma^{\ast}$ или $\lnot A\in \Sigma^{\ast}$ (свойство полноты множества $\Sigma^{\ast}$ ). Это вытекает непосредственно из построения $\Sigma^{\ast}$ , так как $A=A_n$ для некоторого натурального $n$ .

Последнее свойство можно сформулировать несколько в ином виде. Сначала отметим, что $A\in \Sigma^{\ast}\Leftrightarrow \Sigma^{\ast}\vdash A$ . В самом деле, импликация слева направо очевидна. Предположив, что $\Sigma^{\ast}\vdash A$ и $A\notin \Sigma^{\ast}$ , в силу отмеченного свойства получим $\lnot A\in\Sigma^{\ast}$ . В итоге получаем, что $\Sigma^{\ast}$ противоречиво, что противоречит первому отмеченному выше свойству.

Следовательно, второе отмечаемое утверждение принимает вид: $\Sigma^{\ast}\vdash A$ или $\Sigma^{\ast}\vdash\lnot A$ для любой формулы $A$ .

3) Построим теперь саму модель $\mathbf{M}$ . Напомним, что ее сигнатура $\sigma= \bigl\{a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots\bigr\}$ . Рассмотрим всевозможные термы расширенной сигнатуры $\sigma'$ , не содержащие предметных переменных, а содержащие лишь предметные константы $a_0,a_1,\ldots,\, c_0,c_1,\ldots$ . Напомним, что термы представляют собой либо сами эти константы, либо выражения вида $f_i(t_1,\ldots,t_{n_i})$ , где $f_i$ — функциональный символ из $\sigma$ , a $t_1,\ldots,t_{n_i}$ — термы. Множество всех этих термов и есть базисное множество $M$ модели $\mathbf{M}$ . Сигнатурные операции на этом множестве зададим следующим образом:

$a_{i}^{M}= a_i,~ f_{i}^{M}(t_1,\ldots,t_{n_i})= f_i(t_1,\ldots,t_{n_i}),\quad i=0,1,2, \ldots$

Наконец, выполнимость на $\mathbf{M}$ соответствующего сигнатурного отношения определим следующим образом:

$\mathbf{M}\vDash P_{j}^{M}(t_1,\ldots,t_{n_i})~ \Leftrightarrow~ \Sigma^{\ast}\vdash P_{j}(t_1,\ldots,t_{n_i}).$

(4)

4) Проверим, что алгебраическая система $\mathbf{M}$ сигнатуры о действительно является моделью исходного множества $\Sigma$ формул исчисления предикатов сигнатуры $\sigma$ , то есть $\mathbf{M}\vDash\Sigma$ . Для этого докажем сначала, что для всякой формулы $F(x_1,\ldots,x_n)$ сигнатуры $\sigma'$ и любых термов $t_1,\ldots,t_n\in M$ имеет место-следующее утверждение:

$\mathbf{M}\vDash F(t_1,\ldots,t_n)~ \Leftrightarrow~ \Sigma^{\ast}\vdash F(t_1,\ldots,t_n).$

(5)

Доказательство будем вести индукцией по числу $k$ логических знаков, используемых при построении формулы $F$ .

База индукции: $k=0$ . Тогда $F$ — атомарная формула, имеющая вид $P_j(t_1,\ldots,t_{m_j})$ , а для нее утверждение (5) верно по определению (4).

Шаг индукции. Предположим, что для всех формул, в записи которых число логических символов $\leqslant k$ , утверждение (5) верно. Пусть $F$ — произвольная формула, в записи которой участвует $k+1$ логический символ. Покажем, что тогда утверждение (5) будет справедливо и для нее. На основании определения (формулы) формула F имеет один из следующих видов: $\lnot A,\,A\to B,\, (\forall x)(B(x)),\, (\exists x)(B(x))$ . Рассмотрим последовательно каждый из этих случаев.

а) $F\equiv\lnot A$ . Предположим, что $\mathbf{M}\vDash\lnot A(t_1,\ldots, t_n)$ . Тогда по определению отрицания это означает, что $A(t_1,\ldots, t_n)$ не выполняется на $\mathbf{M}\colon\, \mathbf{M}\nvDash A(t_1,\ldots, t_n)$ . Отсюда по предположению индукции заключаем, что $\Sigma^{\ast}\nvdash A(t_1,\ldots, t_n)$ . Следовательно, по свойству полноты множества $\Sigma^{\ast}$ , отмеченному в п. 2 настоящего доказательства, $\Sigma^{\ast}\vdash\lnot A(t_1,\ldots, t_n)$ . Легко видеть, что каждое утверждение настоящего рассуждения допускает обращение, так что

$\mathbf{M}\vDash\lnot A(t_1,\ldots, t_n)~ \Leftrightarrow~ \Sigma^{\ast}\vdash\lnot A(t_1,\ldots, t_n).$

б) $F\equiv A\to B$ . Предположим, что $\mathbf{M}\vDash A(t_1,\ldots, t_n)\to B(t_1,\ldots, t_n)$ . Используя определения импликации, конъюнкции и отрицания, определение (4), полноту $\Sigma^{\ast}$ и предположение индукции для формул $A$ и $B$ , проводим следующее рассуждение:

$\mathbf{M}\vDash A\to B \Leftrightarrow \mathbf{M}\vDash\lnot(A\land\lnot B) \Leftrightarrow \mathbf{M}\nvDash A\land\lnot B \Leftrightarrow \mathbf{M}\nvDash A$ , или $\mathbf{M}\nvDash\lnot B \Leftrightarrow \mathbf{M}\nvDash A$ ,

или $\mathbf{M}\vDash B \Leftrightarrow \Sigma^{\ast}\nvdash A$ , или $\Sigma^{\ast}\vdash B \Leftrightarrow \Sigma^{\ast}\vdash\lnot A$ , или $\Sigma^{\ast}\vdash B$ .

Теперь мы находимся в области формализованного исчисления высказываний. Дальнейшие рассуждения таковы. Из каждого из утверждений $\Sigma^{\ast}\vdash\lnot A$ и $\Sigma^{\ast}\vdash B$ по правилу $\lor$ -вв следует $\Sigma^{\ast} \vdash\lnot A\lor B$ , то есть $\Sigma^{\ast}\vdash A\to B$ . Теперь нужно проделать обратное рассуждение. Предположим, что $\Sigma^{\ast}\vdash A\to B$ и $\Sigma^{\ast}\vdash\lnot A$ . Следовательно, по второму свойству множества $\Sigma^{\ast}$ из п. 2 настоящего доказательства $\Sigma^{\ast}\vdash A$ . Тогда из выводимостей $\Sigma^{\ast}\vdash A\to B$ и $\Sigma^{\ast}\vdash A$ и правила MP $(A\to B,~ A\vdash B)$ следует, что $\Sigma^{\ast}\vdash B$ .

Итак, мы доказали, что $\mathbf{M}\vDash A\to B \Leftrightarrow \Sigma^{\ast}\vdash A\to B$ .

в) $F\equiv (\forall x)(B(x,t_1,\ldots,t_n))$ . Предположим, что $\mathbf{M}= (\forall x)(B(x,t_1,\ldots,t_n))$ . По определению квантора общности это означает, что $\mathbf{M}\vDash B(t,t_1,\ldots,t_n)$ для каждого элемента $t\in M$ . Таким образом, по предположению индукции (5) получим, что $\Sigma^{\ast}\vdash B(t,t_1,\ldots,t_n)$ . Отсюда, в силу правила введения квантора общности, заключаем, что $\Sigma^{\ast}\vdash (\forall x)(B(x,t_1,\ldots,t_n))$ .

Обратно, пусть $\Sigma^{\ast}\vdash (\forall x)(B(x,t_1,\ldots,t_n))$ . Вместе с аксиомой $\mathsf{PA1}\colon (\forall x)(B(x,t_1,\ldots,t_n))\to B(t,t_1,\ldots,t_n)$ , в силу правила MP, это дает: $\Sigma^{\ast}\vdash B(t,t_1,\ldots,t_n)$ . На основании предположения индукции (5) отсюда следует, что $\mathbf{M}\vDash B(t,t_1,\ldots,t_n)$ . Поскольку данная выполнимость на модели $\mathbf{M}$ имеет место для любого элемента $t\in M$ , поэтому на основании определения квантора общности отсюда следует, что $\mathbf{M}\vDash (\forall x)(B(x,t_1,\ldots,t_n))$ .

г) $F\equiv (\exists x)(B(x,t_1,\ldots,t_n))$ . Предположим, что $\mathbf{M}\vDash (\exists x)(B(x,t_1,\ldots,t_n))$ . Тогда по определению квантора существования $\mathbf{M}\vDash B(a_0,t_1,\ldots,t_n)$ для некоторого элемента $a_0\in M$ . В силу предположения индукции (5) отсюда получаем $\Sigma^{\ast}\vdash B(a_0,t_1,\ldots, t_n)$ . Вместе с аксиомой $\mathsf{PA2}\colon B(a_0,t_1,\ldots,t_n)\to (\exists x)(B(x,t_1, \ldots,t_n))$ , в силу правила MP, это дает: $\Sigma^{\ast}\vdash (\exists x)(B(x,t_1,\ldots,t_n))$ .

Обратно, пусть $\Sigma^{\ast}\vdash (\exists x)(B(x,t_1,\ldots,t_n))$ . Поскольку $(\exists x)(B(x,t_1,\ldots,t_n))$ — замкнутая формула сигнатуры $\sigma'$ , то она содержится в последовательности $A_1,A_2,\ldots,A_n,\ldots$ всех таких формул. Предположим, что это формула $A_m$ . Тогда множество $\Sigma_m\cup \{A_m\}$ непротиворечиво. (Если бы оно было противоречиво, то $\Sigma_{m+1}$ равнялось бы $\Sigma_m\cup \{\lnot A_m\}$ , т.е. формула $\lnot A_m$ входила бы в множество $\Sigma^{\ast}$ и последнее было бы противоречивым, что не так в силу п. 2 настоящего доказательства.) Поскольку, кроме того, $A_m$ начинается с квантора существования, то в этом случае $\Sigma_{m+1}= \Sigma_{m}\cup \bigl\{A_m,\, B(c_k,t_1,\ldots,t_n)\bigr\}$ и, значит, $B(c_k,t_1,\ldots,t_n)\in \Sigma^{\ast}$ . Следовательно, для формулы $B(c_k,t_1,\ldots,t_n)$ по предположению индукции имеем $\mathbf{M}\vDash B(c_k,t_1,\ldots,t_n)$ для некоторой константы $c_k\in M$ . Тогда по определению квантора существования $\mathbf{M}\vDash (\exists x)(B(x,t_1,\ldots,t_n))$ .

Итак, мы доказали, что всякая формула, выводимая из $\Sigma^{\ast}$ (и, в частности, принадлежащая $\Sigma^{\ast}$ ), истинна (выполнима) на модели $\mathbf{M}$ . В частности, на $\mathbf{M}$ выполняются и все формулы исходной совокупности $\Sigma= \Sigma_0\subset \Sigma^{\ast}$ , то есть $\mathbf{M}$ — действительно модель непротиворечивого множества формул £. Теорема полностью доказана.

Теоремы о непротиворечивости формул предикатов

Теорема Гёделя о существовании модели позволяет доказать теорему, обратную к теореме 29.8, и они вместе образуют следующую важную метатеорему.

Теорема 29.11 (о непротиворечивости). Множество формул узкого исчисления предикатов семантически непротиворечиво тогда и только тогда, когда оно синтаксически непротиворечиво.

Доказательство. Необходимость есть теорема 29.8. Обратно, если множество формул синтаксически непротиворечиво, то по теореме 29.10 оно имеет модель, а тогда по лемме 29.7 оно семантически непротиворечиво.

Наконец, объединим в одну метатеорему следствие из теоремы 29.8 и теорему 29.10. Получим следующее.

Теорема 29.12 (о непротиворечивости). Множество формул узкого исчисления предикатов синтаксически (дедуктивно) непротиворечиво тогда и только тогда, когда оно имеет модель.

Приведем интересный комментарий, который дает теореме о непротиворечивости известный логик Р. Линдон, по мнению которого доказательства (дедуктивной) непротиворечивости какой-либо теории посредством указания ее модели широко распространены в абстрактной математике. Менее очевидное из утверждений теоремы о непротиворечивости — о существовании модели у каждой дедуктивно непротиворечивой теории — используется далеко не так часто. Возможно, это объясняется тем, что математики не слишком-то большое значение придают понятию существования; теорему о непротиворечивости можно как раз и рассматривать как скромное, но зато точное выражение довольно-таки расплывчатого мнения, что существование в математике — это не что иное, как непротиворечивость.

Возможности применения теоремы о непротиворечивости к проблемам установления непротиворечивости конкретных теорий весьма ограниченны: дело в том, что построение модели обычно требует принятия в метаязыке допущений, значительно более сильных, нежели те, которые выражаются предметной теорией. Другой путь установления непротиворечивости какой-нибудь аксиоматической теории состоит в том, чтобы с помощью чисто синтаксических рассмотрений показать, что в данной теории нельзя доказать тождественно ложную формулу. Область применения этого метода, однако, также невелика. Теорема Гёделя не позволяет надеяться на получение доказательства непротиворечивости теории, если не допускать в теории, предназначенной для такого доказательства на метаязыке, по меньшей мере столь же сильных средств, что и в рассматриваемой предметной теории. Убеждение в непротиворечивости достаточно сложных математических теорий базируется в конечном счете на интуиции и опыте.

Полнота и адекватность формализованного исчисления предикатов

Доказав теорему Гёделя о существовании модели (теорема 29.10), можно доказать теорему, обратную теореме оправданности (следствие 29.2 из теоремы 29.1), т.е. утверждение о том, что из семантической выводимости следует синтаксическая выводимость. В самом деле, пусть $\Phi\vDash F$ . Покажем, что тогда множество формул $\Phi\cup\{\lnot F\}$ противоречиво. Допустим на время, что это не так. Тогда по теореме 29.10 это множество имеет модель $\mathbf{M}$ , т.е. на $\mathbf{M}$ выполняется формула $\lnot F$ и все формулы из $\Phi$ . Из последнего, ввиду условия $\Phi\vDash F$ , следует, что на $\mathbf{M}$ выполняется и формула $F$ . Получаем противоречие. Итак, множество $\Phi\cup\{\lnot F\}$ противоречиво. Значит, из него выводима любая формула, в частности $\Phi\cup\{\lnot F\}\vdash F$ . Тогда по теореме о дедукции имеем $\Phi\vdash\lnot F\to F$ . Учитывая, что, кроме того, формула $(\lnot F\to F)\to F$ является теоремой ФИВ, по правилу MP заключаем, что $\Phi\vdash F$ .

Итак, мы доказали, что если $\Phi\vDash F$ , то $\Phi\vdash F$ . Объединив это утверждение со следствием 29.1 из теоремы 29.2, приходим к следующей важной метатеореме.

Теорема 29.13 (теорема адекватности). Формула $F$ синтаксически выводима из множества формул $\Phi$ тогда и только тогда, когда она семантически выводима из $\Phi\colon\, \Phi\vdash F \Leftrightarrow \Phi\vDash F$ .

Если теорема оправданности означала, что при выборе аксиом и правил вывода мы не были слишком щедры (настолько, что сможем доказать лишь общезначимые формулы), то обратная теорема — теорема адекватности — означает, что при этом выборе мы не были и излишне скупы (ровно настолько, что сможем доказать всякую общезначимую формулу).

Заметим, что нетрудно показать, что теорема о существовании модели вытекает из теоремы адекватности. В самом деле, предположим, что $\Phi$ — непротиворечивое множество формул, не имеющее модели. Тогда ясно, что для любой формулы $F$ справедливо семантическое следование $\Phi\vDash F$ . В силу теоремы адекватности отсюда следует, что $\Phi\vdash F$ для любой $F$ , что означает противоречивость множества $\Phi$ , в противоречие с условием.

Теорема 29.14 (теорема Гёделя о полноте ФИП). Класс доказуемых замкнутых формул совпадает с классом общезначимых (или тождественно истинных) формул: $\vdash F \Leftrightarrow\vDash F$ .

Доказательство. Эта теорема непосредственно вытекает из предыдущей при $\Phi= \varnothing$ .

Справедлива она и для открытых формул. В самом деле, если $\vDash F(x_1,\ldots,x_n)$ , где $x_1,\ldots,x_n$ — свободные предметные переменные в формуле $F$ , то в силу определения квантора общности это будет равносильно тому, что $\vDash(\forall x_1)\ldots (\forall x_n) \bigl(F(x_1,\ldots,x_n)\bigr)$ . По теореме 29.14 это равносильно тому, что $\vdash(\forall x_1)\ldots (\forall x_n) \bigl(F(x_1,\ldots,x_n)\bigr)$ . В силу свойств выводимости последнее утверждение равносильно тому, что $\vdash F(x_1,\ldots,x_n)$ .

Неполнота формализованного исчисления предикатов в абсолютном и узком смыслах

В учебнике обсуждаются два понятия полноты аксиоматической теории: абсолютная полнота и полнота в узком смысле (см. определение 27.6). Доказанная теорема 29.14 может быть истолкована как некая внешняя полнота формализованного исчисления предикатов, его полнота относительно логики предикатов: в этой теории могут быть формально доказаны все общезначимые формулы логики предикатов. Рассмотрим вопросы внутренней полноты формализованного исчисления предикатов, т.е. выясним, будет ли эта теория абсолютно полной и полной в узком смысле (см. определения 27.5 и 27.6). Поскольку на основании теоремы 29.14 множество теорем формализованного исчисления предикатов совпадает с множеством тавтологий (общезначимых формул) логики предикатов, а в логике предикатов существуют выполнимые, но не общезначимые формулы, формализованное исчисление предикатов не является абсолютно полной теорией. Здесь ситуация аналогична соответствующей ситуации в формализованном исчислении высказываний. Что же касается полноты формализованного исчисления предикатов в узком смысле, то исчисление предикатов (в отличие от исчисления высказываний, см. теорему 28.4) таким свойством не обладает. Для доказательства приведем пример формулы, не являющейся теоремой формализованного исчисления предикатов, добавление которой к аксиомам исчисления предикатов (с сохранением правил вывода) приводит к непротиворечивой формальной аксиоматической теории.

Пример 29.15. Рассмотрим формулу $(\exists x)(F(x))\to (\forall x)(F(x))$ . Нетрудно убедиться в том, что она не является общезначимой (приведите пример конкретного одноместного предиката, превращающего эту формулу в ложное высказывание). Поэтому на основании теоремы К. Гёделя о полноте она не доказуема в формализованном исчислении предикатов. С другой стороны, добавив к аксиомам формализованного исчисления предикатов рассматриваемую формулу, получим непротиворечивую формальную теорию $T$ . Ее непротиворечивость можно доказать следующим образом.

Рассмотрим модель этой теории на одноэлементном множестве $M=\{a\}$ . Ясно, что данная формула тождественно истинна на $M$ . Далее, учитывая, что на $M$ можно определить для каждого натурального $n$ лишь два n-местных предиката $P_1^n$ и $P_2^n$ , причем $\lambda(P_1^n(a,\ldots,a))=0$ и $\lambda(P_2^n(a,\ldots,a))=1$ , нетрудно доказать, что все аксиомы новой теории $T$ тождественно истинны на этой модели и правила вывода от тождественно истинных на $M$ формул приводят к тождественно истинным на $M$ формулам. Таким образом, доказывается утверждение: всякая теорема теории $T$ тождественно истинна на одноэлементном множестве $M$ .

Следовательно, если бы для некоторой формулы $F$ обе формулы $F$ и $\lnot F$ были теоремами теории $T$ , то они были бы тождественно истинны на одноэлементном множестве $M$ , что невозможно. Поэтому расширенная теория $T$ непротиворечива, что и доказывает неполноту в узком смысле формализованного исчисления предикатов.

Теорема компактности

Мы уже отмечали (см. теорему 15.3, б) и неоднократно использовали тот простой факт, непосредственно вытекающий из определения понятия вывода, что $\Phi\vdash F$ тогда и только тогда, когда $\Phi_0\vdash F$ , где $\Phi_0$ — некоторое конечное подмножество множества $\Phi$ формул. Теорема адекватности, установленная на основании выдающейся теоремы Гёделя о существовании модели, позволяет получить из этого тривиального соображения аналогичную теорему семантического содержания, уже отнюдь не столь очевидную.

Теорема 29.16 (теорема К. Гёделя–А. И. Мальцева). Если $\Phi\vDash F$ , то для некоторого конечного подмножества $\Phi_0\subset\Phi$ имеет место $\Phi_0\vDash F$ .

Доказательство. Если $\Phi\vDash F$ , то по теореме 29.13 (теорема адекватности) $\Phi\vdash F$ . В силу сделанного перед настоящей теоремой замечания найдется такое конечное подмножество $\Phi_0\subset\Phi$ , что $\Phi_0\vdash F$ . Отсюда по теореме оправданности (следствие 29.2 из теоремы 29.1) заключаем, что $\Phi_0\vDash F$ .

Следствие 29.17(локальная теорема К. Гёделя—А. И. Мальцева). Множество $\Sigma$ замкнутых формул узкого исчисления предикатов сигнатуры $\sigma$ имеет модель тогда и только тогда, когда каждое его конечное подмножество имеет модель.

Доказательство. Необходимость очевидна. Обратно, пусть каждое конечное подмножество множества $\Sigma$ имеет модель. Тогда $\Sigma$ — синтаксически непротиворечиво. (Если бы это было не так, то для некоторой формулы $F$ имелись бы выводимости $\Sigma\vdash F$ и $\Sigma\vdash\lnot F$ , а значит, нашлось бы такое конечное подмножество $\Sigma_0\subset \Sigma$ , что $\Sigma_0\vdash F$ и $\Sigma_0\vdash\lnot F$ , то есть $\Sigma_0$ было бы синтаксически противоречиво, а значит, по теореме 29.12 не имело бы модели, что противоречило бы условию.) Следовательно, по теореме 29.10 о существовании модели множество $\Sigma$ имеет модель. Следствие доказано.

В заключение приведем еще одну теорему о формулах узкого исчисления предикатов и их моделях.

Теорема 29.18 (Лёвенгейм–Сколем). Пусть $\sigma$ — счетная сигнатура и $\Sigma$ — множество замкнутых формул узкого исчисления предикатов сигнатуры $\sigma$ . Если $\Sigma$ имеет модель, то $\Sigma$ имеет счетную модель.

Доказательство. Пусть $\sigma= \bigl\{a_0,a_1,\ldots;\, f_0,f_1,\ldots;\, P_0,P_1,\ldots \bigr\}$ и множество $\Sigma$ формул имеет модель. Тогда (по теореме 29.12) $\Sigma$ синтаксически непротиворечиво и модель этого множества формул может быть построена, как в доказательстве теоремы 29.10. Построенная таким образом модель будет счетной: она состоит из элементов $a_0,a_1,\ldots;\, c_0,c_1,\ldots$ и всех термов (не содержащих переменных), построенных из констант $a_i,\,c_j$ . Эти термы можно занумеровать, например, по следующему правилу:

$\nu(a_i)=4i+1,\quad \nu(c_i)=4i+3,\quad \nu\bigl(f_i(t_1,\ldots,t_{n_i})\bigr)= 2^{n_{n_i}+1}\cdot 3^{\nu(t_1)}\cdot 5^{\nu(t_2)}\cdot \ldots\cdot p_{n_i}^{\nu(t_{ni})},$

где $p_0=2,\,p_1=3,\,p_2=5,\,\ldots,\,p_{n_i},\,\ldots$ — последовательность простых чисел.

Эта теорема может быть доказана и в более общей мощностной формулировке: если множество $\Sigma$ формул имеет бесконечную модель и мощность множества всех букв, из которых составлены формулы из $\Sigma$ , равна $n$ , то для любой бесконечной мощности $m\geqslant n$ существует модель множества $\Sigma$ мощности $m$ .

Укажем два следствия этой теоремы:

1) если $\Sigma$ — множество формул мощности $n$ , имеющее бесконечную модель, то $\Sigma$ имеет бесконечные модели любых мощностей, превышающих $n$ ;

2) всякое конечное множество или счетное непротиворечивое множество формул либо имеет только конечные модели, либо имеет бесконечные модели любых мощностей.

Теорема Лёвенгейма–Сколема дает ряд поразительных следствий двух типов: одни из них гласят, что некоторая теория имеет неожиданно обширные модели, другие — что теория имеет неожиданно узкие модели. Дальнейшее развитие эта мысль получит в следующей лекции.

Математический форум (помощь с решением задач, обсуждение вопросов по математике).

Если заметили ошибку, опечатку или есть предложения, напишите в комментариях.

Список статей » Список форумов

Часовой пояс: UTC + 3 часа [ Летнее время ]