1 1 27.11.2015 Введение в математическую логику и теорию алгоритмов Алексей Львович Семенов Лекция 10.

Презентация:



Advertisements
Похожие презентации
Как устроена математическая логика Алексей Львович Семенов.
Advertisements

Введение в формальные (аксиоматические) системы. Формальные системы - это системы операций над объектами, понимаемыми как последовательность символов.
Введение в математическую логику и теорию алгоритмов Лекция 14 Алексей Львович Семенов.
Введение в математическую логику и теорию алгоритмов Лекция 3 Алексей Львович Семенов.
Введение в математическую логику и теорию алгоритмов Алексей Львович Семенов Лекция 16.
Введение в математическую логику и теорию алгоритмов Алексей Львович Семенов Лекция 5.
{ формальные языки - формальные исчисления - теоремы формального исчисления - выводимость в формальном исчислении - свойства выводимости из посылок - формальный.
Логика первого порядка ХНУРЭ, кафедра ПО ЭВМ, Тел , Лекции Н.В. Белоус Факультет компьютерных наук Кафедра.
Логика первого порядка ХНУРЭ, кафедра ПО ЭВМ, Тел , Лекции Н.В. Белоус Факультет компьютерных наук Кафедра.
Математическая логика и теория алгоритмов формальной теории исчисления Одним из основных понятий математической логики является понятие формальной теории.
1 Кубенский А.А. Дискретная математика. Глава 2. Элементы математической логики Исчисление высказываний Высказывание – утверждение о математических.
Введение в теорию множеств. Введение в теорию множеств 1. Основные определения, терминология Под множеством А мы понимаем совокупность объектов произвольной.
Введение в математическую логику и теорию алгоритмов Алексей Львович Семенов Лекция 9.
Кафедра математики и моделирования Старшие преподаватели Е.Д. Емцева и Е.Г. Гусев Курс «Высшая математика» Лекция 4. Тема: Множество. Операции над множествами.
ФУНКЦИОНАЛЬНЫЙ АНАЛИЗ Составила: М.П. Филиппова доцент кафедры высшей математики ИМИ СВФУ.
Введение в математическую логику и теорию алгоритмов Лекция 2 Алексей Львович Семенов.
Введение в математическую логику и теорию алгоритмов Лекция 2 Алексей Львович Семенов.
Введение в математическую логику и теорию алгоритмов Алексей Львович Семенов Лекция 8.
Введение в математическую логику и теорию алгоритмов Алексей Львович Семенов Лекция 9.
Введение в теорию множеств 1. Основные определения, терминология Под множеством А мы понимаем совокупность объектов произвольной природы, объединенных.
Транксрипт:

Введение в математическую логику и теорию алгоритмов Алексей Львович Семенов Лекция 10

22 План Программа Гильберта Непротиворечивая и полная математика. Логика отношений Исчисление логики отношений Исчисления Породимые множества Грамматики. Тезис Поста

33 Программа Гильберта Построение непротиворечивой и полной математики –Построение аксиоматической теории – исчисления («игры») –Доказательство непротиворечивости и полноты «надежными», «финитными» средствами (анализом «игры»)

4 Логика отношений Синтаксис: Индуктивное построение формул Семантика: Интерпретации

5 Множество D Отношения – подмножества D N Конечное число аргументов Имена отношений, Зн Свободные переменные x 1,… Задача. Формулы R(x) и Q(x) эквивалентны в структуре M т. е. M R(x) Q(x) тетки значения R(x) и Q(x) (отношения в D N ) совпадают. О. Формулы эквивалентны, если они эквивалентны в любой структуре (данной сигнатуры). Отношения, задаваемые формулами логики отношений (Семантика)

6 Предваренная нормальная форма Формула находится в предваренной нормальной форме (п.н.ф.), если она не содержит кванторов, или имеет вид: Q 1 x 1 … Q n x n Ф, где все Q i – это или, а в Ф кванторов нет. Задача. Дать индуктивное определение формулы (находящейся) в п.н.ф. Задача. Построить алгоритм, который по всякой формуле логики отношений строит формулу (находящуюся) в п.н.ф., ей эквивалентную (ее предваренную нормальную форму). Можно переименовывать связанные переменные…

Предваренная нормальная форма ( u [u/x]) ( v [v/x]) (Qu [u/x]) (Qu ( [u/x] )),,, Q,, не содержит u ( ( u [u/x])) ( v [v/x]) 7

8 Теоремы о логике отношений Теорема перечислимости. Множество общезначимых формул перечислимо: есть процесс деятельности, позволяющий для всякой общезначимой формулы когда-нибудь узнать, что она общезначима. Теорема компактности для счетного множества утверждений. Если любое конечное подмножество теории имеет модель, то и вся теория имеет модель. Задача. Как обстоит дело с общезначимыми и с необщезначимыми формулами в логике высказываний? 8

9 Исчисление для логики отношений (дедуктика) Будет указано индуктивное определение выводимой формулы, формализующее практику математических доказательств. 9

10 Частные случаи тавтологий логики высказываний в логике отношений Возьмем тавтологию логики высказываний, например: А 1 (А 2 А 1 ).(*) Подставим в (*) вместо имен высказываний А 1 и А 2 формулы (замкнутые или незамкнутые) логики отношений. Например, вместо А 1 подставим u 1 (P 5 (u 1 )), а вместо А 2 подставим P 4 (x 1,x 1 ): u 1 (P 5 (u 1 )) ( P 4 (x 1,x 1 ) u 1 (P 5 (u 1 )) ). То, что получилось, называется частным случаем тавтологии (*) логики высказываний в логике отношений. Любая такая формула истинна в любой структуре при любой интерпретации. Вместо «частный случай тавтологии…» говорим просто «тавтология».

11 Исчисление логики отношений Фиксируем сигнатуру =. Исчисление (одно для данной сигнатуры) задаётся аксиомами (являющимися формулами сигнатуры ) и правилами вывода. Аксиомы: A1. частные случаи тавтологий логики высказываний, A2. формулы вида u [u/x] [t/x], A3. формулы вида [t/x] u [u/x], где – формула, x – свободная переменная (x FVar), u – связанная переменная (u BVar), не входящая в, t – свободная переменная.

12 Исчисление логики отношений Правила вывода: R1 (modus ponens, (MP)) R2 R3 В R2, R3 x не входит в. Правила R2 и R3 называются правилами Бернайса., u [u/x] u [u/x] Индуктивное определение выводимой формулы: Аксиомы выводимы. Если уже выведены формулы, написанные в верхней части правила, то написанная внизу формула - выводима. Говорят, что она выводима из них.

13 Примеры выводов Вывод – цепочка формул, где каждая формула – аксиома или выводима из предшествующих в цепочке. Пример 1. (1) u P(x) [u/x] P(x) [x/x] (аксиома A2) u P(u) P(x) (аксиома A2) (2) u P(u) v P(v) (по правилу R2 из (1)) (В этом выводе P – имя одноместного отношения.) Пример 2. Пусть - любая формула в нашей сигнатуре. (1) ( u [u/x] ) (( u [u/x]) ( u [u/x] u [u/x])) (Частный случай тавтологии (A B) ((B C) (A C)). ) (2) u [u/x] (A2, – это [ x/x ]) (3) ( u [u/x]) ( u [u/x] u [u/x]) (по MP из (2) и (1)) (4) u [u/x](A3) (5) u [u/x] u [u/x](по MP из (4) и (3))

14 Пример вывода Пример 3. (Используем обычное обозначение для двуместного отношения «меньше или равно».) (1) u (uy) xy (A2, терм t = x) (2) xy v (xv) (A3, терм t = y) (3) ( u (uy) xy ) ( ( xy v (xv) ) ( u (uy) v (xv) ) ) (частный случай тавтологии (A B) ( (B C) (A C) ) ) (4) (xy v (xv)) ( u (uy) v (xv)) (по MP из (1) и (3)) (5) u (uy) v (xv) (по MP из (2) и (4)) (6) u (uy) u v (uv) (по R2 из (5)) (7) v u (uv) u v (uv) (по R3 из (6)) Заметим, что полученная формула – общезначима.

15 Истинность выводимого Теорема об истинности выводимого. Всякая выводимая формула является общезначимой. Структура доказательства (индукция по построению). A1 Частные случаи тавтологий логики высказываний – общезначимы. A2 Формулы вида u [ u/x ] [ t / x] – общезначимы. A3 Формулы вида [ t / x] u [ u/x ] – общезначимы. R1 Если формулы и общезначимы, то формула – общезначима. R2 Если формула общезначима и не содержит x, то формула u [ u/x ] – общезначима. R3 Если формула общезначима и не содержит x, то формула u [ u/x ] – общезначима. Доказательство рассматривает определение истинности, значения на последовательности, и т. д.

16 Выводимость истинного Теорема Гёделя о полноте. Общезначимость в логике отношений совпадает с выводимостью в исчислении логики отношений. Теорема в курсе не доказывается Задача. Доказать теорему. Решение – не обязательно. 16

17 Цепочка = конечная последовательность, которая может быть и пустой – Λ. Длина цепочки – число элементов в ней. Алфавит = конечная цепочка символов Слово (в данном алфавите) – цепочка символов этого алфавита. Ансамбль слов в данном алфавите – все слова. Часто: 0 1 Ансамбль цепочек слов в данном алфавите – все цепочки слов. Ансамбль списков в данном алфавите – все цепочки, элементами которых являются слова или списки (индуктивное определение). Задача. Дать подробные индуктивные определения для понятий с этого экрана. Общее понятие исчисления. Предварительные определения

Действия и проверки. Описания Действие – исходное понятие. Действие: Слово, являющееся текстом (цепочкой) на понятном человеку языке; Его можно применить к любому исходному данному из фиксированного ансамбля, при этом ясно, что всегда получается результат применения – элемент (возможно, другого) фиксированного ансамбля Оно может применяться, выполняться и человеком, и каким-то устройством, Действие – задает всюду определенную функцию Проверка – действие с результатом 0 или 1 Проверка задает характеристическую функцию множества (где она дает 1), мы говорим, что она допускает его элементы (а другие – не допускает) 18

19 Исчисления. Создаваемые объекты Исчисление в данном ансамбле – это пара из двух проверок:. проверка возможности (создания) применяется к цепочке объектов, проверка завершения (окончания)– к объекту. создаваемый исчислением объект индуктивно определяется так: Если проверка возможности допускает цепочку объектов a 1,… a n и все элементы этой цепочки, кроме последнего – создаваемы, то и последний элемент создаваем. Если проверка возможности допускает цепочку из одного элемента, то его называют начальным объектом (в некоторых контекстах – аксиомой). Задача. Что, если таких у данного исчисления нет? Общее представление о деятельности, использующей уже имеющиеся условия.

20 Объект порождаем данным исчислением, если он создаваем и его допускает проверка завершения. Исчисление порождает множество из всех порождаемых им объектов – множество, порождаемое этим исчислением. Породимое множество – множество, порождаемое каким-то исчислением. Эмиль Пост ( ) Исчисления. Породимые множества

21 Фиксируем исчисление. Если a 1, …, a n – допускается проверкой возможности, то говорим. что a n создается из a 1, …, a n-1 (в данном исчислении). Вывод объекта a – цепочка объектов S, каждый из которых создается из какой-то цепочки объектов, встретившихся в S раньше него. Шаг вывода – добавление одного элемента в цепочку Задача. Объект создаваем тогда и только тогда, когда у него имеется вывод. Задача. Пусть дано исчисление. Как организовать процесс выписывания всех выводов? Задача. Пусть дано исчисление. Как организовать процесс выписывания всех порождаемых (в нем) объектов (и только их)? Вывод

Примеры Почему исчисление К модальной логики – это исчисление? Проверка возможности допускает: Цепочки из одной формулы (аксиомы) –Тавтологии –Все формулы (A B) ( A B ). Цепочки из двух формул. Цепочки из трех формул. Проверка завершения Все подходит. Задача. Описать все проверки подробно. Задача. Почему определение формулы – это исчисление.

23 Т. Объединение и пересечение по родимых множеств породимы. Д. Объединение. А:, Б:. Идея: Создаем слова, следуя Проверке А и следуя Проверке Б, Берем то, что создано или по той или по другой проверке. Проблема: как не перемешивать «по ходу дела» проверки А и Б? Выход: Метки для объектов, создаваемых по разным проверкам: Аx, Бy. Считаем, что символы А и Б в алфавит исчисления не входят. Теоремы замкнутости для исчислений

24 Припишем ко всем элементам цепочки, входящей в ту или иную Проверку возможности, в начале символы А или Б. Объединим полученные проверки. Проверка возможности допускает еще все пары, где проверка завершения А допускает x, и пары, где проверка завершения Б допускает x. Задача. Проверка завершения ? Задача. Почему пересечение (конъюнкция) проверок – проверка? Задача. Доказать теорему для пересечения. Задача. Как обстоит дело с дополнением? Продолжение. Породимость объединения

Грамматики (Ноам Хомски, ) Определение. Грамматика Γ – это цепочка Σ – основной алфавит Γ Ω – вспомогательный алфавит Γ S – начальный символ Γ, S Ω ΣΩ=Ø, объединение Σ и Ω – это алфавит Γ, обозначим его Δ. Π – это конечное множество пар слов в алфавите Δ. Эти пары называются заменами.

Грамматика определяет исчисление Γ* Проверка возможности Γ* допускает: S –Всякий вывод в исчислении начинается с S. Для каждой замены из Π все пары вида, где t,p – произвольные слова в алфавите Δ –Один шаг вывода состоит в замене в слове некоторого входящего в него u на v. Проверка завершения для грамматики Γ допускает все слова в алфавите Σ. –Порождаемые слова не могут содержать букв из вспомогательного алфавита. Описание грамматики – слово в конечном алфавите.

27 Примеры грамматик В них, следуя традиции, и для наглядности, используется символ стрелочки в заменах и выводах. Задача. Как породить все цепочки из 0 и 1? Решение. Г = Σ, Ω, П, S, о сновной алфавит Σ = {0, 1}, вспомогательный алфавит Ω = { S }, П = { S S 0, S S 1, S Λ }. Пример вывода: S S 0 S 10 S 010 S Задача. Как породить все десятичные числа? (Пример десятичного числа: ) Как породить все свободные переменные логики отношений? Задача. Что делает грамматика с основным алфавитом {a}, вспомогательным {S, B, M, E} и заменами П = {S BaE, B BM, Ma aaM, ME E, B Λ, E Λ } ? Задача. Построить грамматику порождающую все слова, состоящие из одинакового количества букв a и b ? Задача. Построить множество, которое породить грамматикой нельзя.

Тезис Поста (вариант). Всякое породимое множество порождается некоторой грамматикой. Соответствие между интеллектуальной реальностью и теоретико-множественной математикой