Документ взят из кэша поисковой машины. Адрес оригинального документа : http://www.mccme.ru/dubna/2013/courses/ldb.htm
Дата изменения: Tue Jul 23 12:05:28 2013
Дата индексирования: Fri Feb 28 00:30:19 2014
Кодировка: UTF-8
Поисковые слова: п п п п п п п п п п п п п п п п п п п п п п п п п п
Dubna-2013: Beklemishev
На главную страницу ЛШСМ-2013 К списку курсов ЛШСМ-2013

Лев Дмитриевич Беклемишев

Что такое логика доказуемости?

Л.Д.Беклемишев планирует прочитать одну лекцию

Классическая логика высказываний исходит из предположения о том, что любые высказывания либо истинны, либо ложны. Логика доказуемости отражает более глубокую картину мира, осознанную после теорем Геделя о неполноте: истинность высказывания, вообще говоря, не равносильна его доказуемости. Можно ли - и если да, то как - говорить на уровне логики о доказуемости или недоказуемости высказываний, наряду с их истинностью или ложностью? Решение было, по существу, предложено еще Геделем, а потом эта область активно развивалась начиная с 60-х годов XX века.

Язык логики доказуемости, наряду с обычными связками логики высказываний, содержит одноместные связки, обозначаемые ? и ?. При этом ? A выражает доказуемость высказывания A, а ? A его непротиворечивость. Какие принципы логики доказуемости следует считать тавтологиями, то есть верными (подумайте: истинными или доказуемыми?) независимо от смысла элементарных высказываний, из которых они построены?

Слушателям рекомендуется подумать, следует ли считать тавтологиями следующие примеры:
? A & ? B ? ?(A & B)
? (A ? B) ? ? A ? ? B
? A ? ?? A
? A ? ? ? A
? A ? A
Как можно описать множество всех тавтологий логики доказуемости? Есть ли алгоритм, распознающий тавтологичность?

Для понимания рассказа будет полезно общее знакомство с теоремами Геделя о неполноте и иметь представление о формальных системах, построенных на базе логики предикатов, таких как формальная арифметика Пеано. Разумеется, от слушателей НЕ требуется помнить многочисленные технические детали.

Материалы