Заглавная страница Избранные статьи Случайная статья Познавательные статьи Новые добавления Обратная связь КАТЕГОРИИ: АрхеологияБиология Генетика География Информатика История Логика Маркетинг Математика Менеджмент Механика Педагогика Религия Социология Технологии Физика Философия Финансы Химия Экология ТОП 10 на сайте Приготовление дезинфицирующих растворов различной концентрацииТехника нижней прямой подачи мяча. Франко-прусская война (причины и последствия) Организация работы процедурного кабинета Смысловое и механическое запоминание, их место и роль в усвоении знаний Коммуникативные барьеры и пути их преодоления Обработка изделий медицинского назначения многократного применения Образцы текста публицистического стиля Четыре типа изменения баланса Задачи с ответами для Всероссийской олимпиады по праву Мы поможем в написании ваших работ! ЗНАЕТЕ ЛИ ВЫ?
Влияние общества на человека
Приготовление дезинфицирующих растворов различной концентрации Практические работы по географии для 6 класса Организация работы процедурного кабинета Изменения в неживой природе осенью Уборка процедурного кабинета Сольфеджио. Все правила по сольфеджио Балочные системы. Определение реакций опор и моментов защемления |
Основные положения математической логики
Формальные теории Логика высказывания является одной из разновидностей формальных теорий. Формальная теория : 1) множество символов ,образующих алфавит; 2) множество слов в алфавите, которые называются формулами; 3) подмножество ; состоит из аксиом; 4) множество отношений (не обязательно бинарных) на множестве формул, которые называются правилами вывода. Множества и образуют язык, или сигнатуру. Понятия «истинность» и «ложность» отсутствуют. Существенна лишь выводимость, или доказуемость. Пусть – формулы теории . Если существует такое правило вывода , что , то говорят, что формула непосредственно выводима (или доказуема) из формул по правилу вывода (т.е. не является композицией каких-то иных отношений). Обычно этот факт записывают в виде . Формулы в числителе называются посылками, а формула в знаменателе – заключением, или секвенцией. Иногда обозначение правила вывода справа от черты дроби опускают, если ясно, о чем идет речь. Вывод формулы из формул – это такая последовательность формул , что , а любая из формул является либо аксиомой, либо исходной формулой , либо непосредственно выводимой из ранее полученных формул. Если формула выводима из формул в теории , то это обозначается так: . Формулы называются гипотезами вывода. Если формула G непосредственно выводима из аксиом (т.е. без гипотез), то она называется теоремой. Обозначение: . Если некоторый набор гипотез позволяет вывести формулу, то добавление гипотез не должно приводить к невыводимости: . Интерпретацией формальной теории в области интерпретации называется функция I: , которая с каждой формулой формальной теории сопоставляет некоторое содержательное высказывание относительно объектов множества . Это высказывание может быть истинным, ложным или не иметь значения истинности. Если соответствующее высказывание является истинным, то формула выполняется в данной интерпретации. Интерпретация называется моделью множества формул, если все формулы этого множества выполняются в данной интерпретации. Интерпретация называется моделью формальной теории, если все теоремы этой теории выполняются в данной интерпретации (т.е. все выводимые формулы модели являются истинными в данной интерпретации).
Формула называется общезначимой (или тавтологией), если она истинна в любой интерпретации. Исчисление высказываний Рассмотрим исчисление высказываний как формальную теорию. В алгебре высказываний имеется понятие истинности. В соответствии с общей конструкцией формальных теорий в алгебре высказываний вводятся следующие понятия: 1. Множество символов , образующих алфавит: – и – связки; – (, ) – служебные символы; – – пропозициональные переменные. 2. Формулы: – переменные суть формулы; – если – формулы, то ( ) и ( ) – формулы. 3. Аксиомы: ; ; . Здесь приведены схемы аксиом. Поскольку и – любые формулы, то аксиом бесконечно много. (В конструктивном определении исчисления высказываний в указанные аксиомы входят конкретные формулы, но вводится еще одно правило вывода.) 4. Правило: – modus ponens. Другие связки вводятся определениями (а не аксиомами): . Если в формулу подставить вместо переменных подставить соответственно формулы , то получится формула, которая называется частным случаем исходной. Набор подстановок называется унификатором. Формула называется совместным частным случаем формул и , если является частным случаем и частным случаем при одном и том же общем унификаторе. Наименьший возможный унификатор называется наиболее общим унификатором. При конструктивном определении исчисления высказываний помимо приведенного правила modus ponens вводится еще одно, называемое правилом подстановки: если формула является частным случаем формулы , то формула непосредственно выводима из . Теорема 1. . Доказательство. В аксиому : вместо подставим . Тем самым выведем формулу . По второй аксиоме : . Подставим вместо , вместо : . Теперь видим, что по правилу modus ponens выводится формула . Подключаем : , заменив на : . По правилу modus ponens , что и требовалось доказать. Теорема 2. (правило введения импликации). Доказательство. – гипотеза. : – гипотеза . По правилу modus ponens , что и требовалось доказать. Теорема 3. Если , , то , и наоборот (дедукция). Доказательство. Дано: существуют , такие, что , а – либо аксиомы, либо , либо , либо , .
Доказательство проводим по индукции. Необходимо доказать, что если существует вывод , то , ,… 1. Докажем, что . Дано: , . Доказать: . Возможны три случая: а) – аксиома. Применяем первую аксиому: : . По правилу МР , МР , или (в левой части аксиомы не пишут); б) . Тогда : . Предположим, что . Тогда по МР МР . Значит, , . Но так как , то в левой части писать незачем, и ; в) . Тогда , . Выше было показано, что . Принимая правую (выведенную) часть , в виде гипотезы и используя : , по правилу МР получаем . Это можно записать в виде . Но , значит, . 2. Пусть выведены. Выведем : . Возможны те же три случая а – в, которые доказываются аналогично, но существует и четвертый случай: . Используем вторую аксиому : . Получаем . – это гипотеза индукции, которая считается выведенной. По МР . Опять-таки, – гипотеза вывода, и по МР . Результат: . При приходим к утверждению теоремы. Обратная теорема: . Доказательство. Примем выведенное утверждение в качестве гипотезы. Если – гипотеза, то по МР . Отсюда , что и требовалось доказать. Следствие 1. Если , то , и обратно. Следствие 2. , (правило транзитивности). Доказательство. , – гипотезы. По правилу МР , – гипотезы. Значит, . Это записываем в виде , , . По теореме дедукции , , что и требовалось доказать. Следствие 3. , (правило сечения). Другие теоремы: ; ; ; ; ; ; , …. Способы доказательства теорем в исчислении высказываний следующие: 1. Использовать методику, приведенную выше. Ее суть – применение аксиом, правил вывода и поиск унификаторов. Каждая выведенная теорема подключается к списку левой части любого вывода. Основное средство – теорема дедукции: , . 2. С помощью теоремы дедукции привести выводимую в ИВ (исчислении высказываний) формулу к виду теоремы (т.е. от предложенного для вывода перейти к выводу теоремы): , где . Далее записать формулу АВ (алгебры высказываний): . Можно также использовать рассмотренные в АВ эквивалентности либо составить таблицу истинности (с помощью ЭВМ) и убедиться в тавтологичности этой формулы (т.е. в том, что при любых значениях пропозициональных переменных она принимает значение «истина»). Если это не так, то формула ИВ не является выводимой. 3. В большинстве случаев проще доказывать невыводимость противоположной формулы. Это так называемый метод доказательства от противного: , , где – противоречие, что эквивалентно . Докажем выводимость , если выводимо , . Для этого, как было сказано выше, приведем вывод формулы , к виду теоремы, используя дедукцию: , . Теперь запишем соответствующую формулу АВ (в булевой форме) и преобразуем, используя эквивалентности АВ: . Это значит, что соответствующая формула ИВ выводима: . Пользуясь теоремой, обратной к теореме дедукции, приходим к выводу, что , т. е. выводимо из , что и требовалось доказать. 4. Доказательство от противного лежит в основе метода резолюции, который базируется на выводимости теоремы . Эту теорему нужно доказать. Используем алгебру высказываний (АВ), считая символ «+» дизъюнкцией, а символ «•» конъюнкцией: , что соответствует аналогичной формуле АВ, которую запишем в булевой форме: . Придадим поочередно значения 0 и 1: ; . Итак, при любых значениях , , данная формула алгебры высказываний имеет значение «истина», что и означает выводимость теоремы .
Полученное правило называется правилом резолюции. Пользуясь дедукцией (точнее, обратной теоремой дедукции), это правило можно записать в виде , либо в виде правила вывода метода резолюции: . Этим правилом вывода, доказанным вполне строго, можно пользоваться наряду с правилом МР. Знаменатель правила имеет название «резольвента». Исчисление предикатов Пусть – произвольное множество. Предположим, что на нем задана тотальная функция (однозначное отображение) на этом множестве : (однозначное отображение), т.е. . Эта функция является -парной (или -местной). Предположим, таких функций несколько: . Этот набор называется сигнатурой, что обозначается как . Пара (, )называется алгеброй. Если функции сигнатуры являются произвольными отношениями, то пара (, )называется моделью. Примеры: 1. Пусть – множество целых чисел. Рассмотрим сигнатуру, состоящую из двух бинарных операций: «+», «*». Возникает алгебра чисел – . 2. Задано произвольное множество и операция «*» (или «+»). Получаемая алгебра называется группой. Частные случаи: – = , «*» – группа целых чисел. – (, «+») – группа целых чисел; (2 , «+») – подгруппа группы целых чисел, или группа четных чисел. Если функции сигнатуры являются произвольными отношениями, то пара (, )называется моделью. Пусть дана алгебра (, ) и подмножество исходных элементов . Применение операции может вывести за пределы этого множества. Замыканием подмножества называется множество, полученное как результат применения всех операций сигнатуры ко всем элементам и к промежуточным результатам применения сигнатуры. Пример. (2; 4; 10; «+»); 2 + 2 = 4; 2 + 4 = 6 (2; 4; 6; 10; «+») – все то, что можно получить, и является замыканием (все четные числа). Элементы сигнатуры называются функторами; – терм. Отображение некоторого множества термов во множество {И, Л} называется атомом. Он состоит из двух объектов: , где – предикат, – список термов. С введением предикатов алгебра логики приобретает динамику. Аргументы (термы), вообще говоря, пробегают множество значений в некоторой области. Некоторые утверждения высказываются для случаев, когда некоторая переменная (терм) пробегает все множество значений и когда она принимает некоторые значения из допустимых. Указанием на пункт А или Б являются кванторы: «все» – All: ; «существует» – Exists: . С помощью кванторов исчисление высказываний обогащается новым типом формул: ; – «И», «Л» в зависимости от .
Переменные, по отношению к которым применим квантор, называются связанными, остальные свободными. В дополнение к этому в исчислении предикатов добавляются новые аксиомы типа П1 ; П2 ; MP: : ; : . Формулой исчисления предикатов является любой стандартный набор, содержащий обычные пропозициональные переменные, снабженные кванторами и , а также связками . Кванторы в этой теории применяются лишь к термам. Такая теория называется теорией первого порядка. В теориях высших порядков кванторы применяются также к литералам – именам пропозициональных переменных и предикатов. Одной из основных задач является приведение формул исчисления предикатов к виду, удобному для вывода. Основные идеи такого приведения: 1. . Пример. Доказать, что число 36 делится на 6. Вместо этого докажем две другие теоремы: 36/2 и 36/3. После доказательства этих теорем следует, что (36/2) и (36/3) (36/6). Значит, исходную формулу желательно представить в виде конъюнкций. 2. Избавиться от отрицаний перед кванторами: , . 3. . Пример. Пусть дана плоскость и вектор нормали. Высказывание 1: все прямые, лежащие в плоскости, перпендикулярны вектору нормали. Высказывание 2: прямая, лежащая в плоскости, перпендикулярна к вектору нормали (квантор – лишний). Значит, надо стремиться оставить только кванторы , после чего их удалить. Для удаления квантора используют рассуждение Сколема.Сам процесс называется сколемизацией:
. Алгоритм заключается в выполнении следующих шагов: Шаг 1. Избавление от импликаций: . Шаг 2. «Протаскивание» отрицаний: . Шаг 3. Вспомогательная операция – разделение связанных переменных. Основная идея заключается в том, что каждая связанная переменная может встречаться только два раза: первый раз – в обозначении квантора, второй – в обозначении терма: … … (… …) = … … (… …). Например, – не имеет смысла; – правильно.
|
||||||||
Последнее изменение этой страницы: 2016-04-19; просмотров: 649; Нарушение авторского права страницы; Мы поможем в написании вашей работы! infopedia.su Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав. Обратная связь - 3.129.19.251 (0.11 с.) |