Ключевое слово
29 | 03 | 2024
Новости Библиотеки
Шахматы Онлайн
Welcome, Guest
Username: Password: Remember me

TOPIC: Gödel's Theorem: An Incomplete Guide to Its Use and Abuse

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 28 Март 2011 12:08 #181

  • Serge_P
  • Serge_P's Avatar
  • OFFLINE
  • Бояринъ
  • Posts: 1568
  • Thank you received: 6
  • Karma: 1
Serge_P написал(а):
Alexander написал(а):
И вероятно никакой его конечный кусок не должен обладать избыточной информацией
Нет, для бесконечных (псевдо)случайных последовательностей этот номер не пройдет. Если взять, скажем, десятичное разложение числа
с достаточной точностью, то, скорее всего, где-нибудь там найдется, к примеру, кусок длины 100 из одних нулей (сам не проверял, и не собираюсь
).

Такой подход (последовательность случайна, если ее нельзя сжать архиватором) хорошо работает для конечных последовательностей.
Впрочем, если конечный кусок означает начальный кусок последовательности до какого-то N, а не любой кусок откуда-либо, то тогда согласен.
Last Edit: 27 Март 2015 13:02 by Vladimirovich.

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 28 Март 2011 15:23 #182

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Serge_P написал(а):
если конечный кусок означает начальный кусок последовательности до какого-то N, а не любой кусок откуда-либо, то тогда согласен
Как обоснуется?

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 28 Март 2011 16:08 #183

  • Serge_P
  • Serge_P's Avatar
  • OFFLINE
  • Бояринъ
  • Posts: 1568
  • Thank you received: 6
  • Karma: 1
Хайдук написал(а):
Как обоснуется?
Насколько мне известно, это не доказано, но считается верным на основании вычислений с уже известными знаками.

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 28 Март 2011 16:25 #184

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Наш друг инфолиократ опять, видимо, поплел в деревню с тестем собирать картошку и интернет пропал
. А то иначе дискуссия, должно быть, заинтересовала бы его

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 03 Апр 2011 01:30 #185

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Serge_P написал(а):Да, в этом духе, называют их, видимо, left-computably enumerable reals. Может left- потому, что могут вычислить первые/левые цифры после запятой
. Согласно ссылке, можно ввести обычную вероятностную меру на пространстве Кантора всех бесконечных бинарных последовательностей. В результате оказывается, что некоторое подпространство последних (чьи начальные конечные отрезки представляют собой останавливающиеся, подходящим образом подогнанные (prefix-free) бинарные программы) обладает мерой, выразимой left-computably enumerable реальным числом, которое НЕ вычислимо формулой/алгоритмом по причине алгоритмической неразрешимости проблемы остановки всех (счётно-бесконечных) программ.

По мне, все это не слишком интересно или глубоко. Можно безнадёжно увязнуть в болоте несчётного числа (!) невычислимых алгоритмом чисел/последовательностей и всуе норовить застукать кто случайнее или невычислимее, вроде якобы супер Омеги по ссылке


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


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

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 05 Апр 2011 18:43 #186

  • Serge_P
  • Serge_P's Avatar
  • OFFLINE
  • Бояринъ
  • Posts: 1568
  • Thank you received: 6
  • Karma: 1
Хайдук написал(а):
По мне, все это не слишком интересно или глубоко.
Тоже думаю, что на досуге можно в этом покопаться, а серьезно влезать не следует...

