Освоение математики фундаментально и для практики

[diletto]

Anton_Peplov в сообщении #1556381 писал(а):

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

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

[Anton_Peplov]

diletto
См. определение формальной теории (например, в учебнике математической логики Клини). При определении той или иной формальной теории (в том числе формальной ZFC) мы вводим не только аксиомы, но и правила вывода, то есть алгоритмы, по которым из одних утверждений теории можно получать другие утверждения. Формальный вывод утверждения $X$ из аксиом - это цепочка (или дерево) утверждений, которое начинается с аксиом, а заканчивается утверждением $X$, причем каждый член цепочки получен из предыдущих в соответствии с тем или иным правилом вывода. И да, соответствие правилам вывода можно проверить автоматически. Более того, в принципе, все формально выводимые из аксиом утверждения можно вывести автоматически - полным перебором. Просто перебираем все возможные наборы символов в порядке возрастания длины, пока один из них не окажется доказательством или опровержением утверждения $X$. Но, конечно, это очень "в принципе": сколько придется перебирать, прикиньте сами.

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

Теоремы Геделя и связанные с ними ограничения относятся к формальному выводу. О неформальном они ничего не говорят.

[EminentVictorians]

Было бы интересно узнать, насколько велик и важен тот объем математики, который опирается на работу именно с формальными теориями (в частности с формальной $ZFC$). Я имею в виду, например, арифметику кардиналов (и вытекающие из нее всякие кардинальные инварианты в топологии). Или, возможно, дескриптивную теорию множеств (?) и ее следствия для обычного матанализа, если таковые имеются. Сюда же метод форсинга. Особенно было бы интересно узнать о таких сюжетах в алгебре.

-- 07.06.2022, 01:22 --

Насчет арифметики кардиналов. Я же правильно понимаю, что ее нет в "наивной" теории множеств? Т.е. ее можно использовать только в рамках формальной $ZFC$. Или в "неформальной" $ZFC$ она тоже есть? (по поводу арифметики кардиналов в других теориях множеств тоже было бы интересно послушать)

[diletto]

Anton_Peplov в сообщении #1556661 писал(а):

Логическая корректность такого вывода остаётся на совести математика и его рецензентов (в отличие от формального вывода, где она гарантируется по построению правил вывода).

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

[Someone]

diletto в сообщении #1556667 писал(а):

Мне чудится какая-то когнитивная дырища в том, что неформальный вывод трудно формализовать...

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

diletto в сообщении #1556667 писал(а):

доказательство с помощью ручки, бумаги и головы не всегда формализуемо

Неформализуемо потому, что та математическая теория, к которой это доказательство относится, сама не формализована. Подавляющая часть математики не формализована, потому что это никому не нужно.

EminentVictorians в сообщении #1556665 писал(а):

Насчет арифметики кардиналов. Я же правильно понимаю, что ее нет в "наивной" теории множеств?

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

[Anton_Peplov]

diletto в сообщении #1556667 писал(а):

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

Я бы сказал осторожнее: мы не можем знать априори, формализуемо оно или нет, поскольку никто не пытался его формализовать.

Формализация неформальных доказательств - это тяжелый труд, поскольку, как справедливо отметил уважаемый Someone,

Someone в сообщении #1556688 писал(а):

Простое и наглядное неформальное рассуждение при формализации превращается в длинную цепочку трудновоспринимаемых манипуляций со строками символов.

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

[Someone]

Anton_Peplov в сообщении #1556708 писал(а):

подавляющая часть доказательств не формализована. И, в принципе, нельзя исключать, что среди них окажутся неформализуемые на языке ZFC, хотя и принятые сообществом математиков как корректные.

Это вполне возможно. Может быть, какой-нибудь принцип мы считаем настолько естественным, что пользуемся им совершенно неосознанно и потому не замечаем. Если кто-то такой принцип обнаружит, будет повод дополнить систему аксиом ZFC.
Между прочим, эта система аксиом была сформулирована не одномоментно. Она формулировалась так, чтобы в ней можно было формализовать любые методы, обычно используемые в математике. Например, первоначально в ней не было аксиомы подстановки, была аксиома выделения. Но оказалось, что математики используют рассуждения, которые без аксиомы замены не формализуются. Ситуация может повториться.

[Walker_XXI]

Burunduka в сообщении #1555986 писал(а):

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

Можно. Но критерием правильности теории является её "хорошее соотношение" с действительностью, практической деятельностью, а не с собственными убеждениями. Последнее, конечно, приятно, но ненаучно.

Burunduka в сообщении #1556004 писал(а):

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

Не находите, что сами себе противоречите? Знание математики в рамках школьной программы необходимо.

Burunduka в сообщении #1556077 писал(а):

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

По-моему, вы путаете теоремы и теории (точнее, модели). Модель - это способ описать реальность. А теоремы - они как раз относятся к искусственному абстрактному миру, который у нас в голове (не на пустом месте возник, инспирирован, вдохновлён реальностью, но не реальность, а лишь упрощённая модель отдельных её аспектов). И если уж рассуждать, о том, в чём заложены теоремы, то они скорее заложены в аксиомах и алгоритмах рассуждений. В Реальности же нет никаких теорем. Это если противопоставлять Реальность и нас (субъект её познающий). А в реальности и субъекты со всем их внутренним миром и абстракциями - часть Реальности.

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

[Burunduka]

Walker_XXI в сообщении #1556776 писал(а):

Burunduka в сообщении #1555986 писал(а):

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

Можно. Но критерием правильности теории является её "хорошее соотношение" с действительностью, практической деятельностью, а не с собственными убеждениями. Последнее, конечно, приятно, но ненаучно.

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

Цитата:

Burunduka в сообщении #1556004 писал(а):

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

Не находите, что сами себе противоречите? Знание математики в рамках школьной программы необходимо.

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

Цитата:

Burunduka в сообщении #1556077 писал(а):

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

По-моему, вы путаете теоремы и теории (точнее, модели). Модель - это способ описать реальность. А теоремы - они как раз относятся к искусственному абстрактному миру, который у нас в голове (не на пустом месте возник, инспирирован, вдохновлён реальностью, но не реальность, а лишь упрощённая модель отдельных её аспектов). И если уж рассуждать, о том, в чём заложены теоремы, то они скорее заложены в аксиомах и алгоритмах рассуждений. В Реальности же нет никаких теорем. Это если противопоставлять Реальность и нас (субъект её познающий). А в реальности и субъекты со всем их внутренним миром и абстракциями - часть Реальности.

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

Цитата:

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

Спасибо за совет, посмотрю. Но я уже решил для себя с чего начинать и уже начал.