Видеотека: Л. Д. Беклемишев, Алгебра доказуемости и разреженная топология

ВИДЕОТЕКА


Традиционная новогодняя сессия МИАН-ПОМИ, 2009 «Логика и теоретическая информатика» 17 декабря 2009 г. 12:50, г. Москва

Алгебра доказуемости и разреженная топология Л. Д. Беклемишев
Аннотация: В докладе рассмотрены два класса объектов, имеющих различную природу, но неожиданным образом аналогичные по своим свойствам. С одной стороны, так называемые алгебры доказуемости, возникающие при изучении свойств формальной доказуемости в арифметических теориях. С другой стороны, топологические пространства, наделённые одной или несколькими разреженными топологиями, то есть такими, что любое непустое подмножество $X$ имеет хотя бы одну изолированную точку. Алгебра доказуемости формальной арифметической теории $T$ представляет собой булеву алгебру Линденбаума для $T$, расширенную оператором $D_0\colon L\to L$, сопоставляющим любому предложению $A$ гёделевское предложение, выражающее непротиворечивость теории $T+A$. Ее естественным обобщением является алгебра, в которой наряду с оператором $D_0$ рассматриваются операторы $n$-непротиворечивости $D_n$, выражающие истинность всех доказуемых в $T+A$ предложений с $n$ переменами кванторов. Операторы $D_0, D_1, \dots$ могут интерпретироваться как операторы на алгебре всех подмножеств данного множества $X$. Оказывается, что в случае, когда на алгебре множеств выполнены все тождества алгебры доказуемости, каждый из этих операторов естественным образом определяет некоторую разреженную топологию на $X$, для которой $D_n(A)$ есть множество всех предельных точек множества $A$. В докладе рассмотрены свойства соответствующих политопологических пространств и их связи с вопросами из теории доказательств, в частности вопрос о полноте топологических пространств относительно системы тождеств алгебр доказуемости.