До BRT было три математических (не синтаксических) примера недоказуемых утверждений: Парис-Харрингтон, теорема Крускала и теорема о минорах графов.

Гастрит конечно много знает, но ошибается, утверждая, что недоказуемых утверждений полно. Не найти их так просто, из-за того, что вся низшая математика арифметизируется и доказывается уже в примитивно рекурсивной арифметике. А интересных (=недоказуемых) утверждений только три штуки плюс BRT.

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

В начале мая кстати буду своих детей учить конструктивной математике (но в детской форме: что-то из книжки Мартин-Лёфа, а что-то из воспоминаний детства: последовательность Шпеккера, квадрат Оревкова).

ppkk: Про ZFC надо понять две вещи:

1. почему ZFC - это теория множеств, (а не правда)
2. почему ZFC - это не теория множеств (а труляляшки)

Друг другу даже на конечной арифметике противоречащие теории труляляшек ни к "правде" отношения не имеют ни "каноническими аксиоматизациями" теории множеств не являются.

Раз разные теории друг другу противоречат во всем - почему бурбаковская лучше остальных?

(Reply to this) (Parent) (Thread)

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

Почему ты ее выбрал вместо одной из миллиона остальных, во всем противоречащих ей теорий труляляшек?

(Reply to this) (Parent) (Thread)

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

(Reply to this) (Parent) (Thread)

То есть тут два очень разных вопроса.

1. Можно ли написать какие-то аксиомы, в которых знакомая математика легко сделается (формализуется)?

2. Можно ли выписать какие-то аксиомы, которые помогут нам заниматься математикой, например отвечать на наши сложные вопросы?

Ответ на первый вопрос известен за много лет до Бурбаков.

В качестве ответа на второй вопрос бурбаковская система не подойдет, ибо слаба и беспомощна.

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

(Reply to this) (Parent) (Thread)

Ответ на первый вопрос известен за много лет до Бурбаков.
По-моему, до Бурбаков не ответ известен, а святая вера в знание ответа была у некоторых. Их труд — типа проверки этого метаматематического (в смысле Гильберта) тезиса, который, к тому же, так себе: тяжеловато получилось для народа.

В качестве ответа на второй вопрос бурбаковская система не подойдет, ибо слаба и беспомощна.
Нужны более сильные системы, но они все друг дружке противоречат. Какую из них выбрать?
Теорема-то Гёделя, которую якобы Бурбаки не учитывали, предполагаю, и сподвигла их на ограничение себя ЦФ (и то: из-за аксиомы выбора сколько разговоров).

И почему более сильные системы нужны? Или есть системы, где как-то механически недоказуемость определяется, непротиворечивость которых, так сказать, на том же уровне неопределённости, что и непротиворечивость ЦФ?

(Reply to this) (Parent) (Thread)

Определение 1.

Арифметическая сила теории (arithmetical strength) - это множество арифметических утверждений, доказуемых в данной теории.
Теории образуют частично упорядоченное множество по включению, по своей силе.

Определение 2.

Пи_1-сила (Pi_1 strength) теории - это множество арифметических утверждений с одним квантором всеобщности, доказуемых в этой теории.
Теории образуют частично упорядоченное множество по включению по своей Пи_1 силе.

Определение 3/

Consistency strength (количество силы). Для теорийй Т_1 и Т_2, скажем Т_1 < Т_2 если Т_2 доказывает непротиворечивость Т_1.

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

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

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

Это был мой ответ на твой вопрос "зачем нужны сильные теории?" Чтобы отвечать на арифметические вопросы! И ответ будет не "да" или "нет", а взвесь разных ответов разных теорий.

(Reply to this) (Parent) (Thread)

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

Текст был таким:
> Esche tebe napisal.
Я потихоньку читаю, потом разом отвечу по ощущениям.

> Разноголосица разных теорий, силньных, слабых, всяких, и всех друг с дружкой не соглашающихся -
> основое открытие логики в 20 веке. Когда-то математики верили, что (осмысленные, арифметические)
> утверждения делятся на "истинные" и "ложные". Теперь всё по-другому....
>
> Это был мой ответ на твой вопрос "зачем нужны сильные теории?" Чтобы отвечать на арифметические
> вопросы! И ответ будет не "да" или "нет", а взвесь разных ответов разных теорий.

