Разрешимость элементарной топологии

[Padawan]

Назовём элементарной теорией множеств, совокупность формул, записанных с участием переменных $A,B,C,\ldots$, обозначающих множества, символов логических связок, а также символов $=$, $\setminus$, $\cap$, $\cup$, $\subset$, $\supset$, $U$ (символ универсального множества), $\varnothing$.
Существует алгоритм, который, по любой такой формуле отвечает верна она всегда или нет.
Например, можно свести проверку к составлению таблицы истинности. Я выражаю существание такого алгоритма фразой "элементарная теория множеств разрешима" (пусть меня поправят, если что-то некорректно).

Рассмотрим теперь элементарную топологию. Так назовём совокупность, формул, записанных с участием переменных $A,B,C,\ldots$, обозначающих подмножества некоторого топологического пространства, символов логических связок, теоретико-множественных операций, символа $X$, обозначающего топологическое пространство, в котором всё происходит, а также символов $\overline \cdot$ (замыкание), $int$ (внутренность), $\partial$ (граница).
Существует ли алгоритм, который по любой такой формуле отвечает, верна она в общем случае или нет?

-- Пт апр 01, 2011 18:12:05 --

Например, верна ли формула $(A=int\, A)\to (int\,\partial A=\varnothing)$ ? Или, например, $(A\subset\partial A)\iff (int\, A=\varnothing)$ ?

[Munin]

Тут просто надо изобрести некоторый аналог таблицы истинности. Я его почти знаю: симплектические комплексы. Но это всё-таки для достаточно хорошей топологии.

[мат-ламер]

Ещё в семидесятых годах прошлого века компьютерная программа могла доказывать элементарные теоремы из общей топологии (используя, видимо, метод резолюций Робинсон). А вот с более сложными - проблема. В общей топологии, например, возникают определения и теоремы, связанные арифметикой кардинальных чисел. Там с разрешимостью сомнительно. Например, некоторые теоремы зависят от справедливости континуум-гипотезы. Наверное, надо грамотно определить границы Вашей элементарной топологии, например, записать основные аксиомы в виде логики предикатов первого порядка.

[Padawan]

мат-ламер
Границы элементарной топологии я определил -- это просто множество формул, построенных из символов, которые я перечислил. Формула называется истинной, если для любого топологического пространства $X$ и любых его подмножеств, $A,B,C,\ldots$ она оказывается справедливой. Вопрос в том и состоит, можно ли это проверить. Строго говоря является ли множество истинных формул рекурсивным (разрешимым).
Мне непонятно даже является ли оно рекурсивно-перечислимым, т.е. существует ли алгоритм, который может перечислять все истинные формулы.

[мат-ламер]

(Оффтоп)

Padavan. Я в этом не особо понимаю. По-моему вопрос относится к теории моделей. Возможно Профессор Снейп Вам поможет. Однако получается очень бедная теория. Даже нет понятия точки.

[Padawan]

Куратовский показал, что из множества $A$ при помощи операций замыкания и перехода к дополнению можно получить не более, чем 14 различных множеств. А если еще разрешить использовать операцию пересечения? То сколько получится? Бесконечно поди?

[Munin]

Padawan в сообщении #430250 писал(а):

А если еще разрешить использовать операцию пересечения? То сколько получится? Бесконечно поди?

Если из того же одного множества, то вряд ли более чем те же 14.

[Padawan]

Munin в сообщении #430409 писал(а):

Если из того же одного множества, то вряд ли более чем те же 14.

Можно бесконечно.

Ответ на вопрос в стартовом сообщении -- да, алгоритм существует, но он очень трудоемкий, современные компьютеры не потянут, слишком большой перебор. Хотя если как-то модернизировать-оптимизировать, то может и выйдет. Если кому интересно, напишите в тему, распишу подробнее. Ответ узнал из этой статьи.

Усложним задачу. Пусть теперь можно навешивать кванторы на переменные, обозначающие множества.

[Профессор Снэйп]

мат-ламер в сообщении #430104 писал(а):

Возможно Профессор Снейп Вам поможет.

Я только сейчас увидел тему.

По поводу терминологии. Элементарная теория - это когда с кванторами. Устоявшийся термин

Ну а по сути сказать пока ничего не могу