Общая теория нотаций

[Anton_Peplov]

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

Anton_Peplov в сообщении #1592476 писал(а):

Рискну предположить, что такие "нотируемые" области это скорее исключение, чем правило.

Мне так не кажется. Я думаю, что везде, где есть хорошая теория, должна быть как минимум одна (с точностью до переобозначений) хорошая нотация.

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

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

[mihaild]

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

Вы умеете так делать сразу на уровне нотации?

Ну да. Там перед этим написано, что условие снизу справа слабее чем условие снизу слева, а пересечение большего семейства меньше.

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

[Padawan]

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

Мне так не кажется. Я думаю, что везде, где есть хорошая теория, должна быть как минимум одна (с точностью до переобозначений) хорошая нотация.

Странное мнение, учитывая теоремы Гёделя о неполноте. Достаточно хорошую теорию нельзя свести к формальной нотации. Лейбниц такое мечтал сделать (универсальный язык), но сейчас-то мы понимаем, благодаря Гëделю, что это невозможно.
А так-то да, полезно придумывать удобные обозначения. Ну так придумывайте, кто Вам не дает. В той же общей топологии. Пока от Вас исходят только общие рассуждения, никакой конкретики. Я вот в Вашей теме о правилах преобразования сумм написал кое-какие тождества, Вы их даже не посчитали нужным прокомментировать/дополнить. Ой, извиняюсь, таки ответили, это я не увидел.

[mihaild]

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

Странное мнение, учитывая теоремы Гёделя о неполноте

Какая связь между теоремами Гёделя и нотацией?
Понятно, что никакая нотация не позволит нам алгоритмически распознавать теоремы нетривиальной теории. Но никто же не требует, чтобы легко доказывались все теоремы.

[Padawan]

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

Но никто же не требует, чтобы легко доказывались все теоремы.

А я понял, что ТС этого и хочет.

[EminentVictorians]

А вот кстати интересный момент. Предположим, у нас есть теория, для которой справедлива теорема Геделя. Допустим, мы придумали такую нотацию, что любое доказательство, которое мы сделали, мы сделали чисто на уровне нотации - вообще без слов. Есть ли тут противоречие? По-моему, нету. Существование такой нотации не делает теорию алгоритмически разрешимой (и не претендует на это).

[Padawan]

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

Можно попробовать взять теорему о том, что замыкание множества совпадает с множеством его точек прикосновения.

$$x\in \overline A\iff x\in\bigcap \{B\mid B\supset A, \overline B=B\}\iff \forall B( B\supset A, \overline B=B\Rightarrow x\in B)\iff$$

$$\iff \forall B(X\setminus B\subset X\setminus A, X\setminus \overline B=X\setminus B\Rightarrow x\not\in X\setminus B) \iff \forall U(U\subset X\setminus A, X\setminus\overline{X\setminus U}= U\Rightarrow x\not\in U) \iff$$

$$ \iff \forall U (U\cap A=\varnothing, \operatorname{Int}U=U\Rightarrow x\not\in U) \iff \forall U(\operatorname{Int} U=U, x\in U\Rightarrow U\cap A\neq \varnothing)$$

[mihaild]

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

Допустим, мы придумали такую нотацию, что любое доказательство, которое мы сделали, мы сделали чисто на уровне нотации - вообще без слов

Нужно уточнять, что значит "на уровне нотации".
В общем-то любой формальный вывод в ZF - это просто последовательность строчек, удовлетворяющая простым правилам. Это "на уровне нотации" или нет?

[EminentVictorians]

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

$$x\in \overline A\iff x\in\bigcap \{B\mid B\supset A, \overline B=B\}\iff \forall B( B\supset A, \overline B=B\Rightarrow x\in B)\iff$$

$$\iff \forall B(X\setminus B\subset X\setminus A, X\setminus \overline B=X\setminus B\Rightarrow x\not\in X\setminus B) \iff \forall U(U\subset X\setminus A, X\setminus\overline{X\setminus U}= U\Rightarrow x\not\in U) \iff$$

$$ \iff \forall U (U\cap A=\varnothing, \operatorname{Int}U=U\Rightarrow x\not\in U) \iff \forall U(\operatorname{Int} U=U, x\in U\Rightarrow U\cap A\neq \varnothing)$$

