Когда читаю о таких случаях, всегда возникает вопрос: почему доказательства не формализуют? В компьютерном смысле слова
Это оригинальный вопрос, на который я ответил, что не вижу в этом смысла.
И в частности потому, что в общем случае, там где подобные средства будут необходимы, очень вероятно, что
ошибки лежат за рамками доказательства теоремы.
Соотнося трудозатраты на разработку подобного продукта, его сложность, и практический выхлоп я до сих пор не услышал ни одного аргумента, чтобы поменять своего мнения:)
Про введение новых теорий я ничего не говорил, предполагается использование классических теорий.
Вы и обратного не говорили. И каких это классических теорий предполагается и кем? Если разговор скатывается в какие-то частные случаи — не вижу смысла его поддерживать. Мне уже предлагали здесь «новую логику». С моей стороны выражение «в общем случае» было почти в каждом ответе.
Далее, у нас две теории.
Речь лишь об обнаружении ошибок, которые выясняются после развития и исследования изложенной теории и не фигурируют в доказательстве непосредственно. Не больше и не меньше.
проверяем уже имеющееся доказательство, это работа чисто техническая
Странное заявление, для человека, считающего, что у него нет «проблемы с пониманием математики как таковой».
Вам дают доказательство утверждения, построенное на своей новой уникальной математической теории. Приводят в рамках этой теории доказательство. Вы отдаете его своей чудо-программе и проверяете(еще непонятно как, т.к. надо ее не только правильно понять в итоге, но и прежде правильно формализовать для программы). Программа говорит — ОК (Errors — 0, Warnings — 14 567)
Доказательство утверждения в рамках теории успешное.
Теория и утверждение берется на вооружение научным сообществом. И вот в рамках углубленного последующего изучения и развития этой новой теории в ней обнаруживаются неустранимые противоречия или несостыковки с уже доказанными и проверенными теориями, которые приводят в итоге и пересмотру всех результатов.
На мой взгляд, текст такой программы должен быть предельно прост:
{
print(42)
}
ведь изучением способов получать одни суждения из других занимается логика
Получать одни суждения из других это не проблемная часть математических доказательств. Гораздо интересней оценить адекватность выбора исследуемой модели и соотношение всех значимых следствий, которые получаются после ее построения с уже существующими теориями. Вы можете придумать свою теорию. Доказать в ее рамках требуемое утверждение. Но потом выяснится, что ваша теория противоречит другим, уже доказанным и общепризнанным теориям и/или сама является противоречивой.
Ну а почему нет, если существующих логик недостаточно
Ну в качестве эксперимента можно делать все что угодно:) Я же про это ничего не могу сказать и не знаю как это соотносится с объективной реальностью:) Эли это строго детерминированный алгоритм — это круто.
Не важно:) Выбранные тоже вначале надо доказать или вручную или «автоматически» и мы возвращаемся к сути проблемы, а именно вмешательства человека в процесс доказывания.
Так вы и не объяснили, что за «правильность метода».
Так вы и не спрашивали и странно, что требуется пояснение. Имеется ввиду любой математический метод или прием, который в данной ситуации приведет построению в дальнейшем непротиворечивых суждений.
«Достоверность исходных данных» — что есть в вашем понимании достоверность и причем тут она мне тоже неясно.
Достоверность — самый обычный термин. В своем значении он и употребляется. Любые строгие утверждения могут строится исключительно на достоверных данных.
Все методы — обоснованы.
О чем и речь. Обоснование выбора метода — в этом вопросе задача не алгоритмическая в общем случае. И что делать с новыми методами без вмешательства человека совсем понятно. А если от обоснованность выбора метода является ключевым пунктом доказательства, то смысл существования такого «автоматизированного» средства совсем нивелируется.
мне неинтересно разбираться в вашей терминологии.
Терминология тут, право, не причем. Она самая обычная и разбираться в ней нет необходимости:)
Все выбранные приемы и теоремы должны быть предварительно определены, ибо это математика.
Не могут быть в принципе — ибо это математика. Если бы все они были бы определены — все существующие утверждения были бы уже доказаны или опровергнуты.
А в чем ценность, если «заданное формально доказательство» неверно? Ведь выбор неверных исходных данных, гипотез, приемов, следствий при логической непротиворечивости цепочки вывода даст недостоверный результат.
что в вашем понимании значит «обосновать правильность выбора каждого метода»
То, что любое доказательство, это совокупность различных приемов. Вот пример: school14-v.ucoz.ru/publ/1-1-0-2
Возможно, существуют и другие. От выбора метода на любом этапе зависят дальнейшие результаты. Выбор правильного метода — дает правильные результаты. Неприменимого — недостоверные.
Мы имеет метод, для которого доказана работа на данных класса А. Если этот метод используем в теореме на данных не класса А, то он неприменим. Если на данных класса А, то он применим.
Метод M — неприменим в конкретном доказательстве утверждения, но для M — доказана работа на данных класса А.
Применение М в рассуждениях даст недостоверный результат.
Если проверяемое доказательство уже задано в машину, мы всего лишь проверяем корректность всех логических переходов. Причем здесь произвольные суждения?
Одна только «корректность всех логических переходов» не гарантирует достоверность доказательства.
Необходимы так же достоверность исходных данных и логическая обоснованность самих переходов.
Вот только методы не «выбраны автором», а заранее предопределены математической логикой.
Методы не могут быть заранее предопределены:) Существуют множества, в том числе и еще неизвестные, доказательств одних и тех же утверждений.
набором «общепризнанных» теорем
Все сводится к созданию этого «набора», но проблема в том, что этот набор по-определению уже будет неполон в силу искусственности своего происхождения.
приводится пример полностью формализованного доказательства одной из теорем
Речи о том, что формализовать существующие доказательства нельзя — не было. Речь о том, что в общем случае, алгоритмизировать доказательство произвольных суждений пока что невозможно, а соответственно любая работа в этом направлении пока что лишена смысла в силу.
Вы неправильно интерпретировали запись M1(A). Это не предикат, в общем случае. Это некоторый способ или прием, который применяется к некоторому набору фактов А, чтобы получить другой набор фактов S1 (скорее некоторый набор предикатов). Одну и ту же теорему можно доказать множеством совершенно разных способов используя разные приемы. Результата это не меняет. Но выбрав неправильный прием, можно получить уже другой результат. Как алгоритмически в общем случае определять применимость использования того или иного приема совершенно непонятно. Более того, как оценивать применимость совершенно нового и неизвестного ранее математического приема или способа?
При оценке нового математического доказательства, нужно понимать применимость тех или иных математических методов или приемов
Именно. Любая подобная программа будет работать с уже выбранными автором методами и пытаться искать «ошибки» в уже сформированном доказательстве. В общем случае, алгоритмически правильно обосновать правильность выбора каждого метода равносильно задаче автоматически доказывать произвольные математические утверждения, что равносильно созданию, даже не «искусственного», интеллекта.
Машина Тьюринга, строго говоря, это и есть математическое определение алгоритма. А доказательство произвольных суждений, в общем случаем, вряд ли алгоритмически реализуемая на настоящий момент, задача.
А кто знает какое следствие является логически необходимым? Простой пример: Есть факт A. Есть два метода(утверждения, аксиомы, приема, формулы и т.д. применимых для А): M1 и M2 (на самом деле сколь угодно). И вот автор применяя M1 к А получает следствие S1: S1 = M1(A). Аналогично S2=M2(A). Выбирая M1 и M2 можно получить взаимно противоречивые или просто разные следствия S1 и S2 при полностью формально правильном применении M1 и M2, что можно алгоритмически проверить. Но как алгоритмически проверить правильность выбора M1 или M2? Сколько методов не формализуй остается проблема правильности их выбора. Собственно это и есть самая большая проблема в оценке правильности математических доказательств.
Потому что задача сводится к построению системы, которая умеет думать. При оценке нового математического доказательства, нужно понимать применимость тех или иных математических методов или приемов, используемых в доказательстве, а не формальное наличие алгоритмических ошибок.
Странное(но понимаемое и не разделяемое) желание алгоритмизировать процесс проверки доказательств теорем. Почему бы не пойти дальше и не алгоритмизировать проверку на «красоту» и «правильность» различных произведений искусства вроде картин, скульптур, стихотворений, музыки.
Не может иметь это смысла.
Вы тоже правы. Я, пожалуй, выразился слишком обще по теме, а не применительно к этому репортажу. Но сути это не меняет. И пока из заявленных публично предложений и конкретных шагов по решению этой проблемы и по регулированию Интернета в частности на территории РФ поводов для оптимизма немного.
Это оригинальный вопрос, на который я ответил, что не вижу в этом смысла.
И в частности потому, что в общем случае, там где подобные средства будут необходимы, очень вероятно, что
Соотнося трудозатраты на разработку подобного продукта, его сложность, и практический выхлоп я до сих пор не услышал ни одного аргумента, чтобы поменять своего мнения:)
Вы и обратного не говорили. И каких это классических теорий предполагается и кем? Если разговор скатывается в какие-то частные случаи — не вижу смысла его поддерживать. Мне уже предлагали здесь «новую логику». С моей стороны выражение «в общем случае» было почти в каждом ответе.
Речь лишь об обнаружении ошибок, которые выясняются после развития и исследования изложенной теории и не фигурируют в доказательстве непосредственно. Не больше и не меньше.
Странное заявление, для человека, считающего, что у него нет «проблемы с пониманием математики как таковой».
Вам дают доказательство утверждения, построенное на своей новой уникальной математической теории. Приводят в рамках этой теории доказательство. Вы отдаете его своей чудо-программе и проверяете(еще непонятно как, т.к. надо ее не только правильно понять в итоге, но и прежде правильно формализовать для программы). Программа говорит — ОК (Errors — 0, Warnings — 14 567)
Доказательство утверждения в рамках теории успешное.
Теория и утверждение берется на вооружение научным сообществом. И вот в рамках углубленного последующего изучения и развития этой новой теории в ней обнаруживаются неустранимые противоречия или несостыковки с уже доказанными и проверенными теориями, которые приводят в итоге и пересмотру всех результатов.
На мой взгляд, текст такой программы должен быть предельно прост:
{
print(42)
}
Получать одни суждения из других это не проблемная часть математических доказательств. Гораздо интересней оценить адекватность выбора исследуемой модели и соотношение всех значимых следствий, которые получаются после ее построения с уже существующими теориями. Вы можете придумать свою теорию. Доказать в ее рамках требуемое утверждение. Но потом выяснится, что ваша теория противоречит другим, уже доказанным и общепризнанным теориям и/или сама является противоречивой.
Ну в качестве эксперимента можно делать все что угодно:) Я же про это ничего не могу сказать и не знаю как это соотносится с объективной реальностью:) Эли это строго детерминированный алгоритм — это круто.
Так вы и не спрашивали и странно, что требуется пояснение. Имеется ввиду любой математический метод или прием, который в данной ситуации приведет построению в дальнейшем непротиворечивых суждений.
Достоверность — самый обычный термин. В своем значении он и употребляется. Любые строгие утверждения могут строится исключительно на достоверных данных.
О чем и речь. Обоснование выбора метода — в этом вопросе задача не алгоритмическая в общем случае. И что делать с новыми методами без вмешательства человека совсем понятно. А если от обоснованность выбора метода является ключевым пунктом доказательства, то смысл существования такого «автоматизированного» средства совсем нивелируется.
Терминология тут, право, не причем. Она самая обычная и разбираться в ней нет необходимости:)
Не могут быть в принципе — ибо это математика. Если бы все они были бы определены — все существующие утверждения были бы уже доказаны или опровергнуты.
То, что любое доказательство, это совокупность различных приемов. Вот пример: school14-v.ucoz.ru/publ/1-1-0-2
Возможно, существуют и другие. От выбора метода на любом этапе зависят дальнейшие результаты. Выбор правильного метода — дает правильные результаты. Неприменимого — недостоверные.
Метод M — неприменим в конкретном доказательстве утверждения, но для M — доказана работа на данных класса А.
Применение М в рассуждениях даст недостоверный результат.
Одна только «корректность всех логических переходов» не гарантирует достоверность доказательства.
Необходимы так же достоверность исходных данных и логическая обоснованность самих переходов.
Методы не могут быть заранее предопределены:) Существуют множества, в том числе и еще неизвестные, доказательств одних и тех же утверждений.
Все сводится к созданию этого «набора», но проблема в том, что этот набор по-определению уже будет неполон в силу искусственности своего происхождения.
Речи о том, что формализовать существующие доказательства нельзя — не было. Речь о том, что в общем случае, алгоритмизировать доказательство произвольных суждений пока что невозможно, а соответственно любая работа в этом направлении пока что лишена смысла в силу.
Именно. Любая подобная программа будет работать с уже выбранными автором методами и пытаться искать «ошибки» в уже сформированном доказательстве. В общем случае, алгоритмически правильно обосновать правильность выбора каждого метода равносильно задаче автоматически доказывать произвольные математические утверждения, что равносильно созданию, даже не «искусственного», интеллекта.
Машина Тьюринга, строго говоря, это и есть математическое определение алгоритма. А доказательство произвольных суждений, в общем случаем, вряд ли алгоритмически реализуемая на настоящий момент, задача.
Не может иметь это смысла.