ну, всем известно, что многих интегралов наподобие Вашего [tex]\int \frac{sin x}{x} dx[/tex] нельзя записать формулами, но зато можно заведомо вычислить со сколь угодной точностью без никаких проблем - потому что они есть как мат. объект и нехватка обычных мат. символов для их записи совершенно их не колышет; разумеется, мы можем выдумать дополнительные символы для них специально, но пользы от этого не будет.

важно, что можем вычислять числа е и пи, сами означения "е" и "пи" совершенно пренебрежимы и ничтожны

[tex]\int \frac{sin x}{x} dx[/tex] сама по себе запись задачи, а не решения, на которое записи нет

дифуров всяких будет, далеко не все не решаемы (пока?) как Навье-Стокс, слава Богу

зато уверен, что большинство решений решаемых НЕ могут быть записаны конечными формулами типа (х+у)/2, скажем, но вычислить и знать все детали, включая качественные, этих решений не представляет никакой проблемы

Я лишь говорю о том, что только формальная математика неэмпирична.

Vladimirovich wrote:
Это как-то сомнительно. Вот доказательство гипотезы Римана, данное Атьей, оно формально или ошибочно? Как это установить? Не эмпирическим ли консенсусом специалистов? А всем остальным, в любом случае, придется поверить.

Если бы формализованная математика была так же проста, как
игра в шахматы, то, составив описание выбранного нами
формализованного языка, мы должны были бы затем лишь излагать наши
доказательства на этом языке, подобно тому как автор шахматного
трактата записывает в своей нотации партии, которым он хочет
научить, сопровождая их в случае необходимости комментариями.
Однако вопрос решается отнюдь не столь легко, и не требуется
большого опыта, чтобы убедиться в абсолютной неосуществимости
подобного проекта: даже простейшее доказательство из начального
раздела Теории множеств потребовало бы сотен знаков дла своей
полной формализации. Поэтому, уже начиная с Книги I настоящего
Трактата, возникает настоятельная необходимость сокращать
формализованный текст введением новых слов (называемых
„сокращающими символами") и дополнительных правил синтаксиса (называемых
„дедуктивными критериями") в довольно значительном количестве.
Поступая так, мы получаем языки, гораздо более удобные, чем
формализованный язык в собственном смысле, и относительно которых
любой мало-мальски опытный математик будет убежден, что их можно
рассматривать как стенографические транскрипции формализованного
языка. Но мы уже не будем иметь уверенности, что переход от
одного из этих языков к другому может быть сделан чисто
механическим образом. Чтобы обрести эту уверенность, пришлось бы
настолько усложнить правила синтаксиса, управляющие употреблением
новых слов, что польза от этих слов стала бы иллюзорной. Здесь,
как и в алгебраическом исчислении и при употреблении почти любых
обозначений, которыми обычно пользуются математики, удобный
инструмент предпочитается другому, теоретически более совершенному,
но слишком громоздкому.

Как увидит читатель, введение этого сжатого языка сопровождается
-„рассуждениями" особого типа, принадлежащими к так называемой Метаматематике.
Эта дисциплина, абстрагируясь полностью от всякого' значения, которое могло бы первоначально приписываться словам или
фразам формализованных математических текстов, рассматривает эти тексты как особые простые объекты, как собрания некоторых заранее
данных объектов, для которых важен лишь порядок их расположения.
И как трактат по химии заранее объявляет результат эксперимента, производимого при данных условиях, так и метаматематические
„рассуждения" будут обычно устанавливать, что после некоторой
последовательности операций над текстом данного типа окончательный текст-
будет текстом другого данного типа.

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

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

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

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

не очень-то понимаю как может что-то сходиться и потом начать расходиться...

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

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

точность обеспечивается неуклонно (!) сходящейся вычислительной аппроксимацией хорошей мат. модели опыта, однако

попросту там не будем аппроксимировать

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

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

а может ли быть ... строгой, хоть и не строже формализма?

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