И скоро ли слово "сепульки" будет ассоциироваться не только с нелюбимыми множествами, но и с натуральными числами? (Или проблема и в том, что они бывают вплетены в основу логических рассуждений вообще? Помню, меня это очень поразило и расстроило, когда я изучал логику... на философии в аспирантуре.)

Я пока не понял, чем это дискредитирует Бурбаков: все теории не описать, они взяли что-то (достаточно сильное) и построили в ней. Почему бы теперь не построить такое в других, не сравнить, так сказать, полномасштабно?

Математике как особому виду деятельности по построению моделей для применения в науках, конечно, должно быть плевать на конкретную основу, лишь бы минимизировать риск совсем несуразных внутренних противоречий. И в этом сильные теории ведь не помогают больше чем почти вековая ЦФ, или как?

(Reply to this) (Parent) (Thread)

--- сепульки, "множества" и труляляшки не вплетены естественным способом в человеческие рассуждения. Это придуманные штуки, которые, впрочем, имеют свои мнения по разным осмысленным арифметическим вопросам.

--- Нет, если ты о том, что Бурбаки сели и записали как какие-то теоремы следуют из каких-то аксиом, то я с тобой согласен - молодцы. Не первые, не вторые, но основательно постарались. Критикуют их за то КАК они это сделали (например статья Матиаса про количество символов, участвующих в ИХ опеделении числа 1) и за то, во что они при этом публично верили (верварские примитивные верования: Солнце ходит кругами над землей, а земля плоская и т. п.).

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

(Reply to this) (Parent)

> Когда-то математики верили, что (осмысленные, арифметические) утверждения
> делятся на "истинные" и "ложные". Теперь всё по-другому..

Бедненький глупенький Марков. Так ведь до самой смерти и полагал, дурачина, что конъюнкция замкнутых формул выражает истинность обеих членов (см. «Избранные труды», Т. 2, стр. 404), а замкнутая формула с квантором общности означает наличие общего метода, позволяющего устанавливать опять же истинность формул определённого вида (там же, стр. 404 и 413). И в лекциях своих, лопушара отсталый, писал, что наличие семантики позволяет квалифицировать одни формулы языка как верные, а другие — как ложные (там же, стр. 437).

Полный лох был, одним словом. То ли дело нынешнее поколение!

(Reply to this) (Parent)

Вообще-то принцип Парриса-Харрингтона доказывается, причём в одну строчку. Voilà:

Доказательство. Принцип Парриса-Харрингтона верен. Следовательно, принцип Парриса-Харрингтона верен.

Чем плохо? Тем, что не в PRA проведено? А кто Вам сказал, что выводы в PRA исчерпывают суть понятия «доказательство»? Или просто дело в том, что под "недоказуемость" гранты дают (т.к. слово звучит для неспециалиста заманчивой музыкой), а вот под "невыводимость в PRA" — уже нет (что-то узкоспециальное и неинтересное)? Где же, господа логики, ваша научная честность, без которой, Как Учил Нас Великий Фейнман, наука вырождается в карго-культ?

Стоп: а может, Вы как раз и есть служители карго-культа от логики? Так Вы ж признайтесь — мне можно, я Вашим грантодателям не расскажу. Честное пионерское :-)

> Не найти их так просто

Доказательство теоремы Гёделя состоит в предъявлении алгорифма, перерабатывающего любое $\Sigma_1$-полное семантически пригодное логическое исчисление в невыводимую вместе с отрицанием замкнутую $\Sigma_1$-формулу. Чего тут искать-то?

> Я ищу утверждения, которые ни истинные ни ложные

Опять "истинное" отождествлено с "выводимым в PRA"? Всё надеетесь, что самолёты с тушёнкой прилетят? :-)

> что-то из книжки Мартин-Лёфа

Да, великая книжка. Я о ней ещё ни одного положительного отзыва не слышал — в том числе от себя :-) Так что у Вас есть шанс стать тут Первым!

> что-то из воспоминаний детства: последовательность Шпеккера, квадрат Оревкова

...ленинградский принцип в качестве самостоятельной вещи (хотя он уж сорок почти лет как теорема)...

