Еще раз об аксиоме выбора

[Geen]

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

рассуждал об объектах, которым не были даны определения

К слову, а где Вы дали определение натуральным числам?

[epros]

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

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

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

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

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

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

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

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

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

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

все множества в моем универсуме вроде бы и так регулярны без нее (я пока это не доказал, но сильно удивлюсь, если это не так)

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

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

Обычно под формализацией имеют в виду именно построение формальной системы

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

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

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

А мне не нравится. Куча вложенных скобочек, лишние запятые. То ли дело - зарубки на дереве: никаких лишних символов, отличная модель натурального числа. Строка десятичных цифр - тоже неплохая модель, подходит для записи достаточно больших чисел и операции выполняются достаточно просто. А эта извращённая конструкция из фигурных скобок - нет уж, увольте. Её можно принять только исходя из того, что это лучшее, что может предложить теория множеств.

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

Речь идет о формальной теории (одной) группы. Та, в которой 3 аксиомы, на которые Вы дали ссылку. Эта теория, по-сути - внутренний язык группы. Вы не сможете в ней формализовать даже такое простейшее рассуждение как: "Рассмотрим конечную группу $G$". И про гомоморфизмы в ней тоже, кажется, не поговорить. А Вы ее хотите отождествить со всей теорий групп. Ситуация абсолютно аналогична тому, что Вы отождествляете натуральные числа с формальной арифметикой.

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

[mihaild]

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

Есть набросок доказательства, а есть собственно доказательство

И отличаются они именно возможностью формализации.

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

И по-моему, во времена Эйлера было очевидно, что надо давать определения тем сущностям, с которыми работаешь

Вроде бы в то время это было как раз предметом обсуждений.
А систематически определения начал пытаться давать как раз Коши. Но это ему не помогло.

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

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

Это придется делать в любом случае.

epros в сообщении #1616098 писал(а):

Ничего не понимаю. Теория из трёх аксиом - это нормальная теория

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

[EminentVictorians]

epros в сообщении #1616059 писал(а):

Не надо говорить "понятно как", скажите как именно определённые. Иначе я это расцениваю как попытку увильнуть от признания того, что операции определяются аксиомами.

Итак, что у нас есть на данном этапе.

1) Есть аксиомы Пеано, которые выражают то, что мы хотим от натуральных чисел.
2) Есть множество $\mathbb N_0 = \Bigg\{\varnothing, \{\varnothing\}, \big \{\varnothing, \{\varnothing\} \big \}, \Big \{\varnothing, \{\varnothing\}, \big \{\varnothing, \{\varnothing\} \big \} \Big \}, \ldots \Bigg\} \eqno$
3) Есть функция $S: \mathbb N_0 \to \mathbb N_0$, $S(n) = n \cup \{n\}$.
4) Т.е. по факту уже есть модель, удовлетворяющая аксиомам Пеано.
5) Порядок определен так: $x < y \Leftrightarrow x \in y$. Дальше идут свойства порядка.
6) Существует единственная функция $+: \mathbb N_0 \times \mathbb N_0 \to \mathbb N_0$ такая, что:
$ \quad \quad$ 1)$+(m, 0) = m \quad (\forall m)$;
$\quad \quad $ 2)$+(m, S(n)) = S(+(m,n)) \quad (\forall m,n)$.
$ \quad \quad $ (Доказывается несложно, из основной теоремы о рекурсии)
7) Положим $a + b := +(a, b)$.

epros в сообщении #1616098 писал(а):

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

Конечно. А я разве оспариваю приоритет или авторитет Эйлера? Я всего лишь отметил, что во времена Эйлера математики рассуждали о неопределенных (или наверное правильнее сказать - плохоопределенных) понятиях. Разумеется, это логическая дыра.
А то так говорите, будто я решил перечеркнуть всю математику 18-ого века.

epros в сообщении #1616098 писал(а):

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

Не знаю, мне наоборот понравилось. Можете свой вариант привести.

epros в сообщении #1616098 писал(а):

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

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

mihaild в сообщении #1616128 писал(а):

И отличаются они именно возможностью формализации.

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

Я пишу в тетрадке: "Рассмотрим число 2".
Вы говорите: "Что такое число 2? Не понимаю".
Я: "Число 2 - это множество $\big \{\varnothing, \{\varnothing\} \big \}$, где $\varnothing$ - это пустое множество, т.е. множество, в котором нет элементов.

Мы не делали формализацию. Я не вводил ни формальную теорию, ни исчисление предикатов. Я даже терм "2" в формальном виде не записал. Но неужели осталась какая-то неоднозначность? По-моему, ее нету.

[epros]

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

1) Есть аксиомы Пеано, которые выражают то, что мы хотим от натуральных чисел.
2) Есть множество $\mathbb N_0 = \Bigg\{\varnothing, \{\varnothing\}, \big \{\varnothing, \{\varnothing\} \big \}, \Big \{\varnothing, \{\varnothing\}, \big \{\varnothing, \{\varnothing\} \big \} \Big \}, \ldots \Bigg\} \eqno$
3) Есть функция $S: \mathbb N_0 \to \mathbb N_0$, $S(n) = n \cup \{n\}$.
4) Т.е. по факту уже есть модель, удовлетворяющая аксиомам Пеано.
5) Порядок определен так: $x < y \Leftrightarrow x \in y$. Дальше идут свойства порядка.
6) Существует единственная функция $+: \mathbb N_0 \times \mathbb N_0 \to \mathbb N_0$ такая, что:
$ \quad \quad$ 1)$+(m, 0) = m \quad (\forall m)$;
$\quad \quad $ 2)$+(m, S(n)) = S(+(m,n)) \quad (\forall m,n)$.
$ \quad \quad $ (Доказывается несложно, из основной теоремы о рекурсии)
7) Положим $a + b := +(a, b)$.

