Возможности математики без математической индукции

[arseniiv]

(Оффтоп)

Я наблюдал! Иду как-то мимо реки, слышу: плеск какой-то необычный. Посмотрел в воду — а там она!

ewert в сообщении #556326 писал(а):

"Даже терпентин на что-нибудь сгодится" (с)

Точнее, И терпентин на что-нибудь полезен! (К. П., 60-й плод раздумья.)

[Lukin]

ewert в сообщении #555353 писал(а):

Профессор Снэйп в сообщении #555346 писал(а):

. В частности, не существует алгоритма вычисления для функции

$$ f(x) = \begin{cases} 1, &x=0; \\ 0, &x \neq 1 \end{cases} $$

Я Вам хуже того скажу: даже и самой этой функции не существует.

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

ewert в сообщении #555372 писал(а):

Someone в сообщении #555366 писал(а):

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

Я уже об этом говорил. Сказать мы можем что угодно, только вот воспользоваться этим высказыванием практически не сможем. Поскольку если мы сможем построить некоторый объект только при помощи аксиомы полного выбора, то это означает одновременно две вещи:1) мы знаем, что этот объект существует и 2) не менее твёрдо знаем, что никогда, ни при каких условиях найти этот объект не сможем. Практически это означает, что для нас этого объекта не существует.

Воспользоваться сможем, хотя бы для того, чтобы построить еще объекты с таким же свойством, а потом еще… И еще для того, чтобы доказать, что таких объектов больше, чем тех, которые этим свойством не обладают.

[epros]

Профессор Снэйп в сообщении #555346 писал(а):

ewert в сообщении #555329 писал(а):

Какое конкретно число нельзя вычислить?

Как я Вам его назову, если его нельзя вычислить? Разве что специальную буковку введу для его обозначения?

Я могу определить такое "конкретное число". Берём функцию Busy Beaver $\Sigma(n)$. В двоичном разложении числа $\xi_{\Sigma}$ ставим единички только в тех позициях после запятой, где есть значения функции $\Sigma(n)$, т.е. первая единичка в $\Sigma(1)$-ой позиции, вторая - $\Sigma(2)$-ой позиции, третья - в $\Sigma(3)$-ой позиции и т.д. В остальных позициях - нули. Получаем well-defined действительное число $\xi_{\Sigma}$, которое, однако, невычислимо с произвольно заданной точностью в силу невычислимости функции $\Sigma(n)$.

Someone в сообщении #555366 писал(а):

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

Не передёргивайте. Я ничего не говорил против "общеизвестной теоремы", а изначально привёл другую формулировку, которую готов безоговорочно принять (в отличие от формулировки "общеизвестной теоремы").

LaTeXScience в сообщении #555404 писал(а):

epros в сообщении #553869 писал(а):

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

Что значит ``просто иметь''? Как Вы поймете, что какой-то данный Вам алгоритм является именно тем, чем Вы думаете? И почему Вы уверены, что его вообще можно ``иметь'', т.е. где доказательства, что он существует?

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

LaTeXScience в сообщении #555458 писал(а):

epros в сообщении #554733 писал(а):

я оставляю за собой право сомневаться, что словосочетанию "счётное множество" соответствует что-то реальное.

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

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

Кстати, отдельное спасибо Профессору Снейпу за грамотное провоцирование действительно интересной дискуссии.

[LaTeXScience]

epros в сообщении #558220 писал(а):

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

Вера и наука несовместимы. А если окажется, что для какого-то слова программа выдает не верный ответ? Т.е. это может быть не та программа, что вы думаете.

epros в сообщении #558220 писал(а):

Улавливаете разницу между "юзером", который просто верит в то, что программа делает именно то, что ему нужно, но не понимает как она работает, и "программером", который всё это разработал и отладил?

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

-- 09.04.2012, 13:01 --

epros в сообщении #558220 писал(а):

Математика меня интересует в первую очередь как инструмент для создания практически применимых теорий.

Применимость теории зависит от ее интерпретации. Сопоставлением матмоделей с реальностью занимается физика, а не математика.

