3,14здец! (это я тебе как математик математику говорю)

(Ответить) (Thread)

Для начала, я посоветую вам книжку, которую сам недавно прочитал с большим удовольствием: Gödel’s Theorem.
An Incomplete Guide to Its Use and Abuse, by Torkel Franzén.

Теорема Гёделя - это все-таки обычная математическая теорема, утверждающая нечто о чисто комбинаторном объекте - выводах в формальных системах.

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

Для того, чтобы убедиться в непротиворечивости арифметики, теория множеств, конечно, не нужна. Что ясно хотя бы из того, что в этой непротиворечивости никто никогда не сомневался. Я подозреваю, что даже Брауэр в этом не сомневался.

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

Непротиворечива не только теория множеств ZFC, но и ZFC вместе с хотя бы первыми высшими аксиомами бесконечности (это соображение принадлежит Гёделю).

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

(Ответить) (Thread)

>Для начала, я посоветую вам книжку, которую сам недавно прочитал с
>большим удовольствием: Gödel’s Theorem.
>In Incomplete Guide to Its Use and Abuse, by Torkel Franzén.

Спасибо

>Теорема Гёделя - это все-таки обычная математическая теорема,
>утверждающая нечто о чисто комбинаторном объекте - выводах в формальных
>системах.

Я готов посморить. Как Вы ее докажете исключительно математически, не прибегая и интуитивному второму смыслу формул, и диагональному методу в конце 'это утверждение говорит: Я недоказуемо...' итд ?

>Для этого требуется ничтожный фрагмент теории множеств, никак не
>затрагиваемый никакими парадоксами.

Неважно, какого размера. Важно, что есть. Значит, уже есть выход из формализма на уровень 'наивной теории'

>Что ясно хотя бы из того, что в этой непротиворечивости никто никогда не
>сомневался. Я подозреваю, что даже Брауэр в этом не сомневался.

Хе, я тоже в этом не сомневаюсь. Но на доказательство это все таки не тянет :)

>Непротиворечива не только теория множеств ZFC, но и ZFC вместе с хотя бы
>первыми высшими аксиомами бесконечности (это соображение принадлежит
>Гёделю).

Упс... Непротиворечиваость ZFC доказана ??????????
В соответствии со второй теоремой Геделя она должна быть доказана в чем то, что принципиально мощнее, чем теория множеств. Это что ?

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

Хорошо написано
Да, пожалуй это так

(Ответить) (Parent) (Thread)

Во-первых, понятно, что здесь нет места излагать доказательство теоремы Гёделя. На самом деле, достаточно заметить, что доказательство первой теоремы Гёделя не только "математическое", но формализуемо в арифметике Пеано, которая является очень маленьким фрагментом математики. Эта формализация - часть доказательства второй теоремы Гёделя. С второй теоремой Гёделя дело обстоит аналогично.

Типичное изложение не содержит полного доказательства, откуда и возникает иллюзия махания руками у Гёделя, хотя размахивает руками автор.

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

На доказательство это не тянет? Но ведь нельзя доказать все. Какие-то утверждения нужно принять как очевидные. Непротиворечивость арифметики очевидна.

Непротиворечивость ZFC не доказана (в ZFC), а очевидна. Посмотрите Сморинского, он очень выразительно об этом пишет. (Книга отсканирована и есть в сети.) Гёдель же полагает, что раз уж мы признаем систему ZFC, то мы должны принять и, например, существование первого недостижимого кардинала. И второго.

(Ответить) (Parent) (Thread)

Thank you
I will reply on Monday (I am on a beach now, writing from an internet cafe)

(Ответить) (Parent) (Thread)

