Автопрувер для алгебры множеств

[mihaild]

Ага, т.е. у нас есть сигнатура $L$, состоящая только из предикатных символов и формула $F$ в этой сигнатуре.
Мы добавляем семейства множеств в теорию множеств, и пишем терм $t$, который может быть оценен в $\top = \{\varnothing\}$ тогда и только тогда, когда $F$ выполнима (и каждой оценке предикатных символов из $L$ сопоставляется оценка нашего семейства).
Формуле $P(x_1, \ldots, x_n)$ сопоставляется $P_{x_1, \ldots, x_n}$.
Формуле $F \wedge G$ сопоставляется $\ulcorner F\urcorner \cap \ulcorner G\urcorner$.
Формуле $\neg F$ сопоставляется $\top \setminus \ulcorner F\urcorner$.
Формуле $\forall x: F(x)$ сопоставляется $\cap_x \ulcorner F(x)\urcorner$.

Тут надо еще немного помахать руками про то, что мы делаем, но в конечном итоге да, получается что вопрос о выполнимости формулы сводится к вопросу в исчислении предикатов сводится к вопросу о том, может ли терм в теории множеств с индексацией принимать данное значение.

[EminentVictorians]

mihaild, а можете расшифровать, какие это все имеет последствия для меня? Я просто не очень пока понял о чем речь.

[Padawan]

EminentVictorians
Да нет, под "теорией множеств" я и подразумевал те формулы, которые Вы хотите доказывать. Это алгоритмически не разрешимая задача. Если бы существовал алгоритм, устанавливающий истинность или ложность теоретико-множественного равенства с индексированными семействами множеств (как Вы хотите), то с помощью этого алгоритма можно было бы устанавливать общезначимость/не общезначимость формул ИП. А это не возможно.

-- Вт апр 18, 2023 19:57:10 --

EminentVictorians в сообщении #1589975 писал(а):

Грубо говоря, я ей кидаю на вход любую формулу из той статьи в википедии, и она говорит мне, правильная формула или нет.

Нет, не получится.

[EminentVictorians]

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

Да нет, под "теорией множеств" я и подразумевал те формулы, которые Вы хотите доказывать. Это алгоритмически не разрешимая задача. Если бы существовал алгоритм, устанавливающий истинность или ложность теоретико-множественного равенства с индексированными семействами множеств (как Вы хотите), то с помощью этого алгоритма можно было бы устанавливать общезначимость/не общезначимость формул ИП. А это не возможно.

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

Просто я подозреваю, если есть полуразрешимость, то все обычные, пригодные для восприятия человеком, формулы будут доказываться и так, причем за секунды. А если алгоритм не останавливается, то и фиг с ней, с этой формулой. С вероятностью 99% она ложная.

Собственно, я надеюсь, что все будет то же самое и по отношению к "формальной теории элементарной топологии". Вообще конечно интересно, насколько далеко получится продвинуться, используя такие методы.