[epros]

LaTeXScience в сообщении #558249 писал(а):

Вера и наука несовместимы. А если окажется, что для какого-то слова программа выдает не верный ответ? Т.е. это может быть не та программа, что вы думаете.

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

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

LaTeXScience в сообщении #558249 писал(а):

Но ведь ''юзер'' использует ''программера'', который использовал математическую индукцию. Т.е. ''юзер'' косвенно использовал метод математической индукции.

Не-не, давайте не будем подменять понятия. Юзер не "косвенно использует" что-то там от разработчика, а просто-напросто ВЕРИТ его заявлениям о назначении и функциях программы. Например, нам предоставили некую библиотеку процедур, которые: 1) Распознают корректные высказывания в языке ZFC, 2) Проверяют, что высказывание является аксиомой ZFC, 3) Проверяют, что последовательность высказываний является доказательством в ZFC и т.д. Можем ли мы считать, что у нас теперь есть всё необходимое для "формальных рассуждений в рамках ZFC"? Или нужно лезть в код и всё досконально проверять? А вдруг разработчик с недобрыми намерениями подсунул нам закладку, чтобы в один прекрасный день, когда мы захотим доказать что-то эдакое навороченное, программа подсунула нам ошибочное доказательство и мы бы опозорились на весь математический мир?

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

LaTeXScience в сообщении #558249 писал(а):

Применимость теории зависит от ее интерпретации. Сопоставлением матмоделей с реальностью занимается физика, а не математика.

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

[Maslov]

epros в сообщении #558278 писал(а):

Не забывайте, что безоговорочно принимаемые аксиомы - это тоже "вера", ибо никакого доказательства оных нет и не может быть по определению.

Честно говоря, не понял, при чем тут "вера". Когда мы строим вывод в формальной теории, построенной на основе некоторых аксиом, мы всегда должны помнить, что этот вывод справедлив только в заданной аксиоматике. А уж "верим" мы в принятые аксиомы или не верим -- дело десятое.

epros в сообщении #558278 писал(а):

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

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

epros в сообщении #558278 писал(а):

Можем ли мы считать, что у нас теперь есть всё необходимое для "формальных рассуждений в рамках ZFC"? Или нужно лезть в код и всё досконально проверять?

Безусловно, не можем. И даже после того, как слазали в код, все равно не можем: мы тоже могли ошибиться при верификации.

epros в сообщении #558278 писал(а):

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

Вы бы не могли пояснить, что Вы понимаете под "недоверием к аксиоматике"?

[LaTeXScience]

epros в сообщении #558278 писал(а):

Хе-хе. Смею утверждать, что Вы тут ошибаетесь: вера с наукой ещё как совместимы.

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

epros в сообщении #558278 писал(а):

Мало того, без веры в некоторые вещи никакой науки ну совершенно не получится.

Я подозреваю, что Вы путаете понятия ``вера'' и ``доверие''. Советую Вам почитать http://warrax.net/88/faith.html ``Вера — что это такое?''.

epros в сообщении #558278 писал(а):

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

Не всегда, но я при этом не утверждаю, что создаю математические теории.

epros в сообщении #558278 писал(а):

Не-не, давайте не будем подменять понятия.

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

-- 09.04.2012, 15:50 --

Maslov в сообщении #558292 писал(а):

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

Кстати говоря, есть такая вещь, как формальная верификация.

[epros]

Maslov в сообщении #558292 писал(а):

epros в сообщении #558278 писал(а):

Не забывайте, что безоговорочно принимаемые аксиомы - это тоже "вера", ибо никакого доказательства оных нет и не может быть по определению.

Честно говоря, не понял, при чем тут "вера". Когда мы строим вывод в формальной теории, построенной на основе некоторых аксиом, мы всегда должны помнить, что этот вывод справедлив только в заданной аксиоматике. А уж "верим" мы в принятые аксиомы или не верим -- дело десятое.

