Ни о какой безапелляционности в моих высказываниях не может быть и речи!

Если доказательство есть, его можно найти и предъявить за конечное время, например, перебирая все доказательства по порядку ;) Теоремы Геделя демонструруют несколько другие вещи.

From:

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

From:

и тогда программа поиска, собственно, не является алгоритмом, ибо последний финитен по определению.

From:

Э, между «мы не знаем, есть ли у этого доказательство», «у этого есть доказательство, но его нельзя найти» и «это правда, но доказательства этого не существует» есть разница.

From:

rakshas.livejournal.com

Какой контраст с предыдущей записью :)

From:

abvgd.livejournal.com

но работать-то что ему мешает бесконечно?

A: GOTO A

From:

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

From:

Несоменно, есть; но я ничего про третий вариант и не говорил.

From:

В том-то и дело, а 1 Т. Г. о неполноте строит именно третий вариант. Из нее следует, что возможен первый вариант, т.е. нет алгоритмического способа определить, доказуемо ли некое утверждение. Второй вариант вроде бы просто всегда неверен.

From:

Первая теорема о неполноте не утверждает, что "это правда, но доказательства не существует", она вообще не занимается вопросом истинности. Есть способ ее доказать (не тот, которым пользовался Гедель), который движется этим путем, но он доказывает очень слабый ее вариант.

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

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

From:

Почему же слабый? Насколько я помню, Гедель строит утверждение G, говорящее, что утверждение G невыводимо (нумеруя утверждения и выводы так, что G равносильно утверждению о том, что определенное целое число имеет определенное свойство). Об истинности здесь и правда ничего не говорится, но G таки будет истинно в любой модели. Или я вообще ничего не понимаю ;)

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

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

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

From:

ipain.livejournal.com

алгоритм получения бесконечно работающей программы финитен ли?

From:

G "мета-истинно". Или "интуитивно истинно". Его истинность не используется в доказательстве, и доказательство проходит для теорий, у которых вообще нет естественной семантики.

Есть способ док-ва теоремы, который действительно использует истинность G, но тогда предполагается, что есть естественная модель и исходная теория T в ней доказывает только истинные утверждения (тогда то, что T не опровергает G, становится очевидным, и другие части док-ва упрощаются). Но это очень сильное условие, намного сильнее омега-непротиворечивости Геделя или просто непротиворечивости (в версии Россера).

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

В первоначальных доказательствах; но потом стало ясно, что оно также легко следует из первой теоремы, сформулированной для подходящей конечно аксиоматизированной теории (если теория T конечно аксиоматизирована, то обозначая через phi конъюнкцию всех ее аксиом одной формулой, видим, что T доказывает x тогда и только тогда, когда phi->x универсальная истина).

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

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

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

Я это учил 10 лет назад и через 5 почти все забыл, так что все нормально.

From:

sowa.livejournal.com

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

From:

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

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

From:

sowa.livejournal.com

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

From:

Это следствие чтения Куайна :)

Но я могу попробовать объяснить подробнее/точнее, если мысль все же выражена слишком плохо.

From:

sowa.livejournal.com

Мне кажется, что я вашу мысль понял. Не знаю, как другие. Боюсь, что при попытке все объяснить вам придется написать введение и в теорию моделй, и в теорию доказательств.

From:

Пусть расцветают сто цветов итд. :)

From:

алгоритм финитен по определению. И этот - тоже. Хотя и не все бесконечно работающие программы можно получить с помощью алгоритма.

From:

ipain.livejournal.com

а проверить что он и правда будет бесконечно работать каким алгоритмом можно? или чем?

From: