ЛМвИИ (1086253), страница 4
Текст из файла (страница 4)
Доказательством (или выводом) теоремы называетсяпоследовательность из аксиом, правил вывода и уже доказанных теорем, позволяющихполучить данную теорему. Понятие теоремы не обязательно эффективно, так как может несуществовать эффективной процедуры, позволяющей определять по данной ППФ, существуетли ее вывод в данной ФС. ФС, для которой такая эффективная процедура существуетназывается разрешимой, в противном случае - неразрешимой.ППФ В выводима из ППФ А1, А2, …, An ( или является следствием А1, А2, …, An ) тогдаи только тогда, когда существует такая конечная последовательность ППФ B1, B2, …, Br , что Вrесть В и для любого i (1 ≤ i ≤ r) Bi есть:1.
либо аксиома,2. либо Аi (1 ≤ i ≤ n),3. либо непосредственное следствие некоторых предыдущих ППФ по одному из правилвывода.Элементы последовательности ППФ А1, А2, …, An называются посылками вывода (илигипотезами). Сокращенно вывод В из А1, А2, …, An запишем в виде А1, А2, …, An ├ B, или еслиГ={А1, А2, …, An }, то Г├ В вывод ППФ В без использования посылок есть доказательство ППФВ, а сама В -теорема, и это записывается ├ В.Приведем несколько свойств понятия выводимости из посылок.1. Если Г ⊇П и Г├ В, то П├ В. Это значит, что если ППФ В выводима из множествапосылок, то она также будет выводима, если к Г добавятся новые посылки.2.
Г├ В тогда и только тогда, когда в Г существует конечное подмножество П, длякоторого П├ В. Это очевидно из п. 1.3. Если П├ А и Г├ В для любой ППФ В из множества П, то Г├ А. Это значит, что еслиППФ А выводима из П и каждая содержащая в П ППФ выводима из Г, то ППФ Авыводима из Г.Таким образом, любая формальная система задается четверкой:<T,H,A,R>, гдеТ - множество базовых элементов (алфавит);Н - множество правил конструирования ППФ;А - система аксиом;R - множество правил вывода.Множество Т состоит из конечного или счетного множества элементов (термов,операций), из которых по правилам Н строится синтаксически правильные совокупности (ППФ)формальной системы. Множеством аксиом может быть объявлено любое множествосинтаксически правильных совокупностей.
Применение семантических правил R (правилвывода) к элементам множества А позволяет строить семантически правильные совокупности(выводимые формулы). Соотношение между описанными множествами приведено на рис. 1.1.На рис. 1.2 изображена схема построения формальной аксиоматико-дедуктивной системы.Всякое исчисление содержит правила вывода, необходимые для его формулировки, ониназываются основными. К основным относятся известные со времен Аристотеля следующиеправила и обобщения:Modus ponens (m.p.) - означает: если из А следует В и А истинно, то и В истинно;Modus tollens (m.t.) - означает: если А и В не могут одновременно быть истинными и Аистинно, то В ложно.Укрупнение шагов вывода может быть достигнуто за счет применения производныхправил.
Производным правилом вывода называется правило, которое можно построить изпосылки с помощью основных правил и, возможно, аксиом данного исчисления.Правила вывода делятся на прямые и непрямые. Прямые правила вывода -этоправила непосредственного перехода от одних формул к другим, т.е. от посылки к заключению.Им сопоставляются определенные шаги формального вывода. Непрямые правила вывода сутьправила перехода от одних формальных выводов к другим. Таким правилам соответствуютметаутверждения о преобразованиях одних формальных выводов в другие.Еще одним интересным способом рассуждения который может быть оформлен в виденепрямого производного правила, является метод доказательства от противного. Пусть намнужно доказать вывод формулы А из посылок Г. Тогда данную задачу сводят к следующей:отрицание формулы А добавляют к множеству Г и пытаются получить из посылок ¬А, Гпротиворечие.
Если такое противоречие получено, например мы выводим и В, и ¬В, то этоозначает, что можно построить вывод А из Г. Обозначив противоречие константой можнозаписать соответствующие этому типу рассуждений правило:из ¬А, Г├ f следует Г├ А.Заметим, что способ рассуждения от противного, который выражен приведеннымправилом является сугубо классическим.
Существует аналогичный, но более слабый способ,который можно выразить правилом :из А, Г├ f следует Г├ ¬А1.3. Логика высказываний.Высказывание - повествовательное предложение (декларативная фраза), о которомможно сказать, истинно онс или ложно. Значения "истинно" и "ложно" обычно обозначают 1или 0, или И и Л, или Т и F. Высказывания составляют элементарные фразы логического языка,называемые атомарными формулами или атомами. Будем обозначать атомарные формулылюбыми буквами, возможно с индексами.Из атомарных высказываний с помощью логических операций строятся сложныевысказывания (формулы алгебры высказываний). Правила построения формул определяетсясинтаксисом языка исчисления высказываний:• всякое высказывание есть формула;• если X и Y - формулы, то ¬X, (Х^Y), (XvY), (X→Y), (X↔Y) -формулы.Таким образом, синтаксис позволяет выделить формулы из произвольных соединенийсимволов.
Первое правило, называемое базисом, сопоставляет высказывания висячим узлам, авторое (называемое индукционным шагом) порождает дерево, корнем которого является связка,называемая главной связкой формулы. Например, для формулы a^(bvс) имеем дерево:В рассмотренной формуле символы а, b и с являются конкретными высказываниями,прописные же буквы в этой формуле служат для обозначения формулы вообще и называютсямета символами.Семантика - это набор правил интерпретации формул. Интерпретацией называетсяприписывание формуле одного из двух значений истинности: И (истинно) или Л (ложно).Композиционность семантики заключается в том, что приписываемое значение истинностинекоторой формуле зависит от значения истинности ее составляющих высказываний иструктуры формулы.Интерпретация, при которой формула истинна, называется моделью этой формулы.Формула общезначима, если она всегда истинна, независимо от значений истинностисоставляющих ее высказываний.
Выполнимой называется формула, для которой существуетхотя бы одна интерпретация, для которой она истинна. Невыполнимую формулу называютпротиворечивой. Общезначимые формулы иначе называют тавтологиями. Если А формула, то запись ╞ А есть тавтология. Или в более общем виде: если Е - множество формул,то E╞ A означает, что все интерпретации, обращающие все формулы из E в истинные,обращают в истинную и формулу А.
При этом А является логическим следствием Е. Такимобразом, тавтология является логическим следствием из пустого множества. Примеры,поясняющие данные определения, будут приведены позднее.Фундаментальная проблема логики, называемая проблемой дедукции, состоит в том,чтобы определить, является ли формула А логическим следствием множества Е. Само словодедукция (лат. deductio - выведение) определяется как логическое умозаключение от общихсуждений к частным или другим общим суждениям. Если логическим следствием из множестваформул Е является формула А, имеющая значение истинности Л (ложь или 0), то говорят, чтоформула А невыполнима. В этом состоит принцип дедукции: формула А является логическимследствием множества E тогда и только тогда, когда E∪ {¬ A } невыполнимо.Семантика логических связок определяется таблицей истинности.
Таблица для связкииз n операндов (высказываний) имеет 2n строк, или интерпретаций. Ниже приводится таблицаистинности связок для n=2.Таблица 1.1AB¬AAvBA^BA→BA↔BA|BA↓BA⊕BЛЛИЛЛИИЛИИЛИИИЛИЛИИЛИЛЛИЛЛЛИИЛИИЛИИИИЛЛЛСодержательно логические связки обычно интерпретируется следующим образом:отрицание (инверсия) ¬ (¯ ) - "не";дизъюнкцияv (+)- "или";конъюнкция^ ( · , &) - "и";импликация→ (⊃) - "если... то";эквивалентность↔ (~) - "тогда и только тогда" (или "эквивалентно");неравнозначность⊕- "исключающее или" (сумма по модулю 2);штрих Шеффера|- "и-не";стрелка Пирса↓- "или-не";Примем соглашение о приоритете операций, упорядочив по убыванию: ¬, ^, v, →, ↔.Высказывания А и В называются равносильными, если на одинаковых наборахзначений переменных (атомарных высказываний), входящих в высказывание, значения этихвысказываний будут совпадать.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