Хайдук написал(а):
В то время как можно понять почему гипотеза континуума оказалась неразрешимой
А как это понять? В смысле, вы знаете какое-нибудь интуитивное объяснение этому факту?

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 06 Апр 2011 03:36 #187

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Хайдук написал(а):
В то время как можно понять почему гипотеза континуума оказалась неразрешимой
Serge_P написал(а):
А как это понять? В смысле, вы знаете какое-нибудь интуитивное объяснение этому факту?
Сам Коэн как-будто считал, что гипотеза континуума должна оказаться в конце концов ошибочной, скачок от счётного к континууму казался ему слишком большим. Однако после того, как элементарное +1 уже не может обеспечить рост мощности, все карты ложатся на стол, так сказать, anything goes. алеф_1 следует за счётным по определению и благодаря аксиоме выбора/вполне упорядочению. Но принцип образования континуума как-бы совершенно/независимо
с неба свалился, как присобачить, где найти ему место? Вот и не могут найти, вроде не имеет ничего общего с +1 и потому трудно/нельзя прикинуть насколько бОльше счётного +1. Разумеется, настоящее понимание немыслимо без углубления в труднодоступные детали метода вынуждения Коэна. Полагаю, что многие большие мощности (large cardinals) разделяют судьбу гипотезы континуума и бывает трудно зафиксировать им место на шкале мощностей или по отношению друг к другу
. Такого можно добиться определением, что не очень интересно, ибо надуманно и тавтологично. К примеру, первый недостижимый кардинал по определению бОльше континуума любой меньшей мощности и является верхним пределом объединений любой меньшей мощности любых меньших множеств
. Бывает и масса других, ещё бОльших мощностей - измеримых, огромных/huge, компактных, суперкомпактных, имени Hugh Woodin-а и т.д. - про которыe ничегошеньки не знаю

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 06 Апр 2011 16:11 #188

  • Serge_P
  • Serge_P's Avatar
  • OFFLINE
  • Бояринъ
  • Posts: 1568
  • Thank you received: 6
  • Karma: 1
Хайдук написал(а):
Бывает и масса других, ещё бОльших мощностей - измеримых, огромных/huge, компактных, суперкомпактных, имени Hugh Woodin-а и т.д. - про которыe ничегошеньки не знаю
Тоже особо ничего не знаю про эти вещи.

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 13 Апр 2011 16:37 #189

  • limarodessa
  • limarodessa's Avatar
  • OFFLINE
  • Доцент
  • Posts: 16793
  • Thank you received: 79
  • Karma: -22
en.wikipedia.org/wiki/Closed_timelike_curve
In mathematical physics, a closed timelike curve (CTC) is a worldline in a Lorentzian manifold, of a material particle in spacetime that is closed, returning to its starting point. This possibility was first raised by Kurt Gdel in 1949, who discovered a solution to the equations of general relativity (GR) allowing CTCs known as the Gdel metric; and since then other GR solutions containing CTCs have been found, such as the Tipler cylinder and traversable wormholes. If CTCs exist, their existence would seem to imply at least the theoretical possibility of time travel backwards in time
Last Edit: 27 Март 2015 13:02 by Vladimirovich.

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 14 Апр 2011 02:58 #190

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Вот что пришло в башку: почему бы не проверить ... компом реальную силу некоторых привлекательных аксиоматических систем?
Матлогикам можно попытаться перевести уже наличные и общепринятые гламурные доказательства в некоторую популярную аксиоматическую систему, закодированную в компе. В ходе попыток станет ясно хватает ли системы, дабы доказать результат или тот выходит за её пределы по Гёделю. Если выходит, выяснится какие ещё специфические аксиомы нужно добавить, чтобы заполучить результат.

На этом пути поджидают каверзные трудности, однако. Лучше всего сформулировать на языке аксиом/компа искомую теорему и добиться высокой степени убеждения, что теорема компа совпадает в достаточной степени с нашим интуитивным пониманием её. Потом остаётся только найти компом дедуктивный путь от аксиом до теоремы. Ошибиться или соврать комп не даст, даже если не понимаем до конца того, что он делает с нашей помощью. Мы не можем себе позволить интерпретировать выкладки компа и на ходу менять его аксиоматическую базу, потому что вероятность ошибиться в интерпретациях большая. Как раз потому важно зафиксировать с самого начала теорему на языке компа и приложить усилия понять только её. Потом не важно будет понимать все детали дедуктивного процесса компом, важно будет лишь, чтобы они привели к конечной цели. Комп ошибиться не может и если причалит к теореме, значит она доказуема из его аксиом. А если не подходит к неё и начнём ковырять его аксиомы, то тем самым улетучиваются строгость его вкладок и стоимость всего упражнения, ибо нет гарантий, что не допустили ошибок при модификациях под воздействием ненадёжных интерпретаций сходу того, ЧТО он должен делать


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

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 14 Апр 2011 19:28 #191

  • Serge_P
  • Serge_P's Avatar
  • OFFLINE
  • Бояринъ
  • Posts: 1568
  • Thank you received: 6
  • Karma: 1