> в детской форме

В кои-то веки — честно :-)

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

Не понял "доказательство". PH не является истинным утверждением.

Чем плоха последовательность Шпеккера - тоже не понял.

При чем здесь доказательство теоремы Гёделя? Я же писал, что не в нём дело. А замечание с алгоритмом я исключил, так как исключил синтаксические трюки (оставив лишь интересную содержательную математику).

Денег на мою науку никогда не давали. Я много лет был безработным, до недавнего времени. Не понимаю что за выпады!

Да, ленинградский принцип я не принимаю (недавно меня явным образом выявили): действительно я никогда не говорю про теорию "consistent".
Говорю только "not inconsistent".

Мне этот разговор надоел. Пожалуй, если содержательная часть закончилась, пойду обяснять детям как ZF+ (V=L) влечет существование деревьев Суслина.

Андрей

(Reply to this) (Parent) (Thread)

> Не понял "доказательство". PH не является истинным утверждением.

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

> Чем плоха последовательность Шпеккера - тоже не понял.

Последовательность Шпеккера замечательна, как и сингулярные покрытия. Это книжка Мартин-Лёфа плоха (бессистемное скакание по верхам).

> интересную содержательную математику

Ну вот ppkk только что спрашивал, что же такого в PH и BRT содержательного (упоминание про "интересное" отклоняется как субъективное). Ответа я не пока не вижу.

> Не понимаю что за выпады!

Эти выпады вызваны тем, что Вы постоянно утверждаете, что PH и BRT нужны для конструктивной математики — но при этом старательно уходите от вопроса, для чего же именно они ей нужны (вместо этого идут попытки элементарного запугивания: "можно отстать"). Я вижу в таком положении вещей нарушение научной честности:

1) если новая теория для чего-то действительно нужна, то у неё в активе должны иметься решения каких-то не берущихся по-другому задач (или установление определённой точки зрения, упрощающей какой-то круг вопросов) — почему бы это всё не предъявить сомневающимся?
2) если же теория приложений не имеет, но просто кому-то интересна — так и надо сказать, вопросов тоже больше не будет.

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

> Мне этот разговор надоел.

Не смею навязываться. Хотя жаль, конечно, что содержательных ответов на вопросы про Вашу тематику так и не поступило.

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

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

(Reply to this) (Parent)

(Mizar упорно не качается.)

http://kgs.logic.at/goedel-fellowship/index.php?winners — деньги дают под "Independence results in concrete mathematics", а не за "недоказуемость". Вы неправы.

Но, боюсь, независимость имеется в виду именно от презренной ЦФ…

(Reply to this) (Parent) (Thread)

Далась же Вам эта ZF. Насколько я видел, там независимость от формальной арифметики (независимость чего-то от ZF автоматически означала бы её непротиворечивость — на Филдса, думаю, потянет).

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

Насколько я знаю, в русскоязычной литературе считается, что Коэн доказал "независимость гипотезы континуума от остальных аксиом аксиоматической теории Цермело-Френкеля". И интересно это 1) методом вынуждения 2) тем, что континуум-гипотеза важная (как проблема Гильберта, например). Разве все остальные доказательства независимости от ЦФ удостаивались Филдсовской медали? Что-то Вы мудрите.

Мне рекламировали как раз "утверждения о натуральных числах" зависящие от аксиом о больших кардиналах (со ссылкой на труд Фридмана; в статье Бовыкина "new" об аксиомах о больших кардиналах пишется только как об аналогии, кажется, хотя есть ссылка Friedman, H. (1998). Finite functions and the necessary use of large cardinals. Annals of Mathematics 148, pp. 803-893). Возможно, сам Андрей независимостью от ЦФ и не занимается.

(Reply to this) (Parent) (Thread)

«Проблема непротиворечивости аксиоматической теории множеств — это своего рода "любимая мозоль" специалистов по данному вопросу. Её пытаются решить, но "добровольно" признаваться в том, что она пока ещё не решена, у них как-то не принято. Нередко даже у самых крупных специалистов можно встретиться с точными утверждениями, в которых она фактически фигурирует в качестве решённой (!) в положительном смысле. Это делается таким образом, что вместо верной импликации читателю в качестве верного преподносится её заключение, что, конечно же, в высшей степени курьёзно для математика». А.А.Марков, Н.М.Нагорный, «Теория алгорифмов», 2-е изд., 1996, стр. XVI.

