Теоремы о превосходстве

[lex_kravetski]

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

Comments

[iv_an_ru]

> Гёдель не сможет доказать утверждение 1.

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

[lex_kravetski]

> Конечно. Он же помер почти пол-века назад.

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

[iv_an_ru]

Я не вижу никакого математического доказательства. Вы не задали ни аксиоматику для понятия "Гёдель", ни правила вывода.

[lex_kravetski]

> Вы не задали ни аксиоматику для понятия "Гёдель", ни правила вывода.

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

[razorbck]

Поздравляю, Лекс! Ты только что математически доказал, что любая произвольно выбранная группа людей может быть объективно неполноценной. Гитлер вертится в гробу от зависти :-)

[lex_kravetski]

Вы не докажете, что я это доказал - я буду всё отрицать!

[ext_5312370]

Спасибо.

ПС
Ведь будет же вторая часть с разоблачением ;)
> Существуют такие утверждения, которые принципиально не может доказать [заведомо заданный] непротиворечивый автомат.

[lex_kravetski]

> Ведь будет же вторая часть с разоблачением

[ext_5312370]

Короче

[lex_kravetski]

> На самом деле (говоря более современным языком) Гёдель построил следующий объект:

unsolvable = can_proof(unsolvable) == false
can_proof(unsolvable) = ?

Хм. Давайте попробуем на этот объект взглянуть.

Поскольку к unsolvable присваивается результат сравнения, его тип - Bool. Таким образом, возможные значения unsolvable - true или false.

То есть can_proof тоже принимает булевское значение: сan_proof(true) или can_proof(false).

При этом unsolvable используется до инициализации. Поэтому реально can_proof примет какую-то неинициализированную переменную булевского типа.

Очень, очень интересный объект. Гораздо более интересный, чем у меня в статье. И чем у Гёделя.

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

[unx0r]

<<Так вот, возьмём эту вашу функцию canProve и попытаемся её озадачить вот таким вот утверждением.

Утверждение 1:

canProve(утверждение 1) == false

Ну или, если записать это на разговорном языке…

Утверждение 1:

Этот ваш автомат не сможет доказать утверждение 1.

Теперь смотрите.

Если автомат сможет доказать утверждение 1, то тем самым он докажет утверждение о том, что он не может доказать утверждение 1.

>>

Ну или, если записать это на разговорном языке…

Это так нынче логику учат?

<<Однако смотрите, автомат не сможет доказать утверждение 1, но мы-то в это время как раз доказали, что он не сможет! Как вам такое?>>

[lex_kravetski]

> Это так нынче логику учат?

В смысле «нынче»? Она такой всегда была: утверждение на разговорном языке может быть записано символами и это будет полный эквивалент этого утверждения.

[sumisokomashiro]

эта статья про хохлов или про израиль? не совсем понятно

Можно доказать, что есть такие статьи

[avb]

которые не про хохолов и не про Израиль. Парадоксально, но факт.