Главная » Просмотр файлов » 18-19. Интуиционистская логика. Модальные логики

18-19. Интуиционистская логика. Модальные логики (1158030)

Файл №1158030 18-19. Интуиционистская логика. Модальные логики (В.А. Захаров - Лекции)18-19. Интуиционистская логика. Модальные логики (1158030)2019-09-18СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 18-19.Интуиционистская логика.Модальные логики.модальныелогикиy6интуиционистскаялогикаyI@yдругиелогическиеоперации@@другаятеориядоказательствсемантика@логических@связок@другиеформылогическоговывода@@yдругие кванторылогикивысших порядков@iспециальные интерпретации-КЛАССИЧЕСКАЯЛОГИКАyаксиоматическиетеорииИНТУИЦИОНИСТСКАЯ ЛОГИКАИнтуиционизм — это философское течение в математике,возникшее в начале 20 века как критический отклик нанеограниченное применение формальных логических методов вматематике, приводящее к парадоксам (антиномиям).По мнению интуиционистов (Брауэр, Вейль, Пуанкаре),парадоксы возникают в связи с тем, что законы логики,справедливые для конечных множеств, безосновательнопереносятся на бесконечные множества.Не все математические утверждения, верные для конечныхмножеств, остаются справедливыми и для бесконечныхмножеств.

Например, для конечных множеств верен принципАрхимеда «Часть всегда меньше целого», а длябесконечных множеств — нет.Вполне возможно, что не все законы классической(аристотелевой) логики допускают неограниченное ибезоговорочное использование в математике.ИНТУИЦИОНИСТСКАЯ ЛОГИКАНапример, рассмотрим одну широко распространенную схемудоказательства.Доказать: Если выполнены условия A, то ∃x P(x).Схема доказательства: Предположим противное, т. е.

∀x ¬P(x).Тогда ...(фа-фа, ля-ля)..., что противоречит условиям A.Значит, предположение ∀x ¬P(x) неверно, и поэтому ∃x P(x).QEDВсе хорошо, но где же та x, для которой верно P(x)?Из такого доказательства это значение извлечь невозможно.Но тогда, по мнению интуиционистов, это не доказательство, асловоблудие.Чтобы исключить доказательства такого рода, нужнопересмотреть семантику логических связок и кванторов.ИНТУИЦИОНИСТСКАЯ ЛОГИКАСемантика Колмогорова–Брауэра–ГейтингаПопробуем взглянуть на логические формулы как наутверждения о разрешимости математических задач.Каждая атомарная формула A будет обозначать некоторуюзадачу.

Истинность A будет означает, что задача имеетрешение, и это решение можно предъявить. Ложность A будетозначать, что задача решения не имеет.Логические связки позволяют конструировать из простыхзадач составные задачи.Оценим, как (не)разрешимость составных задач зависит от(не)разрешимости простых задач.ИНТУИЦИОНИСТСКАЯ ЛОГИКАСемантика Колмогорова–Брауэра–Гейтингаϕ & ψ:Решить обе задачи ϕ и ψ и предъявить решение;ϕ ∨ ψ:Выбрать одну из двух задач ϕ и ψ, решить выбранную задачу и предъявить решение;ϕ → ψ:Показать, что решение задачи ψ сводится к решению задачи ϕ, т.