Хайдук написал(а):
Вот что пришло в башку: почему бы не проверить ... компом реальную силу некоторых привлекательных аксиоматических систем?
Матлогикам можно попытаться перевести уже наличные и общепринятые гламурные доказательства в некоторую популярную аксиоматическую систему, закодированную в компе. В ходе попыток станет ясно хватает ли системы, дабы доказать результат или тот выходит за её пределы по Гёделю. Если выходит, выяснится какие ещё специфические аксиомы нужно добавить, чтобы заполучить результат.

На этом пути поджидают каверзные трудности, однако. Лучше всего сформулировать на языке аксиом/компа искомую теорему и добиться высокой степени убеждения, что теорема компа совпадает в достаточной степени с нашим интуитивным пониманием её. Потом остаётся только найти компом дедуктивный путь от аксиом до теоремы. Ошибиться или соврать комп не даст, даже если не понимаем до конца того, что он делает с нашей помощью. Мы не можем себе позволить интерпретировать выкладки компа и на ходу менять его аксиоматическую базу, потому что вероятность ошибиться в интерпретациях большая. Как раз потому важно зафиксировать с самого начала теорему на языке компа и приложить усилия понять только её. Потом не важно будет понимать все детали дедуктивного процесса компом, важно будет лишь, чтобы они привели к конечной цели. Комп ошибиться не может и если причалит к теореме, значит она доказуема из его аксиом. А если не подходит к неё и начнём ковырять его аксиомы, то тем самым улетучиваются строгость его вкладок и стоимость всего упражнения, ибо нет гарантий, что не допустили ошибок при модификациях под воздействием ненадёжных интерпретаций сходу того, ЧТО он должен делать


Я думаю, что при таком подходе воочию обнаружится недоказуемость многих теорем в рамках якобы многообещающих аксиоматических систем и станет ясно, что истина дана нам непосредственно, вне какой-либо ... логики, как учил нас Гёдель
Думаю, что на практике это явно неподъемная задача. Например, доказательство теоремы Ферма и так то занимает сотни страниц, а представьте что будет если записать его как цепочку утверждений в формальной теории?.. Сколько времени потребуется, чтобы перебрать все доказательства подобной длины?

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

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 14 Апр 2011 19:29 #192

  • Serge_P
  • Serge_P's Avatar
  • OFFLINE
  • Бояринъ
  • Posts: 1568
  • Thank you received: 6
  • Karma: 1
limarodessa написал(а):
In mathematical physics, a closed timelike curve (CTC) is a worldline in a Lorentzian manifold, of a material particle in spacetime that is closed, returning to its starting point. This possibility was first raised by Kurt Gdel in 1949, who discovered a solution to the equations of general relativity (GR) allowing CTCs known as the Gdel metric; and since then other GR solutions containing CTCs have been found, such as the Tipler cylinder and traversable wormholes. If CTCs exist, their existence would seem to imply at least the theoretical possibility of time travel backwards in time
Однако, Теорема Гёделя тут явно ни при чем


Помнится, у Брайана Грина про это все весьма неплохо написано.

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 14 Апр 2011 20:49 #193

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Serge_P написал(а):
у Брайана Грина про это все весьма неплохо написано
Брайана Грина не читал в полноте, хотя обе его книги у меня есть (одну одолжил и, кажется, не вернули). Кстати, только-что вышла третья, про множественные вселенные и т.п. Буду ждать год, пока выдет мягкой оболочкой, а то hardcover не люблю