Вот я и говорю про "безоговорочно принимаемые". Разумеется, если мы относимся к аксиоме просто как к некоторому предположению, принятому "чисто чтобы посмеяться", то и к выводу из такой аксиоматики мы будем относиться как к чему-то условному. Например, я примерно так отношусь к аксиоме бесконечности: Забавное утвержение, вроде бы ни к каким противоречиям не приводит. Возможно, даже что-то там упрощает для тех, кто ленится доказывать нечто важное без этой аксиомы. Но чтобы искренне поверить в то, что это утверждение "никак нельзя не принять", мне чего-то не хватает...

Maslov в сообщении #558292 писал(а):

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

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

Maslov в сообщении #558292 писал(а):

epros в сообщении #558278 писал(а):

Можем ли мы считать, что у нас теперь есть всё необходимое для "формальных рассуждений в рамках ZFC"? Или нужно лезть в код и всё досконально проверять?

Безусловно, не можем. И даже после того, как слазали в код, все равно не можем: мы тоже могли ошибиться при верификации.

Гы-гы. При таком подходе мы никогда ни к чему не сможем отнестись достаточно серьёзно, чтобы начать его реально использовать.

Maslov в сообщении #558292 писал(а):

Вы бы не могли пояснить, что Вы понимаете под "недоверием к аксиоматике"?

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

[LaTeXScience]

epros в сообщении #558310 писал(а):

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

А кто же Вас заставляет в это верить? Не верьте. Верить вообще вредно для мозга.

[Lukin]

epros в сообщении #558220 писал(а):

ewert в сообщении #555329 писал(а):

Какое конкретно число нельзя вычислить?

Я могу определить такое "конкретное число". Берём функцию Busy Beaver $\Sigma(n)$. В двоичном разложении числа $\xi_{\Sigma}$ ставим единички только в тех позициях после запятой, где есть значения функции $\Sigma(n)$

epros в сообщении #558220 писал(а):

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

Мне не понятно, как Вы проводите грань между тем, что "могло бы существовать, если бы …" и тем, что не могло бы…
Например, Вы считаете, что положительно определили число $\xi_{\Sigma}$.
А давайте заменим слова "алгоритм длинной $n$ или Тюринг - машина с $n$ состояниями", например, на ту же функцию

$$ f(x) = \begin{cases} 1, &x=0; \\ 0, &x \neq 1 \end{cases} $$

или совсем грустно: если $a \land \neg a$ то на шаге $n$, в двоичном разложении числа $\xi_{\Sigma}$ ставим 1, иначе 0 ?
Вы же не считаете, что последнее - всего - лишь редуцированное к минимуму содержание Вашего определения числа $\xi_{\Sigma}$ и в общем-то заготовка для несчетного количества определений задач (чисел) подобного рода ?

[epros]

LaTeXScience в сообщении #558301 писал(а):

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

Не стоит абсолютизировать. Бывает, что от веры отступаются.

LaTeXScience в сообщении #558301 писал(а):

Первый человек -- верующий, второй человек -- ученый.

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

LaTeXScience в сообщении #558301 писал(а):

Я подозреваю, что Вы путаете понятия ``вера'' и ``доверие''. Советую Вам почитать http://warrax.net/88/faith.html ``Вера — что это такое?''.

Ага, путаю. И настаиваю на этом. Это просто разные по степени категоричности формы выражения одного и того же. Попытки доказывать противоположное с моей точки зрения - словоблудие. Видите ли, я так себе понимаю, что противопоставление веры и "научного подхода" - это чистая идеология, которая нужна была в своё время учёным для того, чтобы отмежеваться от религиозных деятелей в глазах "простых людей". Современной науке эта идеология на самом деле ни к чему.

LaTeXScience в сообщении #558301 писал(а):

epros в сообщении #558278 писал(а):

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

Не всегда, но я при этом не утверждаю, что создаю математические теории.

Любопытно, а когда же Вы начинаете утверждать, что у Вас есть математическая теория? Может когда в терминах теории множеств докажете, что "теория существует"? А это ничего, что Ваше доказательство основано просто на КУЧЕ всяких безапелляционно (и зачастую - неявно) принятых аксиом?

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