е. предъявить способ, который позволяет, располагая решением задачи ϕ,построить решение задачи ψ;¬ ϕ:Доказать, что задача ϕ не имеет решения.Законами интуиционистской логики считаются только теформулы, которые соответствуют описаниям составных задач,имеющих решение при любых условиях.ИНТУИЦИОНИСТСКАЯ ЛОГИКАЗаконы интуиционистской логикиIP → P — каждую задачу можно свести к ней самой;I(P → Q)&(Q → R) → (P → R) — чтобы свести задача Rк задаче P достаточно найти задачу Q, к которой можносвести задачу R, и которую, в свою очередь, можно свестик задаче P;IP → ¬¬P — чтобы убедиться в том, что не существуетдоказательства неразрешимости задачи P, достаточнонайти решение задачи P;I(¬P ∨ ¬Q) → ¬(P&Q) — чтобы показать, что обе задачиP и Q нельзя решить одновременно, достаточно выбратьодну из этих задач и показать, что она неразрешима.ИНТУИЦИОНИСТСКАЯ ЛОГИКАФормулы, не являющиеся законамиинтуиционистской логикиI¬¬P → P — если вы можете обосновать, что нельзяпостроить доказательства неразрешимости задачи P, тоэтого еще недостаточно, чтобы получить решение самойзадачи P;IP ∨ ¬P — неправда, что для любой задачи можно либополучить решение, либо доказать, что никакого решенияне существует;I¬(P&Q) → (¬P ∨ ¬Q) — если можно доказать, что обезадачи P и Q нельзя решить одновременно, то это не даетоснования считать, что хотя бы одна из них являетсянеразрешимой.Да как же это так?Уж не скрывается ли здесь простая игра слов?ИНТУИЦИОНИСТСКАЯ ЛОГИКАПопробуем строго определить семантику утверждений,касающихся разрешимости задач.Истинность формул оценивается в интерпретациях.

Посколькузадачи решают люди, в качестве интерпретаций могутвыступать способности людей решать задачи.Но эти способности у людей со временем изменяются. Значит,интерпретации должны быть динамическими .Рассмотрим модель идеального математика (DutchMathematician), которыйIможет пребывать в разных состояниях знания ипереходить из одних состояний знания в другие;Iв каждом состоянии знания он точно знает, какие изэлементарных задач он умеет решать, а какие нет;Iне утрачивает навыков в решении задач при переходе изодного состояния знания в другое.ИНТУИЦИОНИСТСКАЯ ЛОГИКАОпределение (модель Крипке)Пусть P = {P1 , P2 , .

. . , Pn , . . . } — множество атомарныхформул (названия задач).Интуиционистская интерпретация — это реляционная системаI = hS, R, ξi, в которой1. S 6= ∅ — множество состояний (состояний знания);2. R ⊆ S × S — отношение переходов на S, которое являетсяотношением нестрогого частичного порядка:рефлексивноеR(s, s);транзитивноеR(s1 , s2 )&R(s2 , s3 ) ⇒ R(s1 , s3 );антисимметричное R(s1 , s2 )&R(s2 , s1 ) ⇒ s1 = s2 ;3. ξ : S × P → {true, false} — оценка атомарных формул,удовлетворяющая условию монотонности:R(s1 , s2 ) & ξ(P, s1 ) = true ⇒ ξ(P, s2 ) = true.ИНТУИЦИОНИСТСКАЯ ЛОГИКАПример интуиционистской интерпретации?ys1@@?s2y?s4y@?Rs@3 y @@@@@?Rs@6 y @@?s5yИНТУИЦИОНИСТСКАЯ ЛОГИКАПример интуиционистской интерпретации?s4y? P = falseутро ys1 Q = false@@@@@??s2Rs@y3 y @@@@@??s5Rs@y6 y ИНТУИЦИОНИСТСКАЯ ЛОГИКАПример интуиционистской интерпретации? P = falseys1 Q = false@@@@P = false@??s2 Q = falseRфирма PROGys@3 y @@@@@???s4s5Rs@yy6 y ИНТУИЦИОНИСТСКАЯ ЛОГИКАПример интуиционистской интерпретации? P = falseys1 Q = false@@@@P = false@??s2 Q = falseRs@y3 y @@@@P = false@???s4 Q = trues5Rs@yy6 y экзаменИНТУИЦИОНИСТСКАЯ ЛОГИКАПример интуиционистской интерпретации? P = falseys1 Q = false@@@@P = false P = true @??s2 Q = false Q = false s@Rлекцияy3 y @@@@P = false@???s4 Q = trues5Rs@yy6 y ИНТУИЦИОНИСТСКАЯ ЛОГИКАПример интуиционистской интерпретации? P = falseys1 Q = false@@@@P = false P = true @??s2 Q = false Q = false s@Ry3 y @@@@P = falseP = true@???s4 Q = trues5Rys@Q = falsey6 y экзаменИНТУИЦИОНИСТСКАЯ ЛОГИКАПример интуиционистской интерпретации? P = falseys1 Q = false@@@@P = false P = true @??s2 Q = false Q = false s@Ry3 y @@@@P = falseP = trueP = true @???s4 Q = trues5RyQ = falseQ = true s@y6 y экзаменИНТУИЦИОНИСТСКАЯ ЛОГИКАПример интуиционистской интерпретации? P = falseys1 Q = false@@@@P = false P = true @??s2 Q = false Q = false s@Ry3 y @@@@P = falseP = trueP = true @???s4 Q = trues5RyQ = falseQ = true s@y6 y ИНТУИЦИОНИСТСКАЯ ЛОГИКАОпределение (семантика Крипке)Пусть I = hS, R, ξi — интуиционистская интерпретация.

