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

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

Л. Д. Беклемишев планирует провести 4 занятия.

Доступны 4 видеозаписи курса.

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

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

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

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

Примерная программа

1. 1. Логика высказываний и её модели. Модальная логика, модели Крипке. Логика Гёделя-Лёба GL. Теорема о полноте логики GL по Крипке на конечных деревьях.
2. 2. Формальная арифметика Пеано. Гёделева нумерация. Теорема о неподвижной точке. Формулы доказуемости и непротиворечивости. Теоремы Гёделя, Россера и Лёба.
3. 3. Доказуемость как модальность: арифметическая интерпретация логики GL. Применения: замкнутые модальные формулы, последовательность Тьюринга, локальная рефлексия (Артёмов-Булос, Горячев).
4. 4. Существование и единственность модально определимых неподвижных точек (теорема де Йонга).

Organization Committee e-mail:
dubna@mccme.ru