Математический форум Math Help Planet
Обсуждение и решение задач по математике, физике, химии, экономике Теоретический раздел |
Часовой пояс: UTC + 3 часа [ Летнее время ] |
новый онлайн-сервис число, сумма и дата прописью |
|
Часовой пояс: UTC + 3 часа [ Летнее время ] |
Формализованное исчисление высказываний | |
---|---|
Онлайн-сервисы
Нахождение НОД и НОК
Разложение числа на простые множители
Сравнения по модулю
Операции над множествами
Операции над векторами
Разложение вектора по базису. Доказательство, что векторы образуют базис
Чертёж треугольника по координатам вершин
Решение треугольника
Решение Пирамиды
Построение Пирамиды по координатам вершин
Чертёж многоугольника по координатам вершин
Решение систем методом Крамера и Матричным
Онлайн построение графика кривой 2-го порядка
Определение вида кривой или поверхности 2-го порядка по инвариантам
МНК и регрессионный анализ Онлайн + графики
Онлайн число, сумма и дата прописью
Алгоритмы JavaScript
Алгоритмы поиска
Алгоритмы сортировки
Уникальные элементы массива
Объединение, пересечение и разность массивов
НОД и НОК
Операции над матрицами
Дата прописью
Введение в анализ
Функции: понятие, определение, графики
Непрерывность функции
Исследование функции и построение графика
Теория множеств
Множества: понятие, определение, примеры
Точечные множества
Замкнутые и открытые множества
Мера множества
Группы, кольца, поля в математике
Поле комплексных чисел
Кольцо многочленов
Основная теорема алгебры и ее следствия
Математическая логика
Алгебра высказываний
Аксиоматика и логические рассуждения
Методы доказательств теорем
Алгебра высказываний и операции над ними
Формулы алгебры высказываний
Тавтологии алгебры высказываний
Логическая равносильность формул
Нормальные формы для формул высказываний
Логическое следование формул
Приложение алгебры высказываний для теорем
Дедуктивные и индуктивные умозаключения
Решение логических задач
Принцип полной дизъюнкции
Булевы функции
Множества, отношения и функции в логике
Булевы функции от одного и двух аргументов
Булевы функции от n аргументов
Системы булевых функций
Применение булевых функций к релейно-контактным схемам
Релейно-контактные схемы в ЭВМ
Практическое применение булевых функций
Теория формального
Формализованное исчисление высказываний
Полнота и другие свойства формализованного исчисления высказываний
Независимость системы аксиом формализованного исчисления высказываний
Логика предикатов
Логика предикатов
Логические операции над предикатами
Кванторные операции над предикатами
Формулы логики предикатов
Тавтологии логики предикатов
Преобразования формул и следование их предикатов
Проблемы разрешения для общезначимости и выполнимости формул
Применение логики предикатов в математике
Строение математических теорем
Аристотелева силлогистика и методы рассуждений
Принцип полной дизъюнкции в предикатной форме
Метод полной математической индукции
Необходимые и достаточные условия
Логика предикатов и алгебра множеств
Формализованное исчисление предикатов
Неформальные и формаль-ные аксиоматические теории
Неформальные аксиоматические теории
Свойства аксиоматических теорий
Формальные аксиоматические теории
Формализация теории аристотелевых силлогизмов
Свойства формализованного исчисления предикатов
Формальные теории первого порядка
Формализация математической теории
Теория алгоритмов
Интуитивное представление об алгоритмах
Машины Тьюринга и тезис
Рекурсивные функции
Нормальные алгоритмы Маркова
Разрешимость и перечислимость множеств
Неразрешимые алгоритмические проблемы
Теорема Гёделя о неполноте формальной арифметики
Математическая логика и компьютеры
Дискретная математика
Множества и отношения
Теория множеств: понятия и определения
Операции над множествами
Кортеж и декартово произведение множеств
Соответствия и бинарные отношения на множествах
Операции над соответствиями на множествах
Семейства множеств
Специальные свойства бинарных отношений
Отношения эквивалентности на множестве
Упорядоченные множества
Теорема о неподвижной точке
Мощность множества
Парадокс Рассела
Метод характеристических функций
Группы и кольца
Алгебраические структуры и операции
Группоиды, полугруппы, группы
Кольца, тела, поля
Области целостности в теории колец
Модули и линейные пространства
Подгруппы и подкольца
Теорема Лагранжа о порядке конечной группы
Гомоморфизмы групп и нормальные делители
Гомоморфизмы и изоморфизмы колец
Алгебра кватернионов
Полукольца и булевы алгебры
Полукольца: определение, аксиомы, примеры
Замкнутые полукольца
Полукольца и системы линейных уравнений
Булевы алгебры и полукольца
Решетки и полурешетки
Алгебраические системы
Алгебраические системы: модели и алгебры
Подсистемы алгебраических систем
Конгруэнции и фактор-системы
Гомоморфизмы алгебраических систем
Прямые произведения алгебраических систем
Конечные булевы алгебры
Многосортные алгебры
Теория графов
Теория графов: основные понятия и определения
Способы представления графов
Неориентированные и ориентированные деревья
Остовное дерево и алгоритм Краскала
Методы систематического обхода вершин графа
Алгоритмы поиска в глубину и ширину в графах
Задача о путях во взвешенных ориентированных графах
Изоморфизм, гомоморфизм и автоморфизм графов
Топологическая сортировка вершин графа
Элементы цикломатики в теории графов
Булева алгебра и функции
Булевы функции и булев куб
Таблицы булевых функций и булев оператор
Равенство булевых функций. Фиктивные переменные
Формулы и суперпозиции булевых функций
Дизъюнктивные и конъюнктивные нормальные формы
Построение минимальных ДНФ
Теорема Поста и классы
Критерий Поста
Схемы из функциональных элементов
Конечные автоматы и регулярные языки
Конечные автоматы и регулярные языки
Алфавит, слово, язык в программировании
Порождающие грамматики (грамматики Хомского)
Классификация грамматик и языков
Регулярные языки и регулярные выражения
Конечные автоматы
Допустимость языка конечным автоматом
Теорема Клини
Детерминизация конечных автоматов
Минимизация конечных автоматов
Лемма о разрастании для регулярных языков
Обоснование алгоритма детерминизации автоматов
Конечные автоматы с выходом
Морфизмы и конечные подстановки
Машины Тьюринга
Контекстно-свободные языки
Контекстно-свободные языки и грамматики
Приведенная форма КС-грамматики
Лемма о разрастании для КС-языков
Магазинные автоматы (автомат с магазинной памятью)
Алгоритм построения МП-автомата по КС-грамматике
Алгоритм построения КС-грамматики по МП-автомату
Алгебраические свойства КС-языков
Основное свойство суперпозиции КС-языков
Пересечение контекстно-свободных языков
Методы синтаксического анализа КС-языков
Восходящий синтаксический анализ и LR(k)-грамматики
Семантика формальных языков
Принцип индукции по неподвижной точке
Графовое представление МП-автоматов
Интегральное исчисление
Неопределённый и определённый
Неопределенный и определенный интегралы
Свойства интегралов
Интегрирование по частям
Интегрирование методом замены переменной
Интегрирование различных рациональных функций
Интегрирование различных иррациональных функций
Интегрирование различных тригонометрических функций
Определенный интеграл и его основные свойства
Необходимое и достаточное условие интегрируемости
Теоремы существования первообразной
Свойства определенных интегралов
Несобственные интегралы
Интегральное определение логарифмической функции
Приложения интегралов
Вычисление площадей плоских фигур
Площади фигур в различных координатах
Вычисление объемов тел с помощью интегралов
Объём тела вращения
Вычисление длин дуг кривых
Формулы длины дуги регулярной кривой
Кривизна плоской кривой
Площадь поверхности вращения тела
Интегралы в физике
Статические моменты и координаты центра тяжести
Теоремы Гульдина–Паппа
Вычисление моментов инерции
Другие приложения интегралов в физике
Основные интегралы
Вариационное исчисление
Примеры вариационных задач
Дифференциальное уравнение Эйлера
Функционалы, зависящие от нескольких функций
Задача о минимуме кратного интеграла
Финансовый анализ
Анализ эффективности
Критерии и показатели эффективности предприятия
Методы анализа эффективности деятельности
Факторный анализ прибыли от операционной деятельности
Анализ безубыточности предприятия
Операционный рычаг и эффект финансового рычага
Анализ и оценка состава, структуры и динамики доходов и расходов
Анализ рентабельности и резервов устойчивого роста капитала
Анализ распределения прибыли предприятия
Анализ и оценка чувствительности показателей эффективности
Анализ устойчивости
Финансовая устойчивость и долгосрочная платежеспособность
Характеристика типов финансовой устойчивости
Рыночная активность
Финансовый анализ рыночной активности
Методика анализа рыночной активности
Анализ и оценка дивидендного дохода на одну акцию
Инвестиционная деятельность
Инвестиции: экономическая сущность и классификация
Государственное регулирование инвестиционной деятельности
Источники финансовых ресурсов на капитальные вложения
Инвестиции в основные фонды
Оценка состояния основных фондов
Амортизация основных фондов
Капитальное строительство в инвестиционном процессе
Планирование инвестиций в форме капитальных вложений
Экономическая эффективность инвестиций
Финансирование капитальных вложений
Кредитование капитальных вложений
Кредитоспособность
Финансирование и кредитование затрат
Финансирование и кредитование инвестиционной деятельности потребительской кооперации
Финансирование и кредитование капитальных вложений потребительской кооперации
Инвестиционное строительное проектирование
Анализ инвестиций
Инвестиции и инвестиционная деятельность предприятия
Задачи финансового анализа инвестиций предприятия
Учет фактора времени в инвестиционной деятельности
Аннуитет и финансовая рента в инвестициях
Учет фактора инфляции при инвестировании
Оценка фактора риска инвестиционного проекта
Методы оценки эффективности инвестиций
Показатели эффективности инвестиционного проекта
Стоимость компании
Концепция построения международных стандартов финансовой отчетности (МСФО)
Экономическое содержание международных стандартов финансовой отчётности
Цели и принципы оценки стоимости акций и активов компании
Оценка акций и активов предприятия по справедливой стоимости
Методы оценки справедливой стоимости акций предприятия
Затратный подход к оценки стоимости компаний и акций
Сравнительный подход к оценки стоимости предприятий и акций
Доходный подход к оценке стоимости компании и акций
Выбор ставки дисконтирования при инвестировании в акции
Метод капитализации прибыли
Сравнение подходов к оценке стоимости компаний и пакетов акций
Форвардные контракты
Форвардный контракт и цена
Форвардная цена акции на бирже
Цена форвардного контракта инвестора
Форвардная цена акции с учетом величины дивиденда
Форвардная цена акции с учетом ставки дивиденда
Форвардная цена валюты на рынке форекс
Форвардный валютный курс и инфляция на рынке
Форвардная цена товара и спотовый рынок
Форвардная цена при различии ставок по кредитам и депозитам
Синтетический форвардный контракт на акции и валюту
Теория вероятностей
Основные понятия теории вероятностей
Зависимые и независимые случайные события
Повторные независимые испытания
Формула Бернулли
Одномерные случайные величины
Многомерные случайные величины
Функции случайных величин
Законы распределения целочисленных случайных величин
Законы распределения непрерывных случайных величин
Предельные теоремы теории вероятностей
Закон больших чисел и предельные теоремы
Вероятностные закономерности
Математическая статистика
Элементы математической статистики
Выборочный метод
Оценки параметров генеральной совокупности
Статистические гипотезы
Критерии согласия
Теоретические и эмпирические частоты
Теория очередей (СМО)
Определение системы массового обслуживания
Уравнения Колмогорова
Предельные вероятности состояний
Определение СМО с отказами
Определение СМО с ожиданием (очередью)
Аналитическая геометрия
Векторная алгебра
Метрические понятия и аксиомы геометрии
Равенство и подобие геометрических фигур
Бинарные отношения
Вектор, его направление и длина
Линейные операции над векторами
Линейная зависимость и независимость векторов
Отношение коллинеарных векторов
Проекции векторов на прямую и на плоскость
Угол между векторами
Ортогональные проекции векторов
Координата вектора на прямой и базис
Координаты вектора на плоскости и базис
Координаты вектора в пространстве и базис
Операции над векторами в координатной форме
Ортогональный и ортонормированный базисы
Cкалярное произведение векторов и его свойства
Выражение скалярного произведения через координаты векторов
Векторное произведение векторов и его свойства
Смешанное произведение векторов и его свойства
Ориентированные площади и объемы
Двойное векторное произведение и его свойства
Применение векторов в задачах на аффинные свойства фигур
Применение произведений векторов при решении геометрических задач
Применение векторной алгебры в механике
Системы координат
Прямоугольные координаты
Преобразования прямоугольных координат
Полярная система координат
Цилиндрическая система координат
Сферические координаты
Аффинные координаты
Аффинные преобразования координат
Аффинные преобразования плоскости
Примеры аффинных преобразований плоскости
Аффинные преобразования пространства
Многомерное координатное пространство
Линейные и аффинные подпространства
Скалярное произведение n-мерных векторов
Преобразования систем координат
Геометрия на плоскости
Алгебраические линии на плоскости
Общие уравнения геометрических мест точек
Алгебраические уравнения линий на плоскости
Уравнения прямой, проходящей через точку перпендикулярно вектору
Уравнения прямой, проходящей через точку коллинеарно вектору
Уравнения прямой, проходящей через две точки
Уравнения прямой с угловым коэффициентом
Взаимное расположение прямых
Примеры задач с прямыми на плоскости
Системы неравенств с двумя неизвестными
Системы линейных уравнений с двумя неизвестными
Линии 2-го порядка
Канонические уравнения линий второго порядка
Порядок приведения уравнения линии к каноническому виду
Эллипс
Гипербола
Парабола
Квадратичные неравенства с двумя неизвестными
Применение линий 1-го и 2-го порядков в задачах на экстремум функций
Инварианты линий
Классификация линий 2-го порядка по инвариантам
Приведение уравнения линии к каноническому виду по инвариантам
Геометрия в пространстве
Способы задания ГМТ в пространстве
Алгебраические уравнения поверхностей
Уравнения плоскости, проходящей через точку перпендикулярно вектору
Уравнения плоскости, компланарной двум неколлинеарным векторам
Уравнения плоскости, проходящей через три точки
Взаимное расположение плоскостей
Типовые задачи с плоскостями
Уравнения прямых в пространстве
Взаимное расположение прямых в пространстве
Типовые задачи с прямыми в пространстве
Поверхности 2-го порядка
Канонические уравнения поверхностей
Порядок приведения уравнения поверхности к каноническому виду
Поверхности второго порядка
Эллипсоиды
Гиперболоиды
Конусы
Параболоиды
Применение поверхностей 1-го и 2-го порядков в задачах на экстремум функций
Инварианты поверхностей
Линейная алгебра
Матрицы и операции
Линейные операции над матрицами
Умножение матриц
Возведение матриц в степень
Многочлены от матриц
Транспонирование и сопряжение матриц
Блочные матрицы
Произведение и сумма матриц Кронекера
Метод Гаусса приведения матрицы к ступенчатому виду
Элементарные преобразования матриц
Определители
Определители матриц и их основные свойства
Формула полного разложения определителя
Формула Лапласа полного разложения определителя
Определитель произведения матриц
Методы вычисления определителей
Ранг матрицы
Линейная зависимость и линейная независимость строк (столбцов) матрицы
Ранг матрицы и базисный минор матрицы
Методы вычисления ранга матрицы
Ранг системы столбцов (строк)
Обратная матрица
Обратные матрицы и их свойства
Ортогональные и унитарные матрицы
Способы нахождения обратной матрицы
Матричные уравнения
Односторонние обратные матрицы
Скелетное разложение матрицы
Полуобратная матрица
Псевдообратная матрица
Системы уравнений
Системы линейных алгебраических уравнений
Метод Гаусса решения систем линейных уравнений
Структура общего решения системы уравнений
Решение систем с помощью полуобратных матриц
Псевдорешения системы линейных уравнений
Функциональные матрицы
Функциональные матрицы скалярного аргумента
Производные матриц по векторному аргументу
Линейные и квадратичные формы и их преобразования
Приведение форм к каноническому виду
Закон инерции вещественных квадратичных форм
Знакоопределенность форм вещественных квадратичных
Формы и исследование функций на экстремум
Многочленные матрицы
Многочленные матрицы (лямбда-матрицы)
Операции над лямбда-матрицами
Простые преобразования многочленных матриц
Инвариантные множители многочленной матрицы
Функции от матриц
Собственные векторы и значения матрицы
Подобие числовых матриц
Характеристический многочлен матрицы
Минимальный многочлен матрицы
Теорема Гамильтона-Кэли
Жорданова форма матрицы
Приведение матрицы к жордановой форме
Многочлены от матриц
Применение многочленов от матриц
Функции от матриц
Линейные пространства
Линейные пространства: определение и примеры
Линейная зависимость и независимость n-мерных векторов
Размерность и базис линейного пространства
Преобразования координат в линейном пространстве
Изоморфизм линейных пространств
Подпространства
Подпространства линейного пространства
Пересечение и сумма подпространств
Способы описания подпространств
Нахождение дополнения и суммы подпространств
Нахождение пересечения подпространств
Линейные отображения
Линейные многообразия
Линейные отображения
Матрица линейного отображения
Ядро и образ линейного отображения
Линейные операторы
Линейные операторы (преобразования)
Инвариантные подпространства
Собственные векторы и значения оператора
Свойства собственных векторов операторов
Канонический вид линейного оператора
Методика приведения линейного преобразования к каноническому виду
Евклидовы пространства
Евклидовы пространства
Ортогональные векторы евклидова пространства
Ортогональный базис евклидова пространства
Ортонормированный базис евклидова пространства
Ортогональные дополнения в евклидовом пространстве
Задача о перпендикуляре
Матрица и определитель Грама и его свойства
Линейные преобразования евклидовых пространств
Канонический вид ортогонального оператора евклидова пространства
Сопряженные операторы евклидова пространства
Самосопряженные операторы евклидова пространства
Приведение квадратичной формы к главным осям
Унитарные пространства и их линейные преобразования
Комплексный анализ
Комплексные числа
Комплексные числа в алгебраической форме
Комплексные числа в тригонометрической и показательной формах
Множества на комплексной плоскости
Последовательности и ряды комплексных чисел
Комплексные функции
Функции комплексного переменного. Предел, непрерывность и производная
Элементарные функции комплексного переменного
Дифференцирование функций комплексного переменного
Аналитические функции и их свойства
Конформные отображения
Функциональные ряды в комплексной области
и их свойства Интегрирование функций комплексного переменного
Функциональные ряды и последовательности
Степенные ряды и их свойства
Разложение функций в степенные ряды
Нули аналитических функций
Ряд Лорана и разложение функций по целым степеням
Особые точки, Вычеты
Изолированные особые точки функций и полюсы
Вычеты и их применение
Вычисление интегралов с помощью вычетов
Вычеты и расположение нулей многочлена
Операционное исчисление
Дифференциальные уравнения
ДУ первого порядка
Основные понятия и определения ДУ
Метод изоклин для ДУ 1-го порядка
Метод последовательных приближений
ДУ с разделяющимися переменными
Однородные ДУ
Линейные ДУ 1-го порядка
Дифференциальное уравнение Бернулли
ДУ в полных дифференциалах
Интегрирующий множитель
ДУ, не разрешенные относительно производной
Дифференциальное уравнение Риккати
Составление ДУ семейств линий
Задачи на траектории
Особые решения ДУ
ДУ высших порядков
Понятия и определения ДУ высших порядков
ДУ, допускающие понижение порядка
Линейная независимость функций
Определители Вронского и Грама
Однородные и неоднородные дифференциальные уравнения
Задача Коши и Уравнение Эйлера
Линейные ДУ с переменными коэффициентами
Метод Лагранжа решения ДУ
Краевые задачи для ДУ высших порядков
Разложение решения ДУ в степенной ряд
Разложение решения ДУ в обобщенный степенной ряд
Нахождение периодических решений ДУ
Асимптотическое интегрирование ДУ
Системы ДУ
Системы ДУ: понятия и определения
Сведение системы ДУ к одному уравнению
Нахождение интегрируемых комбинаций
Интегрирование однородных линейных систем ДУ
Методы интегрирования неоднородных систем ДУ
Преобразование Лапласа и решение ДУ и систем
Теория устойчивости
Численные методы
Методы алгебры
Численные методы линейной алгебры
Численные методы решения СЛАУ
Итерационный метод Шульца обратной матрицы
Методы решения задач о собственных значениях и векторах матрицы
Методы решения нелинейных уравнений
Методы решения систем нелинейных уравнений
Методы теории приближений
Методы приближения сеточных функций
Методы функциональной интерполяции
Методы интегрально-дифференциальной интерполяции
Методы интегрального сглаживания
Методы интерполяции и сглаживания сплайнами
Методы численного дифференцирования и интегрирования
Методы численного дифференцирования
Методы численного интегрирования
Методы решения обыкновенных ДУ
Численные методы решения задачи Коши
Разностные схемы для решения задачи Коши
Составные схемы для решения задачи Коши
Экстраполяционные методы решения задачи Коши
Непрерывно-дискретные методы решения задачи Коши
Численные методы решения краевых задач
Методы решения ДУ в частных производных
Численные методы решения уравнений математической физики с двумя переменными
Принципы построения разностных схем для уравнений в частных производных
Разностные схемы решения уравнений в частных производных 1-го порядка
Разностные схемы решения уравнений в частных производных 2-го порядка
Численные методы решения уравнений в частных производных
Численные методы решения уравнений математической физики с тремя переменными
|
Формализованное исчисление высказыванийВ этой лекции рассматривается аксиоматический подход к алгебре высказываний, т.е. такой же подход, какой используется при строгом построении геометрии на базе какой-либо системы аксиом, например систем Гильберта, Вейля и т.д. Алгебра высказываний предстанет как аксиоматическая теория, в определенном смысле достигнет наивысшей степени строгости изложения и совершенства. Формализованное исчисление высказываний, которое рассмотрено в этой лекции, будет служить примером аксиоматической теории. Применительно к алгебре высказываний аксиоматический подход состоит в следующем. Из всех формул алгебры высказываний выделяется некоторая часть. Формулы из этой части объявляются аксиомами. Определяется некоторое правило, по которому из одних формул можно получать новые. Аксиомы выделяются, а правило определяется так, что по нему из аксиом могут быть получены все тавтологии алгебры высказываний, и только они. Таким образом, тавтологии алгебры высказываний оказываются теоремами аксиоматической теории, в результате получаем аксиоматическое построение алгебры высказываний. В качестве системы аксиом могут быть выбраны разные части совокупности всех формул алгебры высказываний. То же относится к правилам получения новых формул. В зависимости от выбора получаются различные аксиоматизации алгебры высказываний. Общим для них является то, что все они обладают одним и тем же множеством теорем — это совокупность всех тавтологий алгебры высказываний. Мы рассмотрим лишь одну из возможных аксиоматизаций. Система аксиом и теория формального выводаВ настоящей лекции будет заложена основа аксиоматической теории высказываний, определены понятия доказательства и теоремы, рассмотрены примеры доказательств теорем и развита теория формального вывода. К первоначальным, неопределяемым понятиям аксиоматической теории высказываний относятся следующие: — пропозициональные переменные; — логические связки; — технические знаки. Первоначальным понятием является также понятие формулы, которое определяется (как и в алгебре высказываний, см. определение 2.1) индуктивным образом: 1) каждая пропозициональная переменная есть формула; 2) если и — формулы, то выражения также являются формулами; 3) никаких других формул, кроме получающихся согласно пунктам 1 и 2 нет. Следующий шаг в построении аксиоматической теории высказываний состоит в выборе системы аксиом. В качестве аксиом выбираются формулы следующих видов: где — произвольные формулы. Таким образом, каждое из выражений задает лишь форму аксиомы. Они превращаются в аксиомы, если вместо и подставить конкретные формулы (в частности, пропозициональные переменные). Следовательно, каждое из этих выражений задает бесконечное множество формул. Все они называются аксиомами. Поэтому каждое из выражений называют схемой аксиом. Наконец, заключительный шаг, закладывающий основу аксиоматической теории высказываний, состоит в выборе правил вывода. Единственным правилом вывода будет служить правило заключения (или отделения, или modus ponens, или сокращенно ): из формул и непосредственно следует формула . Как и в алгебре высказываний, внешние скобки у формулы принято не писать. Поскольку в аксиомах не участвуют связки , то их придется определить. Введем следующие определения: означает ; означает ; означает . Смысл, например, первого из определений состоит в том, что, каковы бы ни были формулы и , формула служит обозначением для формулы . Понятие вывода и его свойстваЗаложив основу будущей аксиоматической теории в виде системы аксиом и правила вывода, приступим к ее развитию, т.е. к доказательству теорем. Прежде всего уточним понятия доказательства и теоремы. Определение 15.1. Доказательством или выводом формулы из множества формул называется такая конечная последовательность формул, каждая формула которой является либо аксиомой, либо формулой из , либо получена из двух предыдущих формул этой последовательности по правилу , а последняя формула совпадает с . Если имеется вывод формулы из множества , то говорят, что выводима из или что выводит , и пишут . Элементы из называются гипотезами или посылками вывода. Если же имеется вывод формулы из пустого множества гипотез, то говорят, что выводима из аксиом (или что доказуема), а последовательность называется доказательством этой формулы. Саму называют теоремой, и пишут . Таким образом, запись служит сокращением утверждения " есть теорема". Если множество конечно: , то вместо будем писать . Совокупность аксиом, правил вывода и всех теорем, выводимых из аксиом, и представляет собой аксиоматическую теорию высказываний (или формализованное исчисление высказываний). Наша ближайшая цель состоит в том, чтобы научиться доказывать теоремы в данной теории, т.е. научиться строить выводы формул из аксиом. Приведем пример доказательства какой-нибудь формулы. Пример 15.2. Доказать: . Для доказательства того, что формула является теоремой формализованного исчисления высказываний, нужно построить вывод (доказательство) этой формулы из аксиом. Таким выводом является, например, следующая последовательность формул: Формула (1) представляет собой аксиому (А2), в которой в качестве формул и взята формула , а в качестве формулы взята формула . Формула (2) представляет собой аксиому (А1), в которой в качестве формулы берется формула . Формула (3) получена из формул (1) и (2) по правилу . Формула (4) есть аксиома (А1). Наконец, формула (5) получена из формул (3) и (4) по правилу modus ponens. Таким образом, доказано, что . В следующей теореме отмечается несколько простых, но важных свойств понятия выводимости из гипотез. Теорема 15.3 (свойства выводимости). а) Если и , то ; б) тогда и только тогда, когда в существует такое конечное подмножество , что ; в) Если для любой формулы из множества и , то . Доказательство. а) Данное свойство выражает следующий очевидный факт: если формула выводима из множества посылок , то она будет выводима и из всякого множества, получающегося добавлением к новых посылок. б) Достаточность вытекает из свойства (а). Обратно, если , то, по определению 15.1, существует вывод из , т.е. некоторая конечная последовательность формул, использующая, следовательно, лишь конечное число посылок из . Поэтому можно считать, что именно эта конечная часть формул из и выводит формулу . в) По условию . Тогда ввиду предыдущего свойства (б) в существует такое конечное подмножество , что . Пусть . По условию, кроме того, , т.е. имеются выводы каждой из формул из множества гипотез , представляющие собой конечные последовательности формул. Выпишем эти последовательности одну за другой и добавим к ним последовательность, являющуюся выводом формулы из множества гипотез . Полученная таким образом последовательность будет представлять собой вывод формулы Fm множества гипотез , т.е. . Теорема о дедукции и следствия из нееПроцесс построения доказательств для тех или иных формул может оказаться достаточно сложным как в идейном, так и в техническом плане Теорема о дедукции, о которой пойдет речь, выявляет некоторую общую закономерность при таких построениях и тем самым облегчает процесс построения доказательства, что будет видно из последующих примеров. Теорема 15.4 (о дедукции). Если , то . В частности, если , то . Доказательство. Пусть последовательность формул (1) является выводом формулы из гипотез (такая последовательность существует, поскольку, по условию, . Следовательно, формула есть формула , т.е. ( — знак графического совпадения, одинаковости формул). Рассмотрим последовательность формул: (2) На последнем месте данной последовательности стоит формула (так как ). Но эта последовательность, вообще говоря, не является выводом из гипотез . Тем не менее ее можно превратить в такой вывод, если перед каждой формулой последовательности добавить подходящие формулы. Для этого покажем методом математической индукции по , что (3) 1) . Покажем, что . Для формулы как первого члена последовательности (1), являющейся выводом из , могут представиться следующие возможности: а) есть либо одна из аксиом, либо одна из гипотез . В этом случае вывод формулы из гипотез строится так: (4) где вторая формула есть аксиома (А1), а третья получена из первых двух по правилу modus ponens. Таким образом, в последовательность (2) перед первой формулой нужно добавить первую и вторую формулы из последовательности (4); б) есть гипотеза . Тогда формула принимает вид . Но согласно примеру 15.2, эта формула выводима не только из гипотез , но и просто из аксиом. В этом случае ее вывод, приведенный в примере 15.2, нужно вписать в последовательность (2) перед первой формулой; 2) . Предположим, что утверждение (3) верно для всех и все необходимые выводы добавлены перед всеми первыми формулами последовательности (2); 3) . Покажем теперь, что утверждение (3) верно для , т.е. справедлива выводимость: . Для формулы как члена последовательности (1), являющейся выводом из гипотез , могут представиться следующие возможности: а), б) есть либо одна из аксиом, либо одна из гипотез . Данные возможности абсолютно аналогичны соответствующим возможностям из случая (там лишь нужно заменить на ); в) получена из двух предыдущих формул последовательности (1) по правилу MP. Следовательно, , а формула имеет вид: , то есть . Поскольку и , то формулы и стоят в последовательности (2) перед формулой а следовательно, по предположению индукции, справедливы утверждения о том, что имеются выводы этих формул из гипотез . Выпишем эти выводы последовательно один за другим, они завершаются формулами и соответственно (напоминаем, что ): Продолжим выводы следующими формулами: Первая из формул есть аксиома (А2), вторая формула получена из первой и формулы по правилу MP, третья получена из второй и формулы (а) по правилу MP. Таким образом, построенная последовательность есть в этом случае вывод формулы из гипотез . Итак, утверждение (3) верно для любого . При получаем (напоминаем, что ): , что и требовалось доказать. Следствие 15.5. тогда и только тогда, когда . Доказательство. Необходимость представляет собой теорему о дедукции. Обратно, если , то существует соответствующий вывод: . Дополним его двумя формулами и Получим последовательность , представляющую собой вывод формулы из гипотез , потому что предпоследняя формула этой последовательности есть одна из гипотез, а последняя получена из двух предшествующих ей формул по правилу MP. Следовательно, . Следствие 15.6. тогда и только тогда, когда Доказательство. Данное следствие получается в результате m-кратного применения предыдущего следствия. Применение теоремы о дедукцииС помощью теоремы о дедукции сначала будет доказана одна лемма, которая затем вместе с теоремой о дедукции будет использована для доказательства того, что ряд формул являются теоремами формализованного исчисления высказываний. Лемма 15.7. Для любых формул справедливы следующие выводимости: а) ; б) . Доказательство. а) Покажем сначала, что . Для этого построим последовательность, являющуюся соответствующим выводом: . Поясним. Первые три формулы последовательности суть гипотезы. Четвертая формула получена из первой и третьей формул последовательности по правилу modus ponens, а пятая — из второй и четвертой по тому же правилу. Итак, и . Отсюда на основании теоремы о дедукции заключаем, что б) Нетрудно видеть, что , откуда требуемая выводимость следует на основании теоремы о дедукции. Теорема 15.8. Для любых формул следующие формулы являются теоремами формализованного исчисления высказываний: а) ; б) ; в) ; г) ; д) ; е) ; ж) . Доказательство. а) Обоснуем возможность доказательства (построения вывода из аксиом) этой формулы. Рассмотрим следующую последовательность формул: (1): [аксиома (A3)]; (2): [пример 15.2]; (3): [(1), (2), лемма 15.7, пункт б]; (4): ([аксиома (А1)]; (5): [(4), (3), лемма 15.7, пункт а]. Обратим внимание на то, что сама последовательность (1) —(5) не является выводом формулы из аксиом. Чтобы превратить ее в вывод, нужно перед формулами (2) и (5) вписать их выводы из аксиом. Для формулы (2) это сделать нетрудно. Обоснование формулы (5) опирается на утверждение леммы 15.7 пункт а, которое, в свою очередь, обосновано с помощью теоремы о дедукции. Поэтому, чтобы это утверждение можно было использовать в формальном выводе, его необходимо превратить в некоторую формулу, вывод которой, в свою очередь, должен быть построен на основании теоремы о дедукции. Продумайте самостоятельно эти взаимосвязи. б) Строим последовательность формул, которая также выводом не является, а служит лишь обоснованием возможности построения такого вывода, но которую можно дополнить до вывода без принципиальных трудностей: (1): [аксиома (A3)]; (2): [теорема 15.8, а]; (3): [правило МР: (1), (2)]; (4): [аксиома (А1)]; (5): [лемма 15.7, а: (4), (3)]. в) В двух предыдущих доказательствах теорема о дедукции применялась опосредованно через лемму 15.7. В настоящей задаче происходит прямое применение этой теоремы. Это делается следующим образом. Покажем сначала, что . Приводим соответствующий вывод, обосновать который предлагается самостоятельно (это уже действительно вывод, но пока еще вывод из гипотез — вывод формулы из гипотез ): Итак, . Тогда по теореме о дедукции . Применяя еще раз теорему о дедукции, получаем . г) Покажем, что . Для этого строим соответствующий вывод (обоснуйте его самостоятельно): Итак, . Применив теперь дважды теорему о дедукции, получаем требуемый результат. д) Покажем сначала, что . Строим последовательность формул, которая выводом не является (снова обращаемся к лемме 15.7 и еще к доказанным выше теоремам), но может быть дополнена до такового: (1): [использована гипотеза]; (2): [теорема 15.8, пункт а]; (3): [лемма 15.7, пункт а: (2), (1)]; (4): [теорема 15.8, пункт б]; (5): [лемма 15.7, пункт а: (3), (4)]; (6): [теорема 15.8, пункт г]; (7): [правило MP: (5), (6)]. Применив теорему о дедукции, получаем требуемое утверждение. е) По правилу MP имеем . Тогда по теореме о дедукции . Применяем еще раз теорему о дедукции: . Далее, по пункту д) настоящей теоремы имеем (взяв в качестве формулу , а в качестве — саму ): Из этих двух последних утверждений на основании леммы 15.7 (пункт а) получаем . ж) Покажем сначала, что . В самом деле, строим соответствующую последовательность (определите самостоятельно, что это — вывод из гипотез или обоснование возможности его построения): Итак, . Следовательно, по теореме о дедукции . Еще раз применяя теорему о дедукции, получаем: Производные правила выводаАксиоматическая теория высказываний развита довольно глубоко: теорема о дедукции, вскрыв важное свойство выводимости, оказалась мощным средством, облегчающим доказательства того, что та или иная формула является теоремой формализованного исчисления высказываний. Следующим шагом на этом пути служит выявление дальнейших закономерностей процесса выведения одних формул из других и формулировка таких закономерностей в виде правил вывода. Получаемые вторичные правила вывода носят название производных правил вывода. Разделим их на две группы и сформулируем их в двух теоремах: в одной — производные правила введения логических связок, в другой — производные правила удаления таких связок. Для формулировки правил будет использоваться символическая запись. Например, правило состоит в следующем: "Если и , то ". Теорема 15.9 (правила введения логических связок). Справедливы следующие производные правила вывода, называемые правилами введения логических связок (где — некоторое, возможно и пустое, множество формул): а) введение импликации ; б) введение конъюнкции ; в) введение дизъюнкции ; г) введение отрицания (приведение к абсурду) . Доказательство. а) Данное правило есть не что иное, как теорема о дедукции (теорема 15.4). б) Обосновать правило предлагается самостоятельно. Напомним только, что запись , согласно определению, означает . в) Обоснуем первое правило. При доказательстве теоремы 15.8, (пункт в) показано, что , или . Отсюда, по теореме о дедукции, заключаем, что , т.е. на основании определения логической связки дизъюнкции . Поэтому если , то отсюда, в силу теоремы 15.3 (пункт в), заключаем, что . Обосновать второе правило введения дизъюнкции предлагается самостоятельно. г) Пусть дано, что и . Тогда, по теореме о дедукции, и . Выпишем одну за другой обе последовательности формул, представляющие собой выводы формул и из множества посылок Продолжим полученную последовательность следующим образом [использована теорема 15.8, пункт д]; [МР: ]; [теорема 15.8, пункт д]; [МР: ]; [теорема 15.8, пункт д] [MP: ]; [теорема 15.8, пункт d]; ( [MP: ]; [теорема 15.8, пункт а]; [лемма 15.7 о: ]; [аксиома (A3)]; [MP: ]; [МР: ]; Тем самым доказано, что . Правила удаления логических связокТеорема 15.10 (правила удаления логических связок). Справедливы следующие производные правила вывода, называемые правилами удаления логических связок (где — некоторое, возможно и пустое, множество формул): а) удаление импликации ; б) удаление конъюнкции ; в) удаление конъюнкции ; г) удаление дизъюнкции (Генцен): ; д) удаление дизъюнкции (Клини): ; е) сильное удаление отрицания (сильное ): ; ж) слабое удаление отрицания (слабое ): . Доказательство. а) Это правило получается непосредственно на основании правила вывода modus ponens. б) Обоснуем второе из двух правил удаления конъюнкции, предоставив сделать обоснование первого правила самостоятельно. Пусть . Покажем, что . Напомним, что по определению конъюнкции запись означает . Поэтому нужно показать, что . Строим соответствующий вывод: (1): [использована гипотеза]; (2): [аксиома (А1)]; (3): [MP: (1), (2)]; (4): [аксиома (A3)]; (5): [MP: (3), (4)]; (6): [аксиома (Al)]; (7): [MP: (5), (6)]. Итак, и . Следовательно, по теореме 15.3, (пункт в) заключаем, что . е) Пусть . Ввиду теоремы 15.8, (пункт а) имеем , что на основании следствия 15.6 из теоремы о дедукции дает выводимость . Следовательно, из двух выводимостей и no теореме 15.3, (пункт в) заключаем, что .
Математический форум (помощь с решением задач, обсуждение вопросов по математике).
Если заметили ошибку, опечатку или есть предложения, напишите в комментариях.
|
Часовой пояс: UTC + 3 часа [ Летнее время ] |