Тогдаотношение выполнимости I , s |=I ϕ формулы ϕ в состоянии sинтерпретации I определяется так:1. если ϕ = P ∈ P, то I , s |=I ϕ ⇐⇒ ξ(s, P) = true;2. I , s |=I ϕ1 &ϕ2 ⇐⇒ I , s |=I ϕ1 и I , s |=I ϕ2 ;3. I , s |=I ϕ1 ∨ ϕ2 ⇐⇒ I , s |=I ϕ1 или I , s |=I ϕ2 ;4. I , s |=I ϕ1 → ϕ2 ⇐⇒ для любого состояния s 0 , если(s, s 0 ) ∈ R и I , s 0 |=I ϕ1 , то I , s 0 |=I ϕ2 ;5. I , s |=I ¬ϕ1 ⇐⇒ для любого состояния s 0 , если(s, s 0 ) ∈ R, то I , s 0 6|=I ϕ1 .Формула ϕ называется интуиционистски общезначимой(законом интуиционистской логики), если для любойинтерпретации I и для любого состояния s верно I , s |=I ϕ.ИНТУИЦИОНИСТСКАЯ ЛОГИКАПример необщезначимой формулы6|=I P ∨ ¬PдискотекаP = false?вечерys1 ¬P = false@ P ∨ ¬P = false@@@P = false P = true @?? библиотекаs2 ¬P = true ¬P = false s@Ry3 y ИНТУИЦИОНИСТСКАЯ ЛОГИКАДругие необщезначимые формулыДокажите самостоятельно, выбрав подходящую интерпретацию(контрмодель) I ,6|=I ¬¬P → P6|=I ¬(P&Q) → (¬P ∨ ¬Q)6|=I ¬(P ∨ Q) → (¬P&¬Q)ИНТУИЦИОНИСТСКАЯ ЛОГИКАПример общезначимой формулы|=I P → ¬¬PОт противного.

Допустим, что I , s0 6|= P → ¬¬P. ТогдаP = true?ys0¬¬P = false¬P = trueP = falseP = true?ys1?ys2Полученное противоречие свидетельствует о невозможностипостроения контрмодели для формулы P → ¬¬P.ИНТУИЦИОНИСТСКАЯ ЛОГИКАДругие общезначимые формулыДокажите самостоятельно интуиционистскую общезначимостьследующих формул|=I ¬¬¬P → ¬P|=I (¬P ∨ ¬Q) → ¬(P&Q)|=I ¬P ∨ ¬¬PИНТУИЦИОНИСТСКАЯ ЛОГИКАНекоторые особенности интуиционистской логикиТеорема 1|=I ϕ =⇒ |=C ϕТеорема 2 (дизъюнктивное свойство)|=I ϕ ∨ ψ ⇐⇒ |=I ϕ или |=I ψТеорема 3 (экзистенциальное свойство)|=I ∀x1 . . .

∀x1 ∃y ϕ(x1 , . . . , xn , y )⇐⇒существует такой терм t(x1 , . . . , xn ), что|=I ϕ(x1 , . . . , xn , t(x1 , . . . , xn ))t(x1 , . . . , xn ) — это программа решения задачи ϕ.Это называется «изоморфизмом Карри–Ховарда».МОДАЛЬНЫЕ ЛОГИКИЗимой идет снегЗимой всегда идет снегЗимой иногда идет снегЭто разные высказывания. И поэтому они должны бытьзаписаны разными формулами.Эти высказывания по смыслу связаны друг с другом. И этодолжно быть отражено в формулах.

