Аксиомы "не математики"

[Ribocyte]

bin в сообщении #631093 писал(а):

Прежде всего: что понимается под термином "вычисление"?

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

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

-- 15.10.2012, 08:44 --

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

[Ribocyte]

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

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

А если не думаю?

-- 15.10.2012, 10:01 --

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

Во-первых, это не новость.

Очень рад за Вас, что Вы знаете этот банальный факт. Цепочка любых логических рассуждений сводится к совокупности банальных применений фиксированных правил вывода. Будете ли Вы при любом выводе стоять рядом и с каждым применением этого правила декларировать истину - "это - банальная процедура"? Объявите ли Вы при этом любую теорему банальной?

-- 15.10.2012, 10:11 --

bin в сообщении #631093 писал(а):

Как, нпр., с помощью вычислений доказать, что отношение длины окружности к ее диаметру есть величина постоянная?

Формальное доказательство в классическом смысле - одна из разновидностей психологического убеждения. Каждый может рассмотреть хотя бы в принципе протокол доказательства.
Квантовое вычисляющее устройство оперирует с объектами, которые нельзя перенумеровать. И протокол доказательства Вы не получите. Тем не менее оно на выходе также даёт результат, которому мы можем доверять на том основании, на котором мы доверяем самой квантовой физической модели. Равно как мы доверяем физической модели, дающей возможность манипулировать с нумеруемыми макроскопическими объектами. И там, и там принципиально - физические явления. Просто к модели оперирования с камешками на песке мы больше доверяем, больше к ней привыкли - настолько, что такая модель считается для нас банальной.
Хотя и даже в рамках такой модели операции с нумеруемыми символами - это разновидность экспериментирования.
Возьмите ЛЮБУЮ кучу камешков (будем для определенности считать, что в куче камешков больше 1).
Если Вы доверяете физической модели, описывающей собирание камешков в кучи, то Вы можете сформулировать очень просто гипотезу Гольдбаха:
Если кучу камешков можно разбить на две кучи с равным количеством камешков (если число чётное), то её обязательно можно разбить на две кучи, каждую из которых в отдельности нельзя разбить на кучи с равным количеством камешков (простые числа).

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

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

[bin]

Ribocyte в сообщении #631094 писал(а):

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

Где?

[Ribocyte]

bin в сообщении #631148 писал(а):

Где?

На второй странице данной темы - моё сообщение.

[bin]

Ribocyte в сообщении #631094 писал(а):

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

Всякий ли алгоритм есть результат вычислений?

[Ribocyte]

bin в сообщении #631153 писал(а):

Всякий ли алгоритм есть результат вычислений?

Всякое применение алгоритма есть вычисление.

[bin]

Ribocyte в сообщении #631150 писал(а):

bin в сообщении #631148 писал(а):

Где?

На второй странице данной темы - моё сообщение.

Спектр излучения молекул пример такого рода вычисленя? Не вижу сходства с

bin в сообщении #631093 писал(а):

Как, нпр., с помощью вычислений доказать, что отношение длины окружности к ее диаметру есть величина постоянная?

-- Пн окт 15, 2012 10:59:02 --

Ribocyte в сообщении #631154 писал(а):

bin в сообщении #631153 писал(а):

Всякий ли алгоритм есть результат вычислений?

Всякое применение алгоритма есть вычисление.

Я спросил не о применении!

[Ribocyte]

bin в сообщении #631156 писал(а):

Спектр излучения молекул пример такого рода вычисленя? Не вижу сходства с

Почему Вы решили искать сходство там, где его искать нет смысла? Я отвечал на вопрос о вычислении вообще и вопрос этот цитировал. И при этом не цитировал вопрос о каком-то конктретном вычислении.

-- 15.10.2012, 14:03 --

bin в сообщении #631156 писал(а):

Я спросил не о применении!

Верно. Изначально Ваш вопрос мне показался сумбурным "Всякий ли алгоритм есть результат вычислений?" Именно поэтому я и написал, что вычисление в классическом понимании - это результат применения алгоритма.

[bin]

Смысл в цитате:

Цитата:

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

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

Т.о. доказательные вычисления возможны не для всех доказательств.

-- Пн окт 15, 2012 11:12:28 --

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

[Ribocyte]

bin в сообщении #631160 писал(а):

Цитата:
Автоматическое доказательство — доказательство, реализованное программно. В основе лежит аппарат математической логики. Используются идеи теории искусственного интеллекта. Процесс доказательства основывается на логике высказываний и логике предикатов.

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

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

[bin]

Оставим в покое геометрию. В любом случае:

Цитата:

Интуитивно понятно, что чем сложнее и выразительнее теория, тем больше шансов, что она окажется неразрешимой. Поэтому, грубо говоря, «неразрешимая теория» — синоним к «сложная теория».[...]Разрешимость — очень сильное свойство, и большинство полезных и используемых на практике теорий им не обладают. (Википедия: Алгоритмическая разрешимость)

-- Пн окт 15, 2012 11:48:06 --

Ribocyte в сообщении #631166 писал(а):

Этот алгоритм страшно громоздкий. Вряд ли его будут применять на практике.

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

[Ribocyte]

bin в сообщении #631178 писал(а):

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

Что такое неразрешимость теории? Это остутствие алгоритма, с помощью которого можно узнать, является ли утверждение данной теории теоремой или нет.
Например, элементарная геометрия разрешима.
Арифметика сложения и умножения натуральных чисел - нет.
Даже логика первого порядка, хотя она и полна, всё равно неразрешима.

[epros]

bin в сообщении #631093 писал(а):

Прежде всего: что понимается под термином "вычисление"? Как, нпр., с помощью вычислений доказать, что отношение длины окружности к ее диаметру есть величина постоянная?

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

[Ribocyte]

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

Как, нпр., с помощью вычислений доказать, что отношение длины окружности к ее диаметру есть величина постоянная?

Можно.
Формализовать теорию. Потом генерировать доказательства с помощью какого-то алгоритма. Рано или поздно (важно, что за конечное число шагов) наткнётесь на доказательство этого утверждения - вычислите его.

[Padawan]

Ribocyte в сообщении #631190 писал(а):

Что такое неразрешимость теории? Это остутствие алгоритма, с помощью которого можно узнать, является ли утверждение данной теории теоремой или нет. Например, элементарная геометрия разрешима. Арифметика сложения и умножения натуральных чисел - нет. Даже логика первого порядка, хотя она и полна, всё равно неразрешима.

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

Ribocyte в сообщении #631222 писал(а):

Формализовать теорию. Потом генерировать доказательства с помощью какого-то алгоритма. Рано или поздно (важно, что за конечное число шагов) наткнётесь на доказательство этого утверждения - вычислите его.

не факт, что Вы дождетесь, что нужное утверждение будет доказано.