Вернувшись из рая (Cote d'Azur)

1
На самом деле, достаточно заметить, что доказательство первой теоремы Гёделя не только "математическое", но формализуемо в арифметике Пеано,

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

Причем для каждого варианта теории (с AND,NOT Или OR,Not, или NOT,=>, или XOR) и каждого варианта геделизации получатся РАЗНЫЕ теоремы изза разного кодирования. И, главное, то что некое утверждение с тесячью кванторов на сто страниц чтото означает еще - будет совсем не очевидно

2. Типичное изложение не содержит полного доказательства

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

3. Но ведь нельзя доказать все. Какие-то утверждения нужно принять как очевидные. Непротиворечивость арифметики очевидна.

Непротиворечивость наивной теории множеств тоже была очевидна. Я хочу уточнить свою позицию. Я согласен с Вами что выход за пределы формализма неизбежен. Но он должен быть четко осознаваем. Доказательсво - это дерево выовда с номерами правил вывода и номерами аксиом в листьях. Кодируется одним числом. Хоть один шаг вне этого - и теорема превращается в мета-теорему. Это не так страшно, но следует осознаватиь, что мета теореме не соответствует число, так как ее не геделизировать.

3
Непротиворечивость ZFC не доказана (в ZFC), а очевидна. Посмотрите Сморинского, он очень выразительно об этом пишет.

Выразительна ??? Очевидна ??? А я например читал что по моему ZFC + Universal Choice Function уже противоречива. То есть теория балансирует на уровне чуть посильнее (UCF сильнее AC), и кирдык. Вообще, как можно говорить об очевидности в ZFC, вспоминая AC, которая имеет контрочевидные следствия ?

(Ответить) (Parent) (Thread)

Для беседы нам с вами надо согласовать терминологию, иначе ничего не получится.

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

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

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

Кстати да, теоремы зависят от кодирования, этот вопрос исследовался, в частности, в упоминавшихся мной работах Фефермана (там это важно).

Ссылочки? Сам Гёдель, например. Переведы на английский язык легко доступны. Пожалуй, Richard Kaye, Models of Peano arithmetic. На мой вкус, тяжеловесная книжка, зато аккуратная.

Вопрос о непротиворечивости наивной теории множеств не ставился. Да он и не имеет точного смысла. Можно говорить о непротиворечивости формальной системы. А "наивное" канторовское определение множества аппелирует к неформальным идеям. "Парадоксы" лишь показывают, что некоторые языковые конструкции не достаточно точны, чтобы с их помощью образовывать множества.

Я не понял, вы прочитали Сморинского, или нет? Во всяком случае вы не возражаете на его текст, а повторяете ваш пример с универсальной выбирающей функцией. Универсальная выбирающая функция слишком близко подходит к "множеству всех множеств" и универсальной "аскиоме выделения". Я бы не сказал, что это "чуть посильнее". Это принципиально сильнее, причем именно в том направлении, которое, как уже сто лет понятно, ведет к противоречиям.

ZFC - очень слабая теория.

(Ответить) (Parent) (Thread)

Я принимаю Ваши определения доказательства и формального доказательства. Тем не менее, я хотел убедиться в том что

1. Теорема Геделя в общепринятом виде есть метатеорема
2. У нее есть эквивалентная (кодированная) формула в аксиоматике Пеано
3. Доказательство этого утверждения есть формальное доказательство
4. Этого никто еще не делал в виду большой длины доказательства

>Я не понял, вы прочитали Сморинского, или нет?
Я хочу заказать все на Амазоне но пока в связи с отпуском не собрался... Но обязательно закажу

(Ответить) (Parent) (Thread)

1. В моем смысле теорема Гёделя - это обычная математическая теорема.

2. Да.

3. Можно доказать математически, что у этого утверждения есть формальное доказательство. На самом деле это с самого начала считалось настолько очевидным, что Гёдель не стал публиковать вторую часть своей работы, в которой только это и требовало обоснования.

4. Практически ни для одной интересной матемтической теоремы никто не выписывал формального доказательства. Теоремы Гёделя не являются каким-либо исключением.

Хотите, я вам пришлю дежавю файл со статьей Сморинского в русском переводе?

(Ответить) (Parent) (Thread)

>Хотите, я вам пришлю дежавю файл со статьей Сморинского в русском переводе?

Да, заранее спасибо !!!
Мое мыло: dots67 собака goodoldscripts.com

(Ответить) (Parent) (Thread)

Вроде послалось. Почти 5 Мб. Подвердите, пожалуйста, что дошло.

(Ответить) (Parent) (Thread)

Кстати, вы не могли бы дать ссылку или объясняние насчет UCF? Я, видимо, чего-то тут не понимаю.

(Ответить) (Parent) (Thread)

Я видел об этом упоминание вскользь в старой книжке Мендельсона (по русски), которую прочел году наверное в 89-90.

P.S. Я Видел, Вы тоже из тридцатки
Какой выпуск ? Я учился в одном классе с mancunian....

(Ответить) (Parent) (Thread)

Посмотрел. У Мендельсона написано, что, очевидно, UFC влечет AC, но неизвестно, вытекает ли UFC из AC. В теории множеств Морса-Келли за аксиому принят вариант UFC. Так что мы тут с вами пообсуждали несуществующую проблему, судя по всему. :)

Нет-нет, моя персональная информация - это ЖЖ-секрет. Извините.

(Ответить) (Parent) (Thread)