С уважением,
Гастрит

(Reply to this) (Parent)

нет, там в двух местах две разные истории: одна про аналогии, а одна про недоказуемость в ZFC + кардиналы Мало.

(Reply to this) (Parent) (Thread)

Там как-то обзорно написано.

Another series of H. Friedman’s results under the general name of “boolean relation theory” can be found in [38]: if we list all (second-order) statements of a certain simple shape (all of them a priori equally simple and natural) and try to classify them according to their truth, some of them turn out to be unprovable in some theories stronger than ZF, e.g. the following statement from [38] is provably in ACA0 equivalent to 1-consistency of the theory ZFC+{there is an n-Mahlo cardinal}(n∈ω)

А ссылка на "Interpreting set theory in discrete mathematics" — я это тоже счёл чем-то типа аналогии.

(Reply to this) (Parent)

ppkk: Про ZFC надо понять две вещи:
1. почему ZFC - это теория множеств, (а не правда)
2. почему ZFC - это не теория множеств (а труляляшки)
Можно узнать, где я утверждал, что ЦФ — "правда"? И я что, мало раз утверждал, что не знаю никаких "реальных множеств", что ЦФ может оказаться неверной и т.п.? Прежде чем снисходительно предлагать мне что-то "понять", имеет смысл попытаться понять, что я утверждаю, а не писать мне обращения к какой-то убогой придуманной модели меня.

почему бурбаковская лучше остальных?
Потому что у них не только теория множеств. Потому что они не остановились на первом томе. Вот они в основном уже перестали книги печатать, пожалуйста: пишите с другой логической теорией/теорией множеств многотомник с основными достижениями современной математики. Только тогда у Бурбаков (если не будет принципиальных новых достоинств этих других теорий, сохраняющих выжные общепризнанные результаты и позволяющие получить новые) останется только старшинство.

А интересных (=недоказуемых) утверждений только три штуки плюс BRT.
То есть основные достижения логики — придумывать иллюстрации к теореме Гёделя о неполноте? А то, что Бурбаки на основе логической теории и теории множеств выписали немаловажную часть математики — разве не более серьёзное достижение в области логики?

> при наличии общепринятой логической теории/теории множеств.
Нет никакой "общепринятой логической теории". Многочисленные теории труляляшек и сепулек друг дружке противоречат (потенциально) даже на утверждениях о конечных множествах.
То есть до тебя наконец дошло, что для того, чтобы считать решением проблемы Уайтхеда результат Шелаха, нужно считать ЦФ общепринятой?

(Reply to this) (Parent) (Thread)

Петр,

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

Я действительно утверждаю, что:

1. ZFC - это не теория множеств. Большинство математиков того времени отвергли ZFC (а принимали Канторовскую теорию множеств). И этому есть причина.
2. ZFC - это теория множеств (=труляляшек), в отличие от осмысленных утверждений.

Насчет твоего вопроса, просто ли я иллюстрирую теорему Гёделя. Да, но лишь в той же степени в которой обычные математики иллюстрируют 0=0.
Я думаю, что обычный математик удивится, если ты начнешь формулировать суть его занятий как "переформулирование 0=0". Суть не в этом.
Я интерестюсь ни истинными ни ложными утверждениями (или утверждениями "имеющими силу") в той же степени, в какой обычный математик интересуется истинными утверждениями.
(Главное - интересность и важность, новые математические явления. Понятно, само собой разумеется, что обычный математик должен доказать истинность своих теорем, но совсем не обязательно на этом концентрироваться...)

Нет, импликация Шелаха доказывается в примитивно рекурсивной арифметике. Его теорема говорит, что ZF+V=L верит в такй-то ответ на вопрос Уайтхеда...

Теперь про формализацию. Формализация математики началась с Фреге и закончилась книжкой Рассела и Уайтхеда. Нужны ли для этого труляляшки обсуждалось много десятилетий (с 1870х годов до 1920х годов). То, что после этого Бурбаки с малым числом ошибок по-дилетантски попробовали это повторить - хорошо. Но они сопроводили свои книги какими-то объяснениями, наивными и ошибочными. За это их и критикуют. А то что они из аксиом вывели какие-то теоремы (в большом количестве) - это никто не критикует. Это правда, и это и без Бурбаков было ясно.

