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

[mihaild]

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

[EminentVictorians]

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

А что Вы вообще понимаете под "нотацией"?

Вчера - просто какую-то синтаксическую надстройку над формальной теорией (символы + грамматика, с ними связанная). Сегодня, как видите, допускаю и более, так сказать, смелые решения

У меня идея-фикс следующая. Посмотрите на текст доказательства (о замыкании и точках прикосновения), написанный Padawan-ом. Он синтаксически довольно простой. Я хочу всю эту элементарную топологию (и, разумеется, не только ее; но пока можно ограничиться ею) подарить компьютеру, чтобы он занимался доказательствами. Разумеется, я не говорю про любой топологический факт (т.к. некоторые факты могут быть завязаны на конкретные конструкции типа $\mathbb R$ и прочие). Я лишь говорю про элементарную теорию (одного) топологического пространства. И если взять конкретно эту теорию, то я уверен, что как минимум полуразрешимой она точно будет.

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

Нотации для людей тоже интересуют (причем не в меньшей степени).

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

Но халявы не будет

А вдруг будет? У меня есть подозрение, что все теоретические ограничения (типа алгоритмической неразрешимости, неполноты, теорем Геделя и т.п.) - никакие не ограничения. Нам не нужны все теоремы, нам не нужен алгоритм, доказывающий или опровергающий произвольное утверждение. Я даже не уверен, нужна ли нам полуразрешимость. То, что точно надо - это проверка корректности готового доказательства. Это - гораздо более легко решаемая задача. А сами доказательства можно искать всякими не очень детерминированными методами.

Другими словами, у меня прекрасное будущее выгляди так: Очень много разных "элементарных" теорий (типа элементарной топологии). "Голые" факты из этих теорий (типа той же теоремы о совпадении замыкания и множества точек прикосновения) доказываются автоматически. А роль человека в том, чтобы искать известные структуры в конкретных объектах и доказывать сведение к этим известным структурам.

[Ende]

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

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

Либо мы ограничимся математическими понятиями и средствами, либо поедем в "Свободный полет". Выбирайте.

[EminentVictorians]

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

[Ende]

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

нейросеть, ищущая доказательства в некоторой нотации - это математическое понятие или нет?

Нейросеть, ищущая доказательства в некоторой нотации - это тема для форума «Искусственный интеллект и Машинное обучение». И то если Вы готовы сказать об этой нейросети нечто конкретное, например, предложить ее архитектуру и метод обучения. Маниловские мечтания "как было бы хорошо, если бы компьютер/плесень/двое из ларца делали всё за меня, но я понятия не имею, как этого добиться" - это "Свободный полет" с потенциалом перемещения в Пургаторий.

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