RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ЛИЧНЫЙ КАБИНЕТ
Видеотека
Архив
Популярное видео

Поиск
RSS
Новые поступления





Для просмотра файлов Вам могут потребоваться






Летняя школа «Современная математика», 2016
27 июля 2016 г. 11:15, г. Дубна, дом отдыха «Ратмино»
 


Доказуемость и модальная логика. Занятие 4

Л. Д. Беклемишев
Видеозаписи:
Flash Video 518.2 Mb
Flash Video 3,105.0 Mb
MP4 518.2 Mb

Количество просмотров:
Эта страница:157
Видеофайлы:76

Л. Д. Беклемишев


Видео не загружается в Ваш браузер:
  1. Установите Adobe Flash Player    

  2. Проверьте с Вашим администратором, что из Вашей сети разрешены исходящие соединения на порт 8080
  3. Сообщите администратору портала о данной ошибке

Аннотация: Классическая логика высказываний исходит из предположения о том, что любые высказывания либо истинны, либо ложны. Логика доказуемости отражает более глубокую картину мира, осознанную после теорем Гёделя о неполноте: истинность высказывания, вообще говоря, не равносильна его доказуемости. Можно ли — и если да, то как — говорить на уровне логики о доказуемости или недоказуемости высказываний, наряду с их истинностью или ложностью? Решение было, по существу, предложено ещё Гёделем, а потом эта область активно развивалась начиная с 60-х годов XX века.
Язык логики доказуемости, наряду с обычными связками логики высказываний, содержит одноместные связки, обозначаемые $\square$ и $\lozenge$. При этом $\square$ A выражает доказуемость высказывания A, а $\lozenge$ A его непротиворечивость. Какие принципы логики доказуемости следует считать тавтологиями, то есть верными (подумайте: истинными или доказуемыми?) независимо от смысла элементарных высказываний, из которых они построены?
Слушателям рекомендуется подумать, следует ли считать тавтологиями следующие примеры:
$\Box \; A \; & \; \Box \; B \to \Box(A \;&\;B)$
$\Box \; (A \vee B) \to \Box \; A \vee \Box \; B$
$\Box \; A \to \Box\Box \; A$
$\Diamond \; A \to \Box \; \Diamond \; A$
$\Box \; A \to A$
Как можно описать множество всех тавтологий логики доказуемости? Есть ли алгоритм, распознающий тавтологичность?
Для понимания рассказа будет полезно общее знакомство с теоремами Гёделя о неполноте и иметь представление о формальных системах, построенных на базе логики предикатов, таких как формальная арифметика Пеано. Разумеется, от слушателей не требуется помнить многочисленные технические детали.
Примерная программа
  • Логика высказываний и её модели. Модальная логика, модели Крипке. Логика Гёделя-Лёба GL. Теорема о полноте логики GL по Крипке на конечных деревьях.
  • Формальная арифметика Пеано. Гёделева нумерация. Теорема о неподвижной точке. Формулы доказуемости и непротиворечивости. Теоремы Гёделя, Россера и Лёба.
  • Доказуемость как модальность: арифметическая интерпретация логики GL. Применения: замкнутые модальные формулы, последовательность Тьюринга, локальная рефлексия (Артёмов-Булос, Горячев).
  • Существование и единственность модально определимых неподвижных точек (теорема де Йонга).


Website: http://www.mccme.ru/dubna/2016/courses/beklemishev.html
Цикл лекций

ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru
 
Обратная связь:
 Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2018