Первого уже достаточно!

Дальнейшее - $\mathbb N_0 = \Bigg\{\varnothing, \{\varnothing\}, \big \{\varnothing, \{\varnothing\} \big \}, \Big \{\varnothing, \{\varnothing\}, \big \{\varnothing, \{\varnothing\} \big \} \Big \}, \ldots \Bigg\} \eqno$ и $S(n) = n \cup \{n\}$ - это уже относится к построению модели, с точки зрения понятия о числах это ничего не меняет. Зачем нужно 7 вообще непонятно. Это всего лишь две разные формы записи бинарной операции: инфиксная и префиксная.

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

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

А то так говорите, будто я решил перечеркнуть всю математику 18-ого века.

Было очень похоже на это. Типа, Эйлер и Коши ничего существенного не доказали, поскольку не изложили всё "достаточно строго" (по Вашим понятиям).

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

Не знаю, мне наоборот понравилось. Можете свой вариант привести.

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

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

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

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

Что значит "выразить в теории"? Как Вы себе представляете выражение в теории, например, конечности группы? Добавлением новых аксиом? Так я Вам скажу, что можно все новые аксиомы запихнуть в антецедент (он же - предпосылка) импликации и в консеквенте (он же - вывод) данной импликации изложить любой вывод этой "новой" теории. При этом сама импликация будет теоремой старой теории.

[Geen]

(Оффтоп)

Немного не в тему. Меня до сих пор плющит от таких "естественных" фраз, как "это пространство удовлетворяет очередной аксиоме счётности"....

[EminentVictorians]

epros в сообщении #1616191 писал(а):

Первого уже достаточно!

Хорошо. И почему, по-Вашему, справедливо $a+b = b+ a \quad (\forall a, b)$?

epros в сообщении #1616191 писал(а):

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

Ну я действительно считаю это логичным.

epros в сообщении #1616191 писал(а):

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

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

[epros]

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

Хорошо. И почему, по-Вашему, справедливо $a+b = b+ a \quad (\forall a, b)$?

Теорема арифметики Пеано. Доказывается по индукции.

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

Ну я действительно считаю это логичным.

Считать можно что угодно. А Вы попробуйте это правило строго определить.

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

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

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

[mihaild]

epros в сообщении #1616207 писал(а):

А что, понятия "биекции" и "натурального числа" определять не нужно?

Нужно.
Но понятно как через $\in$ выразить утверждение "у симметричной матрицы существует базис из собственных векторов". А как через $\cdot$ и $=$ выразить утверждение "образ гомоморфизма изоморфен фактору по ядру"?

[Geen]

Аксиома выбора: в споре нужно выбирать сторону, которая может не давать определений и произвольно, по месту менять правила вывода.

[EminentVictorians]

epros в сообщении #1616207 писал(а):

Так это и делается дополнительными аксиомами.

Нет. Чтобы определить в ZFC натуральные числа и биекции, никаких новых аксиом в нее добавлять не нужно.

epros в сообщении #1616207 писал(а):

Считать можно что угодно. А Вы попробуйте это правило строго определить.

А "строго" - это обязательно с построением формальной системы, да?

epros в сообщении #1616207 писал(а):

См. конец моего предыдущего сообщения.

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

[Geen]

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

Давайте по порядку. Вы в рамках теории из трех аксиом

Приведите эти три аксиомы, пожалуйста (раз уж всё по порядку). И объясните, пожалуйста, при чём тут теория групп?

[epros]

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

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

К сведению: Любое утверждение, принимаемое без доказательства, является аксиомой. Как Вы будете что-то определять без утверждений?

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

А "строго" - это обязательно с построением формальной системы, да?

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

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

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

Я не понял, что там написано.

Вы не поняли что такое импликация или где у неё антецедент и консеквент?

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

Вы в рамках теории из трех аксиом не сможете даже сформулировать теорему Бернсайда, а я в рамках теории множеств смогу ее и сформулировать, и доказать. С этим согласны?

А вот я не понял, чего и зачем Вы от меня хотите. Для начала объясните, что значит "сформулировать и доказать в рамках теории".

[EminentVictorians]

epros в сообщении #1616438 писал(а):

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

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

К сведению: Любое утверждение, принимаемое без доказательства, является аксиомой. Как Вы будете что-то определять без утверждений?

Так в ZFC есть аксиомы. (Есть немного разные конкретные формализации ZFC, но это не важно. Чаще всего имеют в виду ту, в которой 9 аксиом.)

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

И имеющиеся 9 аксиом прекрасно позволяют давать определения подавляющему большинству обычных математических объектов.

epros в сообщении #1616438 писал(а):

Вы не поняли что такое импликация или где у неё антецедент и консеквент?

Это понимаю. Я не понял рассуждение про аксиомы.

epros в сообщении #1616438 писал(а):

Для начала объясните, что значит "сформулировать и доказать в рамках теории".

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

[epros]

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

И имеющиеся 9 аксиом прекрасно позволяют давать определения подавляющему большинству обычных математических объектов.

Я вот смотрю на имеющиеся аксиомы ZFC и не вижу ничего ни про "натуральные числа", ни про "биекцию", ни про "конечность". Поэтому вопрос: Что Вы имели в виду под "позволяют дать определения"? Лично я не могу понять, каким образом имеющиеся аксиомы ZFC (или их отсутствие) могут помешать давать какие-то новые определения.

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

Я не понял рассуждение про аксиомы.

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

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

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

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

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

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

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

Дать определение терма - это значит написать строчку, которая является тем термом, который мы определяем.

А это вообще непонятно о чём. Записать строчку - это значит записать строчку. Слово "определить", очевидно, должно означать что-то другое.