Потеряем общность, но получим легкость преобразований

[iifat]

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

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

Ну дык есть же ж уже! «Один плюс один равно жёлтые ботинки». Алиса в стране чудес не то в Зазеркалье, не помню. Правда, глупый Доджсон не стал выводить из этого математическую теорию.

[talash]

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

Хочется, чтобы числовая система была сильно интереснее: можно, например, пожертвовать существованием или алгоритмическим определением нуля (а иметь вместо него "монаду" околонулевых чисел).

Что это за философский принцип такой "сильно интереснее"? Вот есть "принцип простоты", на самом деле он неявно используется при выборе математических правил. Например, чтобы операция извлечения корня была определена на всей числовой прямой, можно было определить умножение отрицательных чисел, как "минус на минус даёт минус", но такое определение ломает другие важные правила(переместительный и распределительный законы) и делает математику сложнее.
Поэтому, выбор очевиден. И вот эти другие варианты определения умножения отрицательных чисел они очевидны. А как избавиться от 0 и вариантов конкретных нету. В древности не встречался 0 в записи, но и математика без него была крайне примитивна.

[Mihaylo]

"Если упрощенно, то вселенная - это есть огромная нейронная сеть."

Черт! Мне нравятся такие умозаключения!

[iifat]

talash в сообщении #1649971 писал(а):

Что это за философский принцип такой "сильно интереснее"?

Да принцип-то, как по мне, вполне нормальный. Заинтересоваться чем-то, понастроить теорий, убедиться, что ничего интересного не выводится — почему нет? А иногда ведь может и вывестись — не так ли появились неевклидовы геометрии?
Другое дело ­— «мне интересно, постройте-ка мне теорию, а я с дивана погляжу»...

[mihaild]

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

Хочется чтобы проверку на корректность делал компилятор, а не руки. А в обычной версии матанализа такое невозможно

Вот на Вашем примере: если $f$ и $g$ интегрируемы по Риману, то равенство верно, а если нет - то его нельзя записать, "попытка взять интеграл Римана от неинтегрируемой по Риману функции".

[мат-ламер]

EminentVictorians
Почитайте про Лейбница .

Цитата:

Опередив время на два века, 21-летний Лейбниц задумал проект математизации логики[10][13]. Будущую теорию (которую он так и не завершил) он называет «всеобщая характеристика». Она включала все логические операции, свойства которых он ясно представлял. Идеалом для Лейбница было создание такого языка науки, который позволил бы заменить содержательные рассуждения исчислением на основе арифметики и алгебры: «… с помощью таких средств можно достичь… удивительного искусства в открытиях и найти анализ, который в других областях даст нечто подобное тому, что алгебра дала в области чисел»

Цитата:

Лейбниц мыслил высший анализ не кинематически, как Ньютон, а алгебраически. В первых работах он, похоже, понимал бесконечно малые как актуальные объекты, сравнимые между собой, только если они одного порядка. Возможно, он надеялся установить их связь со своей концепцией монад[51].

Цитата:

Лейбниц писал также о возможности машинного моделирования функций человеческого мозга[26].

Мне кажется, вы собираетесь стать продолжателем его идей. Но как-то у вас всё сильно глобально - конкретики не хватает. Без конкретных примеров ваши идеи мне не уловить.

[EminentVictorians]

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

"попытка взять интеграл Римана от неинтегрируемой по Риману функции".

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

$$D(x) = \left\{ \begin{array}{rcl} 1, x \in \mathbb Q\\ 0, x \in \mathbb I \\ \end{array} \right.$$

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

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

[dgwuqtj]

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

Сам язык должен ограничивать нас, чтобы мы не могли выразить в нем ни $\mathbb Q$, ни $\in$ и т.д.

Вы свою систему для записи интегралов совместите с каким-нибудь пруфчекером и запретите писать интеграл, если не доказано, что подынтегральная функция интегрируема. Вообще тут общая проблема, что в языках первого порядка функциональные символы интерпретируются как тотальные функции, а иногда хочется частично определённые. Стандартное (пусть и не эргономичное) решение — формализовывать частичные отображения как предикатные символы, скажем, $\text{IsIntegral}(f, a, b; i)$ вместо $\int_a^b f(x)\, dx = i$.

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

[EminentVictorians]

dgwuqtj в сообщении #1650165 писал(а):

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

Тогда пропадает основной смысл всего мероприятия - делать преобразования нативно, не отвлекаясь на проверки условий. Проверять интегрируемость каждый раз я и на бумаге могу.

dgwuqtj в сообщении #1650165 писал(а):

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

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

dgwuqtj в сообщении #1650165 писал(а):

Речь вообще идёт о том, как придумывать маленькие алгоритмические эффективные формализации кусочков математики (типа арифметики Пресбургера) или о том, как формализовывать всю математику целиком?

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

[dgwuqtj]

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

Пока хочу эффективную реализацию матанализа.

В классическом матанализе может хватит и классов функций $\mathrm C^k(U \to V)$ для открытых множеств $U$ и $V$, $0 \leq k \leq \infty$. Для них есть хорошие всюду определённые операции. Если не хочется следить за порядком гладкости, вообще ограничьтесь $\mathrm C^\infty(U \to V)$, только там функций типа $x \mapsto |x|$ нет.

[talash]

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

talash в сообщении #1626882 писал(а):

Доказательство, что два равно один. Начнём с простого утверждения:

$a = b$

Умножив обе части равенства на $a$, получим:

$a^2 = ab$

Добавив к обеим частям равенства по $a^2 - 2ab$:

$a^2 + a^2 - 2ab = ab + a^2 - 2ab$

Это равенство можно упростить:

$2(a^2 - ab) = a^2 - ab$

Наконец, сокращая это выражение на $a^2 - ab$ получаем:

$2=1$

[epros]

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

Хочется чтобы проверку на корректность делал компилятор, а не руки. А в обычной версии матанализа такое невозможно.

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

Википедия в статье Typed lambda calculus писал(а):

All the systems mentioned so far, with the exception of the untyped lambda calculus, are strongly normalizing: all computations terminate. Therefore, they cannot describe all Turing-computable functions.

[Mihaylo]

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

Потеряем общность, но получим легкость преобразований

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