LaTeXScience в сообщении #558301 писал(а):

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

Попробуйте теперь сказать, что мат. индукция - не предмет вашей ВЕРЫ. Я-то как раз принимаю её с существенными оговорками, а вот с Вами, похоже, мы имеем тот самый случай, когда Вы "никогда не отступитесь".

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

[Maslov]

LaTeXScience в сообщении #558301 писал(а):

Кстати говоря, есть такая вещь, как формальная верификация.

Вам известны реальные примеры применения верификации программ, более сложных, чем вычисление факториала? Не алгоритмов, а именно программ?

epros в сообщении #558310 писал(а):

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

Ну это, так сказать, Ваши личные сложности :)

epros в сообщении #558310 писал(а):

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

Тем не менее, мы летаем на самолетах, зная, что они могут упасть, ездим на машинах, зная, что можем попасть в аварию, и т. д. и т. п.

epros в сообщении #558310 писал(а):

Например, не верим, что скорость света равна известной величине в любой ИСО, и всё тут: Продолжаем подозревать, что найдутся ситуации, в которых это могло бы не сработать.

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

[epros]

Maslov в сообщении #558336 писал(а):

epros в сообщении #558310 писал(а):

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

Ну это, так сказать, Ваши личные сложности :)

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

Maslov в сообщении #558336 писал(а):

Тем не менее, мы летаем на самолетах, зная, что они могут упасть, ездим на машинах, зная, что можем попасть в аварию, и т. д. и т. п.

Ну так а я о чём? Вопрос - практический: аксиому "самолёт не упадёт" иногда полезно принять. Может иногда и аксиому бесконечности имеет смысл принимать - для упрощения чего-то там, чтобы запудрить мозги первокурсникам, отделавшись "простыми" объяснениями и т.п. Но если вопрос ставится фундаментально - типа того, что без этой аксиомы никак не обойтись "в народном хозяйстве", то я что-то сомневаюсь...

Консенсус?

Maslov в сообщении #558336 писал(а):

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

Хе-хе. Не согласен я. Это - аксиома в теоретическом смысле, который от математического по существу ничем не отличается. Ну, в физике это именуют не "аксиомой", а "постулатом", и что с того? И насчёт "экспериментального факта" - это тоже не совсем точно. Результаты экспериментов (т.е. "экспериментальные факты") всегда свидетельствуют о конкретных вещах, применительно к конкретным условиям. А в теории речь идёт об обобщении, которое в строгом смысле из совокупности результатов экспериментов не следует. Разумеется, мы пользуемся физической теорией постольку, поскольку она адекватно описывает наблюдения в своей сфере применения. Но по-моему это имеет прямое отношение к "доверию к аксиомам формальной теории": Если мы придём к мысли, что объекты рассматриваемой предметной области корректно описываются теорией групп, а не теорией действительных чисел, то мы будем "доверять" аксиомам теории групп, а не аксиомам теории действительных чисел.

[LaTeXScience]

Maslov в сообщении #558336 писал(а):

Вам известны реальные примеры применения верификации программ, более сложных, чем вычисление факториала? Не алгоритмов, а именно программ?

http://coq.inria.fr/cocorico/FormalizedAndVerified
http://proval.lri.fr/gallery/index.en.html
Сойдет?

[Maslov]

epros в сообщении #558354 писал(а):

Вопрос - практический: аксиому "самолёт не упадёт" иногда полезно принять.

По-моему, Вы слишком вольно обращаетесь понятием "аксиома". Употребление слова "аксиома" для утверждений типа "самолеты не падают" или "Солнце вращается вокруг Земли" говорит только о степени нашей уверенности в истинности этих утверждений и к использованию этого термина при построении формальных теорий отношения не имеет.

epros в сообщении #558354 писал(а):

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

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

epros в сообщении #558354 писал(а):

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

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

LaTeXScience в сообщении #558362 писал(а):

http://coq.inria.fr/cocorico/FormalizedAndVerified
http://proval.lri.fr/gallery/index.en.html
Сойдет?

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