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

[EminentVictorians]

Последнее время заинтересовался компьютерной проверкой доказательств. Я решил взять маленькую, но, как мне кажется, самодостаточную часть - алгебру множеств. Как известно, есть определенное количество операций над множествами, которые разным образом связаны друг с другом. Эти связи можно записать в виде различных соотношений. Например, можно взять такое

$$\bigcup\limits_{i \in I}^{}\bigcap\limits_{j \in J}^{}S_{i,j}\subset\bigcap\limits_{j \in J}^{}\bigcup\limits_{i \in I}^{}S_{i,j}$$

(просто оно мне нравится, поэтому я его и взял). Я хочу акцентировать, что я допускаю подобные "сложные" формулы, а не просто бинарные в духе $A \cup B = B \cup A$. Есть хорошая статья в википедии List of set identities and relations, чтобы было представление, какие формулы я имею в виду.

Так вот. Мой план максимум - сделать компьютерную программу. Программа должна уметь следующее:

1. В ней должен быть механизм определения операции. Т.е. чтобы можно было определить операции объединения, пересечения, декартова произведения, разности и т.д. Хотелось бы, чтобы механизм был универсальный и чтобы можно было определять любые операции, какие вздумается. Ну я не знаю, допустим 10-арную операцию $\circ_{i = 1}^{10} A_i = (\bigcap\limits_{i = 1}^{9}A_i) \triangle A_{10}$ (где $\triangle$ - симметрическая разность). Думаю, что у меня получилось написать достаточно абсурдную операцию, чтобы показать, что я хочу.

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

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

[пианист]

https://en.wikipedia.org/wiki/Thomas_Callister_Hales
https://ru.wikipedia.org/wiki/Agda
https://ru.wikipedia.org/wiki/Coq

[mihaild]

Чем это отличается от булевых формул?
Если, как мне кажется, ничем, то проверка их общезначимости - классическая NP-полная задача SAT, создание солверов для которой - довольно большая область. Начать обзор можно хоть с википедии.
(но это гораздо более простая задача, чем доказательство произвольных формул в исчислении предикатов)

[EminentVictorians]

Мне тоже кажется, что все сводится к SAT. Правильно ли я понимаю, что если я захочу практически проверить те формулы из статьи в википедии про алгебру множеств, то любой, даже самый тупой SAT-солвер (без всяких эвристик и примочек), будет щелкать их как орешки? Ну т.е. NP-полнота будет сказываться только на формулах с миллионами переменных, а не на тех обычных тождествах с множествами, помещающихся в одну строчку.

[Sender]

В общем, да. В принципе, можно подобрать примеры с сотнями переменных, которые поставят в тупик любой солвер, но такие случаи сравнительно редки.

[Padawan]

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

Например, можно взять такое

$$\bigcup\limits_{i \in I}^{}\bigcap\limits_{j \in J}^{}S_{i,j}\subset\bigcap\limits_{j \in J}^{}\bigcup\limits_{i \in I}^{}S_{i,j}$$

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

-- Вт апр 18, 2023 10:06:51 --

Вот, кстати, моя похожая тема, связанная с доказательством формул общей топологии Разрешимость элементарной топологии

[EminentVictorians]

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

Если Вы допускаете такие формулы с бесконечным проиндексированным семейством множеств

А знаете, почему я их допускаю? Я недавно открывал книжку Виро и др. по общей топологии. Там в параграфе про базы вводятся предбазы. И есть теорема, что если у нас есть предбаза $\Delta$ некоторой топологии $\Omega$ на $X$, то объединение элементов предбазы даст $X$. Ну и я начинаю доказывать: (будем считать $X$ нетривиальным топологическим пространством, т.е. $X \ne \varnothing$)

$$X \in \Omega \Rightarrow X = \bigcup\limits_{i \in I}^{}B_i = \bigcup\limits_{i \in I}^{} \bigcap\limits_{j = 1}^{k_i} D_{ij} = \bigcap\limits_{f \in \prod\limits_{i \in I}^{}J_i}^{} (\bigcup\limits_{i \in I}^{}D_{i, f(i)}) \quad \subset \quad \bigcup\limits_{i \in I}^{}D_{i, f(i)} \quad \subset \quad \bigcup\limits_{D \in \Delta}^{}D \Rightarrow X = \bigcup\limits_{D \in \Delta}^{}D $$

А в процессе ловлю себя на мысли: "Какой же фигней я занимаюсь. Это все должно делаться автоматически, а не руками". Вот у меня и возникала мысль сделать формальную теорию элементарной топологии. Грубо говоря, я хотел теорию, гораздо более бедную, чем, например, $ZFC$, но разрешимую, и чтобы в ней можно было бы сформулировать простейшие теоремы общей топологии, которые не завязаны на конкретные структуры типа $\mathbb R$. А для начала решил сделать подобное с теорией множеств.

