Видеотека: Л. Д. Беклемишев, Что такое логика доказуемости?

ВИДЕОТЕКА


Летняя школа «Современная математика», 2013 21 июля 2013 г. 12:45, г. Дубна

Что такое логика доказуемости? Л. Д. Беклемишев
Аннотация: Классическая логика высказываний исходит из предположения о том, что любые высказывания либо истинны, либо ложны. Логика доказуемости отражает более глубокую картину мира, осознанную после теорем Гёделя о неполноте: истинность высказывания, вообще говоря, не равносильна его доказуемости. Можно ли – и если да, то как – говорить на уровне логики о доказуемости или недоказуемости высказываний, наряду с их истинностью или ложностью? Решение было, по существу, предложено ещё Гёделем, а потом эта область активно развивалась начиная с 60-х годов XX века. Язык логики доказуемости, наряду с обычными связками логики высказываний, содержит одноместные связки, обозначаемые $\Box$ и $\diamond$. При этом $\Box A$ выражает доказуемость высказывания $A$, а $\diamond A$ его непротиворечивость. Какие принципы логики доказуемости следует считать тавтологиями, то есть верными (подумайте: истинными или доказуемыми?) независимо от смысла элементарных высказываний, из которых они построены? Слушателям рекомендуется подумать, следует ли считать тавтологиями следующие примеры: $\Box A \mathbin{\&} \Box B \to \Box(A \mathbin{\&} 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$ Как можно описать множество всех тавтологий логики доказуемости? Есть ли алгоритм, распознающий тавтологичность? Для понимания рассказа будет полезно общее знакомство с теоремами Гёделя о неполноте и иметь представление о формальных системах, построенных на базе логики предикатов, таких как формальная арифметика Пеано. Разумеется, от слушателей НЕ требуется помнить многочисленные технические детали. Website: https://www.mccme.ru/dubna/2013/courses/ldb.htm