Про это все весьма неплохо написал и Sean Carroll в From Eternity to Here: The Quest for the Ultimate Theory of Time. Как раз читаю щас, очень интеллигентно написанная и углублённая книжка
. Скажем, впервые чёрным по белому встретил признание, что существует намного бОльше чего, чем доступно путём (неизбежно локальных, по-видимому) эмпирических опыта с экспериментами (это про квантовую механику).

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 15 Апр 2011 02:20 #194

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Serge_P написал(а):
Думаю, что на практике это явно неподъемная задача. Например, доказательство теоремы Ферма и так то занимает сотни страниц, а представьте что будет если записать его как цепочку утверждений в формальной теории?..  Сколько времени потребуется, чтобы перебрать все доказательства подобной длины?
Речь не о поиске компьютером самому доказательства, а о переложении уже найденного математиками существующего доказательства. Такая формальная версия будет намного длинее, конечно, но зато должна помочь оценить выразимо ли интуитивное доказательство в формальной системе. Может некоторые структуры существующего доказательства окажутся невыразимыми формальным языком компа, что бросит тень сомнения на принципиальную доказуемость теоремы в данной формальной системе (см. ниже). Во всяком случае подобный подход уже использовали для проверки правильности наличного (содержащего компьютерные вычисления!) доказательства теоремы о 4-ёх красках. Там комп сумел проложить путь от аксиоматической базы до утверждения теоремы


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

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 15 Апр 2011 18:31 #195

  • Serge_P
  • Serge_P's Avatar
  • OFFLINE
  • Бояринъ
  • Posts: 1568
  • Thank you received: 6
  • Karma: 1
Хайдук написал(а):
Такая формальная версия будет намного длинее, конечно, но зато должна помочь оценить выразимо ли интуитивное доказательство в формальной системе.
Ну, вроде как, среди математиков никто не сомневается, что выразимо. Если, конечно, под интуитивным доказательством имеется в виду цепочка не вполне строгих рассуждений, которую, однако, каждый квалифицированный математик может сделать вполне строгой (удлинив доказательство в несколько раз), если будет очень надо.

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 16 Апр 2011 03:01 #196

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Serge_P написал(а):
вроде как, среди математиков никто не сомневается, что выразимо
Не факт. Гёделевы предложения напрашиваются как несомненные арифметические истины и выразимы в формальной арифметике, но тем не менее их доказательства НЕ выразимы. Стоит ещё добавить, что в формальной арифметике всегда существуют НЕ имеющие решения диофантовые уравнения такие, что отсутствия у них решения нельзя доказать в формальной арифметике
. Потому представляется, что не можем быть наперёд уверены в силе конкретной, заданной аксиоматической системы.

Я понимаю, что перевод известного доказательства в формальную систему суть громоздкое дело, но как раз компьютер должен в этом помочь. Матлогик на глаз выбирает формальные структуры, которые кажутся ему адекватно отвечающими структурам интуитивного доказательства. Комп принимает только то, что формально правильно, а матлогик старается интерпретировать то, что одобрил комп и увязать с этапами интуитивного доказательства. Если на этом пути можно добраться до формального выражения искомой теоремы, то она оказывается доказуемой в формальной системе компа; вдогонку даже проверили/верифицировали правильность/безошибочность интуитивного доказательства
. Интерпретациям промежуточных формальных структур не следует придавать большого значения, потому что могут быть неадекватными или ошибочными. Если, однако, не удаётся застукать конечный формальный результат, то придётся пристальнее посмотреть на эти представления и выявить проблемы несходимости формального доказательства. Менять лёгкой рукою саму формальную систему, дабы сошлась к желанному результату, сильно НЕ рекомендуется ввиду неконтролируемого возрастания энтропии интерпретаций и значит вероятности фатальных ошибок, а также снижения надёжности или даже угрозы утраты непротиворечивости самой формальной системой/компом

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 16 Апр 2011 05:22 #197

  • infoliokrat
  • infoliokrat's Avatar
  • OFFLINE
  • Инфолиократ
  • Posts: 1288
  • Thank you received: 2
  • Karma: 0
Serge_P написал(а):
Я думаю, что при таком подходе воочию обнаружится недоказуемость многих теорем в рамках якобы многообещающих аксиоматических систем и станет ясно, что истина дана нам непосредственно, вне какой-либо ... логики, как учил нас ГёдельДумаю, что на практике это явно неподъемная задача. Например, доказательство теоремы Ферма и так то занимает сотни страниц, а представьте что будет если записать его как цепочку утверждений в формальной теории?.. Сколько времени потребуется, чтобы перебрать все доказательства подобной длины?
Ну и, кстати говоря, убедиться в недоказуемости какой-либо теоремы подобным образом принципиально нельзя: мы никогда не можем быть уверены, что доказательство теоремы не находится среди тех доказательств, до которых комп еще не добрался.
Serge_P написал(а):
скорее всего, где-нибудь там найдется, к примеру, кусок длины 100 из одних нулей (сам не проверял, и не собираюсь ).
Такой подход (последовательность случайна, если ее нельзя сжать архиватором) хорошо работает для конечных последовательностей.Впрочем, если конечный кусок означает начальный кусок последовательности до какого-то N, а не любой кусок откуда-либо, то тогда согласен
Во какая прелесть! И тут диктуют погоду!
По цитатам (навскидку): на сайте школьницы о числе
отмечено, что любая мыслимая комбинация (конечная !) цифр любых (в т.ч. и подряд) в нем прячется (предположительно имеется).