Но вообще, я конечно подофигел, увидев Вашу тему)) Странное ощущение - читаю как-будто свою тему из будущего, а рядом дата - 2011 год...

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

то доказательство таких формул равносильно доказательству формул исчисления предикатов (объединение - существует, пересечение - для любого),

Я довольно сильно уверен, что это не так. Но это пока на уровне интуиции.

[Padawan]

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

Я довольно сильно уверен, что это не так. Но это пока на уровне интуиции.

Равносильно, равносильно. Любую формулу теории множеств можно переделать в формулу исчисления предикатов и наоборот. Напишите какую-нибудь, я переделаю из одного в другое. И общезначимость одной равносильна тождественной истинности другой.

-- Вт апр 18, 2023 17:46:44 --

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

$\bigcup\limits_{i \in I}^{} \bigcap\limits_{j = 1}^{k_i} D_{ij} = \bigcap\limits_{f \in \prod\limits_{i \in I}^{}J_i}^{} (\bigcup\limits_{i \in I}^{}D_{i, f(i)})$

Вот это, да, прикольно.
Функции Сколема в исчислении предикатов как раз отсюда и возникают.

[mihaild]

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

Любую формулу теории множеств можно переделать в формулу исчисления предикатов и наоборот

Наоборот даже переделывать ничего не нужно, формула теории множеств уже в исчислении предикатов.
А в прямую сторону - речь вроде о формулах, в которых есть объединение и пересечение по произвольному множеству, ну и наверное разность, кванторов нет. Понятно что будем предикаты кодировать множествами (а без констант и функциональных символов можно обойтись), но я не очень представляю, как это к равенству сводить.
Ну т.е. например формула в сигнатуре $(e, \cdot, =)$:

$$[(\forall x \exists y: xy = e) \wedge (\forall x: ex = xe = x) \wedge (\forall x \forall y \forall z: ((xy)z) = (x(yz)))] \rightarrow \forall x \exists y \forall z: (xy = yx = e \wedge xz = e \rightarrow z = y)$$

(ассоциативность, нейтральность единицы и правого обратного влекут единственность правого обратного и совпадение его с левым обратным). Как это к множествам без кванторов сводить?

[Padawan]

Давайте в сигнатуре будут только предикаты.

[mihaild]

$\cdot$ имеет валентность $3$, $=$ имеет валентность $2$, для равенства нужно еще в посылку добавить аксиомы для ну допустим всех формул не длиннее 20 символов.

$$ \forall x \forall y \exists z: \cdot(x, y, z) \wedge \forall x \forall y \forall z_1 \forall z_2: (\cdot(x, y, z_1) \wedge\cdot(x, y, z_2) \rightarrow =(z_1, z_2)) \wedge \exists e: [ \quad[ \quad\quad(\forall x \exists y: \cdot(x, y, e)) \wedge \quad\quad (\forall x: \cdot(x, e, x) \wedge \cdot(e, x, x)) \wedge \quad\quad (\forall x \forall y \forall z \forall a \forall b \forall c \forall d: (\cdot(x, y, a) \wedge \cdot(a, z, b) \wedge \cdot(y, z, c) \wedge \cdot(x, c, d) \rightarrow =(b, d))) \quad] \rightarrow \quad\quad \forall x \exists y \forall z: (\cdot (x, y, e) \wedge \cdot (y, x, e) \wedge (\cdot(x, z, e) \rightarrow =(y, z))) ]$$

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

[Padawan]

Просто $\forall x\exists y P(x, y) $ заменяем на $\bigcap_{x}\bigcup_y P_{x, y}$, где $P_{x, y}$ -- проиндексированное семейство множеств $\to$ заменяем на $\subset$.

[mihaild]

А что идейно содержат множества $P_{x, y}$? Ничего, если предикат не выполнен, и что-то фиксированное, если выполнен?

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

$\to$ заменяем на $\subset$

Но ведь стрелок в формуле может быть много, а $\subset$ максимум одно.

[Padawan]

mihaild в сообщении #1590136 писал(а):

Но ведь стрелок в формуле может быть много, а $\subset$ максимум одно.

Хм. Вы правы. Но, мне кажется, что можно выкрутиться.

-- Вт апр 18, 2023 18:51:29 --

А, ну просто заменим $P\to Q$ на $cP\cup Q$, где $c$ - это дополнение.

-- Вт апр 18, 2023 18:57:05 --

mihaild в сообщении #1590136 писал(а):

А что идейно содержат множества $P_{x, y}$? Ничего, если предикат не выполнен, и что-то фиксированное, если выполнен?

Содержат что-то фиксированное, если выполнен, и не содержат это фиксированное, если не выполнен.

[EminentVictorians]

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

Любую формулу теории множеств можно переделать в формулу исчисления предикатов и наоборот.

У меня в любом случае не полноценная теория множеств, а просто "алгебра множеств". Она же гораздо беднее любой теории множеств, поэтому у меня есть надежда, что она разрешима.