(Но бурбаковские аксиомы не ответят мне на некоторые простейшие вопросы про натуральные числа.)

Важнейшим событием в основаниях математики в 20 веке была Арифметизация, проведенная Расселом-Уайтхедом, Гильбертом, Гёделем, Тюрингом, Марковым, Шаниным и некоторыми другими.

То, что Бурбакам на всё историю наплевать - еще одна причина не принимать их всерьез.

(Reply to this) (Parent) (Thread)

ZFC — это не теория множеств… в отличие от осмысленных утверждений
Таки "реальные множества", что ли, которые сами по себе, как у Гастрита? Можно определённее?
В отличие от каких ещё "осмысленных утверждений"?!

Да, но лишь в той же степени в которой обычные математики иллюстрируют 0=0.
Всяк кулик своё болото хвалит. Разъяснишь (хотя бы ссылками), что такое по твоим понятиям "арифметизация пятой ступени", авось можно будет понять, в чём же дело. Не увлекайся моделированием "обычных математиков", кстати: их много разных, вряд ли тебе (или мне) так легко их обобщить.

Нет,… Его теорема говорит, что ZF+V=L верит в такй-то ответ на вопрос Уайтхеда…
Почему нет-то??

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

некоторые простейшие вопросы про натуральные числа
Можно пример?

Важнейшим событием в основаниях математики в 20 веке была Арифметизация, проведенная Расселом-Уайтхедом, Гильбертом, Гёделем, Тюрингом, Марковым, Шаниным и некоторыми другими.

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

(Reply to this) (Parent) (Thread)

> В отличие от каких ещё "осмысленных утверждений"?!

---- Ну например арифметических. Хотя тема "осмысленности" - это тоже серьезный разговор, куски из которого знамениты (например разговор Рассела с Витгенштейном).


> Почему нет-то??

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

> Я большего о них и не утверждаю. Хотя форма, более доступная для рутинной компьютеризации была бы предпочтительнее, но они давно писали.

---- Тогда я с тобой согласен.

> Ну, это как в архитектуре важнейшими называть нереализованные проекты, если я не ошибаюсь, а не построенные здания.

---- Ну почему нереализованные? Дедекинд-Пеано-Вейерштрасс свою волну арифметизации хорошо записали, Фреге-Уайтхед и Рассел хорошо записали, Чёрч, Гёдель и Тюринг арифметизацию языка и выводимости записали со всеми подробностями, четвертая волна (Марков, Клини, Шанин и т.д.) даже до матфизики и функционального анализа добралась, вся записана в подробностях. Сейчас идет пятая волна, с новыми идеями. Она не вся записана и из-за разных философий там разные мнения да и идеи еще не кристаллизовались. Я их знаю, но так просто не рассказать.

Андрей

(Reply to this) (Parent)

я ничего не говорил про всех математиков, кроме того, что они находят доказуемые утверждения (теоремы).

Нелепо утверждать, будто вместо смысла математики концентрируются на "доказуемости" или на "переформулировании 0=0".

Точно так же и я. Не только в недоказуемости дело, а в содержании.

(Reply to this) (Parent)

Еще одна мысль: ZFC не является и "неправдой".

У Бурбаков, отставших на 50 лет от оснований математики (есть такая наука) того времени, уж точно никакого старшинства.

(Reply to this) (Parent) (Thread)

Ага. Старшинство у Гильберта.

На 50 лет им сложно было отстать: за 50 лет до них теория множеств была, как я понимаю, ещё с канторовским определением множества, если не хуже.

От чего 50 лет отсчитываешь?

(Reply to this) (Parent) (Thread)

Отсчитывать можно от Кронекеровской критики теории множеств (1880?).

Можно от первых парадоксов (1895).

Можно от аргументов Пуанкаре (1900).

А можно действительно и от спора Гильберта и Брауэра (1910?).

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

(Reply to this) (Parent) (Thread)

Они в 1935-м начали.

(Reply to this) (Parent)