Поскольку высказыванияотличаются лишь словами всегда, иногда (модальностивремени ), нужно ввести какие-то логические конструкции длявыражения этих модальностей.Может быть для этой цели пригодны кванторы?МОДАЛЬНЫЕ ЛОГИКИСтуденты посещают лекцииСтуденты обязаны посещать лекцииСтуденты имеют право посещать лекцииобязан, имею право — деонтические модальности .А будут ли пригодны кванторы в этом случае для выражениямодальностей?МОДАЛЬНЫЕ ЛОГИКИЗадача имеет решениеИзвестно, что задача имеет решениеМожно допустить, что задача имеет решениезнаю, предполагаю — эпистемические модальности.А как быть здесь?МОДАЛЬНЫЕ ЛОГИКИМодальности (в естественном языке они, как правило,представлены наречиями или служебными глаголами)выражают различные оттенки истинности (уверенность,необходимость, доказуемость, осведомленность и др.).Эти оттенки можно классифицировать:Модальности необходимогонеобходимообязательновсегдадолжназнаюдоказуемоМодальности возможноговозможноне исключеноиногдаимею правопредполагаюнепротиворечиво♦МОДАЛЬНЫЕ ЛОГИКИСинтаксис модальных формулРасширим синтаксис классической логики предикатов, введядва логических оператора (модальность необходимого) и♦ (модальность возможного),при помощи которых разрешается строить формулыследующего вида:(ϕ)«необходимо ϕ»,(♦ϕ)«возможно ϕ».Во избежание большого количества скобок, будем считать, чтомодальные операторы имеют такой же приоритет, что икванторы.МОДАЛЬНЫЕ ЛОГИКИСемантика модальных формул многообразна и непроста.РассмотримПримерВерно ли, что формула ϕ → ϕ — это закон модальнойлогики?Если — модальность времени, «всегда», то ϕ → ϕ — этозакон модальной логики.Если студенты всегда ходят на лекции, то они ходят на лекции.А вот если — деонтическая модальность, «должны», тоформула ϕ → ϕ уже не может претендовать на статуслогического закона.Если студенты должны ходить на лекции, то они ходят на лекции.Это неправда, а законы логики не зависят от прихоти студентов.МОДАЛЬНЫЕ ЛОГИКИСемантика Крипке модальных формулОпределим самое общее отношение выполнимости длямодальных формул.Пусть P = {P1 , P2 , .

Характеристики

Тип файла
PDF-файл
Размер
548 Kb
Тип материала
Высшее учебное заведение

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций

В.А
6. Общая схема метода резолюций. Равносильные формулы. Теорема о равносильной замене. Предваренная нормальная форма. Сколемовская стандартная форма. Системы дизъюнкт.pdf
12. Хорновские логические программы - синтаксис. Декларативная семантика логических программ. Операционная семантика логических программ. SLD-резолютивные вычисления.pdf
17. Отрицание в логическом программировании. Оператор not. Встроенные предикаты и функции. Оператор вычисления значений. Модификация баз данных.pdf
20. Правильные программы. Императивные программы. Задача верификации программ. Логика Хоара. Автоматическая проверка правильности программ.pdf
21. Верификация распределённых программ. Логика линейного времени PLTL. Размеченные системы переходов. Задача верификации моделей программ.pdf
22. Задача верификации моделей программ. Подформулы Фишера-Ландера. Табличный метод верификации моделей программ. Алгоритм верификации моделей программ.pdf
23. Как устроена математика. Исчисление предикатов первого порядка. Аксиоматические теории. Элементарная геометрия. Теория множеств Цермело-Френкеля.pdf
Свежие статьи
Популярно сейчас
Почему делать на заказ в разы дороже, чем купить готовую учебную работу на СтудИзбе? Наши учебные работы продаются каждый год, тогда как большинство заказов выполняются с нуля. Найдите подходящий учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6374
Авторов
на СтудИзбе
309
Средний доход
с одного платного файла
Обучение Подробнее