Мне понравилось. Я не знаю, можно ли сделать такое прям полностью на автомате, но мне кажется, что довольно близко к этому (по крайней мере я шел взглядом по переходам и практически заранее понимал, что будет дальше; настолько оно естественно; но это может быть потому что я и так знаю доказательство).

К тому же это полностью вписывается в формальную теорию (одного) топологического пространства.

Padawan, Вы интересовались насчет алгоритма для всего этого мероприятия, писали, что он вычислительно сложный. Насколько там все плохо?

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

Нужно уточнять, что значит "на уровне нотации".

Символьно, без слов.

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

В общем-то любой формальный вывод в ZF - это просто последовательность строчек, удовлетворяющая простым правилам. Это "на уровне нотации" или нет?

Да, "на уровне плохой нотации". Хорошая нотация - более человеко-ориентированная и компактная.

-- 05.05.2023, 00:28 --

Мне тут пришла в голову мысль. А не будет ли любая нотация любой теории просто ее консервативным расширением?

[Aritaborian]

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

А не будет ли любая нотация любой теории просто ее консервативным расширением?

А вы хотели чего-то существенно большего?

[EminentVictorians]

Aritaborian в сообщении #1592556 писал(а):

А вы хотели чего-то существенно большего?

Да нет, не хотел. Наоборот, для меня это очень хорошая новость - все стало гораздо прозрачнее выглядеть. Просто забавно, что я не сразу догадался до этого, несмотря на то, что мысль очень простая. Ну что поделать, это мозг. Никто не обещал, что он будет работать линейно.

[Padawan]

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

Padawan, Вы интересовались
насчет алгоритма для всего этого мероприятия, писали, что он вычислительно сложный. Насколько там все плохо?

Я там рассматривал класс формула гораздо более ограниченный: только конечное число множеств, нет символов для отдельных точек, нельзя ставить кванторы по множествам.
Насчет сложности - в той статье, на которую я даю ссылку, строится алгебраическая структура "Closure algebra" -- булева алгебра с дополнительной унарной операцией (замыканием), удовлетворяющей аксиомам замыкания Куратовского. Доказывается (теорема 4.15), что для того, чтобы функция $f(x_1, \ldots, x_n) $ от элементов алгебры с замыканием, построенная при помощи операций объединения, пересечения и т. д. и замыкания за $r$ шагов, была тождественна равна нулю (т.е. пустому множеству), необходима и достаточно, чтобы она была равна нулю в любой конечной алгебре с замыканием, состоящей из $2^{2^{n+r}}$ элементов. Осталось перебрать все такие алгебры с точностью до изоморфизма (их конечное число, очевидно) и в каждой из них проверить, что $f$ равна нулю, перебрав все их $n$-элементные наборы $(x_1, \ldots, x_n) $.
Понятно, что наибольшие проблемы будут с перебором всех возможных алгебр с замыканием. Хотя, если это делать не методом грубой силы, а с умом, возможно не все так плохо. У меня были кое-какие соображения на этот счет (обобщение универсального множества на числовой прямой, дающего пример к теореме Куратовского о 14 множествах, на несколько множеств)

[EminentVictorians]

Так если есть необходимость и достаточность, значит теория разрешима. Не слишком ли сильное требование? Может быть хватило бы и полуразрешимости.

К тому же, если я правильно понял, $r$ и $n$ не слишком большие. Странно, что возникают какие-то проблемы с реализацией этого алгоритма.

[mihaild]

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

К тому же, если я правильно понял, $r$ и $n$ не слишком большие.

Да там не то что перебрать, там хотя бы сохранить одну алгебру при $n = r = 3$ довольно сложная задача.

-- 05.05.2023, 10:47 --

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

Хорошая нотация - более человеко-ориентированная и компактная.

А тогда само построение хорошей нотации как раз примерно эквивалентно построению хорошей теории. Ну примерно как можно что-то доказывать про $\mathbb Z_p$ про каждое $p$ по отдельности, а можно сообразить что тут речь о конечных полях. Но халявы не будет, всё равно придется доказывать и общий результат, и сведение к нему.

[EminentVictorians]

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

Да там не то что перебрать, там хотя бы сохранить одну алгебру при $n = r = 3$ довольно сложная задача.

Интересно.

Подумал я еще раз по поводу нотаций. И чет я как-то уже не уверен, что любая нотация - это просто консервативное расширение

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

Сильно не смейтесь, я сам понимаю, как это звучит