Школьникам показывал псевдослучайность так: комп (от Корвета до любого современного)только одно конкретное случайное первым выдает после включения... Но это может быть как раз и значит, что в будущих соответствующих программах все подобные трудности не трудности, а пыль, не заслуживающая особого внимания, ведь согласимся, что в решениях (компьютарных любых задач, хоть эвристических, философских, юридических, научно-коммунистических= неестественных наук) все определяется не возможностями математики (тут я патриот даже нынешней математики!, а софтом (железным и мягким). И, по инфолиоподходу, третьим софтом, субъективным,
Помню, как был поражен, что для доказательства основной теоремы равнобедренного трехугольника ЭВМ не опусказа высоту с его вершины, а просто использовала зеркальное отражение его же! (Типа: Тассмотрим треугольник АВС и треугольник АСВ. Против равных сторон = равные углы.
это вместо квадратика=теорема доказана )

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 16 Апр 2011 05:40 #198

  • infoliokrat
  • infoliokrat's Avatar
  • OFFLINE
  • Инфолиократ
  • Posts: 1288
  • Thank you received: 2
  • Karma: 0
написал(а):
в будущих соответствующих программах все подобные трудности не трудности, а пыль, не заслуживающая особого внимания, ведь согласимся, что в решениях (компьютарных любых задач, хоть эвристических, философских, юридических, научно-коммунистических= неестественных наук) все определяется не возможностями математики (тут я патриот даже нынешней математики!, а софтом (железным и мягким). И, по инфолиоподходу, третьим софтом, субъективным,
Т.е. на решение ЭВМ (точность, скорость, достижимость ... и прочая прочая) влияет железо, программа и постановка задачи, инчае софт жесткий, мягкий и человеческий фактор- гомо сапиенс, можно сокращенно и так:
жемягософт Результат зависит не только от того, какое решение определяется по условию, не только от исполнителя: устройств или/и программы но и от того
кто определяет, кто дает команды... Проще: как экскаватор быстрее копает траншею, так и комп (будущий быстрее и лучше, точнее и красивее) решает задачи, доказывает теоремы, создает стихи, музыку, картины (из пикселов и без травы или/и грибов, без гипноза и снов, без любви-химии)

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 16 Апр 2011 23:41 #199

  • Serge_P
  • Serge_P's Avatar
  • OFFLINE
  • Бояринъ
  • Posts: 1568
  • Thank you received: 6
  • Karma: 1
Хайдук написал(а):
Serge_P написал(а):
вроде как, среди математиков никто не сомневается, что выразимо
Не факт. Гёделевы предложения напрашиваются как несомненные арифметические истины и выразимы в формальной арифметике, но тем не менее их доказательства НЕ выразимы. Стоит ещё добавить, что в формальной арифметике всегда существуют НЕ имеющие решения диофантовые уравнения такие, что отсутствия у них решения нельзя доказать в формальной арифметике
. Потому представляется, что не можем быть наперёд уверены в силе конкретной, заданной аксиоматической системы.

Я понимаю, что перевод известного доказательства в формальную систему суть громоздкое дело, но как раз компьютер должен в этом помочь. Матлогик на глаз выбирает формальные структуры, которые кажутся ему адекватно отвечающими структурам интуитивного доказательства. Комп принимает только то, что формально правильно, а матлогик старается интерпретировать то, что одобрил комп и увязать с этапами интуитивного доказательства. Если на этом пути можно добраться до формального выражения искомой теоремы, то она оказывается доказуемой в формальной системе компа; вдогонку даже проверили/верифицировали правильность/безошибочность интуитивного доказательства . Интерпретациям промежуточных формальных структур не следует придавать большого значения, потому что могут быть неадекватными или ошибочными. Если, однако, не удаётся застукать конечный формальный результат, то придётся пристальнее посмотреть на эти представления и выявить проблемы несходимости формального доказательства. Менять лёгкой рукою саму формальную систему, дабы сошлась к желанному результату, сильно НЕ рекомендуется ввиду неконтролируемого возрастания энтропии интерпретаций и значит вероятности фатальных ошибок, а также снижения надёжности или даже угрозы утраты непротиворечивости самой формальной системой/компом
Я имел в виду скорее нормальные математические доказательства (ну, в смысле, в комбинаторике, теории чисел, топологии, и т.д.), а не ужасы из недр современной матлогики


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

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 17 Апр 2011 17:35 #200

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Serge_P написал(а):
имел в виду скорее нормальные математические доказательства (ну, в смысле, в комбинаторике, теории чисел, топологии, и т.д.), а не ужасы из недр современной матлогики
Нормальные доказательства всегда опираются на достаточных для вывода некоторой теоремы аксиомах, конечно. Однако может быть, что эти аксиомы все-таки разные для разных теорем, хотя на интуитивном, хоть и строгом уровне это трудно заметить. Очевидные, но недоказуемые Гёделевы предложения как-будто свидетельствуют о таких возможностях. По-видимому, от Гёделевой неполноты нельзя отделаться за счёт никаких, сколь угодно сильных (по числу и качеству доказуемых следствий) аксиоматических систем. Потому и представляется интересным проверить доказуемость гламурного результата гламурной аксиоматикой


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

Вот интересно как застукать наперёд потенциально неразрешимые/недоказуемые проблемы? Скажем, ясно (почему?), что гипотеза о бесчисленности пар простых-близнецов (p и p+2) НЕ может быть неразрешимой, на интуитивном уровне у неё должно быть однозначное решение: или пар таких конечное число, или их бесчисленно/счётно много. В некоторых аксиоматиках гипотеза может быть неразрешимой, конечно, но эти аксиоматики заведомо должны выглядеть неудовлетворительными, бедными, игрушечными, неестественными. Любая аксиоматика, претендующая на адекватное представление нашей интуиции, а также математической реальности, должна однозначно разрешать гипотезу простых-близнецов, потому что решение это как-бы уже существует out there и нам остаётся лишь его найти. Полагаю, такое хитрое положение вещей имеет прямое отношение к счётности вопросных математических объектов/структур (то бишь натуральных чисел, в нашем случае). В заметном и фундаментальном отличии, однако, гипотеза континуума затрагивает существенно несчётную структуру, а там само понятие математического существования уже другое, обычная логика (счётного) уже не работает. Как раз потому и можно было ожидать неразрешимости гипотезы континуума

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 17 Апр 2011 23:33 #201

  • Serge_P
  • Serge_P's Avatar
  • OFFLINE
  • Бояринъ
  • Posts: 1568
  • Thank you received: 6
  • Karma: 1
Хайдук написал(а):
Нормальные доказательства всегда опираются на достаточных для вывода некоторой теоремы аксиомах, конечно. Однако может быть, что эти аксиомы все-таки разные для разных теорем, хотя на интуитивном, хоть и строгом уровне это трудно заметить.
Нормальной математике много не надо - целые числа, действительные числа, да наивная теория множеств. Ну, правда, мы знаем, что в основаниях кое-где запрятана Аксиома Выбора вместе с прочей ZF, но по этому поводу уже давно никто не парится. А когда вдруг для доказательства приходится использовать что-то более экзотическое, типа трансфинитной индукции, тогда, разумеется, все проверяют такого рода рассуждения с утроенным вниманием. Вообще говоря, не думаю, что в нормальных теоремах вдруг неожиданно могут всплыть какие-то гёделевские штучки.

Хайдук написал(а):
Лучше работать дружно, сразу отчеканивая формальные выкладки и сравнивая их интерпретации с частями интуитивного доказательства.
Думаю, что работа по формальной записи доказательства (так, чтоб можно было скормить компу) сравнима по объему c проверкoй этого доказательства.

Хайдук написал(а):
потому что решение это как-бы уже существует out there и нам остаётся лишь его найти.
Ну это заманчивое рассуждение, конечно... А чем проблема континуума тогда хуже? Отрезок [0,1] он тоже out there, какие-то точки выкинуть, какие-то оставить, всего делов...

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 18 Апр 2011 04:53 #202

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Serge_P написал(а):
Думаю, что работа по формальной записи доказательства (так, чтоб можно было скормить компу) сравнима по объему c проверкoй этого доказательства.
По большому счёту это так, но вот что вспомнил: работая дружно с компом, НЕ обязательно скармливать ему на 100%. Можно предлагать компу самому найти/восстановить достаточно маленькие шаги доказательства, задавая промежуточные формальные цели; если компу не удаётся достичь этих скромных целей, можно уменьшить шаг и заказать ему ещё более скромные рубежи

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 18 Апр 2011 16:05 #203

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Serge_P написал(а):
Нормальной математике много не надо - целые числа, действительные числа, да наивная теория множеств. Ну, правда, мы знаем, что в основаниях кое-где запрятана Аксиома Выбора вместе с прочей ZF, но по этому поводу уже давно никто не парится. А когда вдруг для доказательства приходится использовать что-то более экзотическое, типа трансфинитной индукции, тогда, разумеется, все проверяют такого рода рассуждения с утроенным вниманием. Вообще говоря, не думаю, что в нормальных теоремах вдруг неожиданно могут всплыть какие-то гёделевские штучки.
Выглядит правдоподобно, что ZFC (ZF + Аксиома Выбора) сможет прибрать к рукам всю математику за исключением гёделевских штучек, хотя мало-кто утруждался такое продемонстрировать компом. Даже напротив - неразрешимые арифметикой Пеано, но более содержательные результаты вроде обобщённой комбинаторной теоремы Рамсея (Дж.Парис, Л.Харрингтон) вполне доказуемы в более сильных аксиоматиках, тем более в ZFC. Можно ожидать, однако, дальнейших подлинных (то бишь интуитивных) неразрешимостей в ZFC (вкупе с высшими мощностями, large cardinals) наподобие гипотезы континуума.

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 18 Апр 2011 16:19 #204

  • Serge_P
  • Serge_P's Avatar
  • OFFLINE
  • Бояринъ
  • Posts: 1568
  • Thank you received: 6
  • Karma: 1
Хайдук написал(а):
Можно ожидать, однако, дальнейших подлинных (то бишь интуитивных) неразрешимостей в ZFC (вкупе с высшими мощностями, large cardinals) наподобие гипотезы континуума.
Может и накопают чего. Но вряд ли это сильно повлияет на нормальную математику. К примеру, я что-то не помню, где реально нужны множества мощности больше 2^c.

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 18 Апр 2011 16:34 #205

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Некоторые подозревают, что NP P неразрешима
. К сожалению, я плохо понимаю эту проблему. По поводу недавнего ажиотажа вокруг её будто-бы решения неким (паршивым
) индусом Вы, Сергей, дали хорошие ссылки, но я не воспользовался

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 18 Апр 2011 17:26 #206

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Хайдук написал(а):
потому что решение это как-бы уже существует out there и нам остаётся лишь его найти
Serge_P написал(а):
А чем проблема континуума тогда хуже? Отрезок [0,1] он тоже out there, какие-то точки выкинуть, какие-то оставить, всего делов...
Счётное по определению конструктивно, алгоритмично, перечислимо, если не разрешимо, а с несчётным дела намного хуже
- оно как-бы НЕ количество, а качество, идея, концепция. А идеи птички свободные, могут быть любыми, произвольными, anything goes...

Кстати, вот никак не могу себе представить континуума Суслина, как же может у того не быть всюду плотного счётного подмножества?
Такое должно влачит за собой неметризуемость, неизмеримость и всю остальную сволочь

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 18 Апр 2011 23:20 #207

  • Serge_P
  • Serge_P's Avatar
  • OFFLINE
  • Бояринъ
  • Posts: 1568
  • Thank you received: 6
  • Karma: 1
Хайдук написал(а):
Некоторые подозревают, что NP P неразрешима
. К сожалению, я плохо понимаю эту проблему. По поводу недавнего ажиотажа вокруг её будто-бы решения неким (паршивым ) индусом Вы, Сергей, дали хорошие ссылки, но я не воспользовался
В википедии (en.wikipedia.org/wiki/P_versus_NP_problem) все эти ссылки есть, там вообще про P/NP вполне грамотно написано, imho.

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

Хайдук написал(а):
Кстати, вот никак не могу себе представить континуума Суслина, как же может у того не быть всюду плотного счётного подмножества? Такое должно влачит за собой неметризуемость, неизмеримость и всю остальную сволочь
Я в этом плохо разбираюсь. Но влачить вышеперечисленное оно, конечно, может.
Last Edit: 27 Март 2015 13:03 by Vladimirovich.

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 20 Апр 2011 17:25 #208

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16
Serge_P написал(а):
Множество действительных чисел ведь строится через множество рациональных (через, к примеру, дедекиндовы сечения). Так что, все-таки, остаются вопросы, почему одна бесконечность сложнее другой...
Счётная бесконечность минимальная, так сказать, порождённая интуитивно фундаментальным +1, дальше/ниже уж некуда
. Идентификация/отделение/застукивание или выбор какого-либо (тем более бесконечного счётного) подмножества из счётной бесконечности это совсем другая идея, если задуматься, может вполне непротиворечивая и значит (математически) легитимная, но - другая, независимая по смысловому содержанию, к чему в конце концов и достучались Коэн с Гёделем до этого.

Serge_P написал(а):
А чем проблема континуума тогда хуже? Отрезок [0,1] он тоже out there, какие-то точки выкинуть, какие-то оставить, всего делов...
Отрезок напрашивается фиксированным, застывшим существованием, но как сплошная, неделимая протяжённость. Безусловно естественная нужда наделить точечной структурой вынуждает, однако, ту же вышеупомянутую и независимую от счётного +1 концепцию

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 25 Апр 2011 11:25 #209

  • limarodessa
  • limarodessa's Avatar
  • OFFLINE
  • Доцент
  • Posts: 16793
  • Thank you received: 79
  • Karma: -22
Заходят Вернер Гейзенберг, Курт Гёдель и Ноам Хомский в бар.
Гейзенберг смотрит по сторонам и говорит: «Поскольку здесь находимся мы втроём, и поскольку здесь бар, то это — наверняка анекдот. Однако, остаётся один вопрос — смешной он или нет?»
Гёдель на секунду задумывается и отвечает: «Ну, так как мы находимся внутри анекдота, мы не можем сказать, смешной он или нет. Чтобы это понять, нам нужно взглянуть на него снаружи».
Хомский смотрит на них и говорит: «Конечно же, он смешной. Вы просто неправильно его рассказываете.»

======================

Два математика в ресторане поспорили, насколько хорошо знают математику большинство людей.
Один (пессимист) утверждал, что большинство ее вообше не знает, а другой (оптимист) — что хоть и не много, но знают.
Когда пессимист отошел в туалет, оптимист подозвал симпатичную официантку–блондинку и говорит:

— Когда мой коллега вернется, я задам вам вопрос. Суть не важна. Все, что вы должны сделать — это сказать Треть икс куб.
— Как–как? Третий скуп? — переспрашивает официантка?
— Да нет, Треть Икс Куб, Понятно?
— А–а! Третик скуп? — повторяет официантка.
— Да, да. Это все, о чём я вас прошу.

Официантка уходит, твердя про себя фразу Третик скуп. Тут возвращается пессимист.
Оптимист говорит — давай спросим у нашей официантки, чему равен какой–нибудь простенький интеграл.
Пессимист, со смехом соглашается. Оптимист вызывает официантку и спрашивает:
— Извините, вы не помните случайно, чему равен интеграл от x^2 по dх?
— Треть икс куб… — с готовностью отвечает официантка.
Пессимист сильно удивлен, оптимист весело смеется.
Официантка отходит на несколько шагов и, обернувшись через плечо, добавляет:
— Плюс константа.

Отредактировано limarodessa (2011-04-25 15:27:51)

Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 25 Апр 2011 14:23 #210

  • Хайдук
  • Хайдук's Avatar
  • OFFLINE
  • Наместник
  • Posts: 49331
  • Thank you received: 130
  • Karma: 16

Moderators: Grigoriy
Рейтинг@Mail.ru

Научно-шахматный клуб КвантоФорум