"Как с этим работать?"

[EminentVictorians]

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

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

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

[Mikhail_K]

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

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

Если Вы $\mathbb{R}$ определяете аксиоматически, то это не нужно доказывать - это аксиома.
Вот если Вы определяете $\mathbb{R}$ по Дедекинду или одним из аналогичных способов, тогда да, надо доказывать. Но Вы же сами так не хотите. Если хотите относиться к $\mathbb{R}$ как к "чёрному ящику", то надо принимать аксиомы как данность.
Собственно, а как иначе? Не хотите разбираться во внутренней структуре - значит начинаете с каких-то "внешних" свойств.

[EminentVictorians]

Mikhail_K в сообщении #1721108 писал(а):

Если Вы $\mathbb{R}$ определяете аксиоматически, то это не нужно доказывать - это аксиома.

Аксиоматически - как именно? Тут как минимум 2 варианта:
1)Как элементарная теория (с алфавитом, сигнатурой, в которой есть значки +, $\cdot$, формальными аксиомами). Это обычный вариант формальной теории (первого порядка, если просто линейно-упорядоченное поле, или второго порядка, если с полнотой). Этот вариант мне не интересен, не люблю изолированные формальные теории.
2)Просто выписать список аксиом и искать множество, которое ему удовлетворяет. Этот вариант тоже не устраивает, потому что делается в рамках теории множеств.

Mikhail_K в сообщении #1721108 писал(а):

Вот если Вы определяете $\mathbb{R}$ по Дедекинду или одним из аналогичных способов, тогда да, надо доказывать.

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

Mikhail_K в сообщении #1721108 писал(а):

Если хотите относиться к $\mathbb{R}$ как к "чёрному ящику", то надо принимать аксиомы как данность.

Нет, не обязательно. Допустим все происходит в ETCC-подобной теории. $\mathbb R$ - это просто объект - неопределяемое атомарное понятие без внутренней структуры. Но это же не снимает необходимость доказать, что существует стрелка типа $+ : \mathbb R \times \mathbb R \to \mathbb R$ с известными свойствами. То есть из того, что в $\mathbb R$ нету внутренней структуры не следует, что необходимо сразу же принимать на веру все его свойства как аксиомы.

[Someone]

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

Нет, не обязательно. Допустим все происходит в ETCC-подобной теории. $\mathbb R$ - это просто объект - неопределяемое атомарное понятие без внутренней структуры. Но это же не снимает необходимость доказать, что существует стрелка типа $+ : \mathbb R \times \mathbb R \to \mathbb R$ с известными свойствами. То есть из того, что в $\mathbb R$ нету внутренней структуры не следует, что необходимо сразу же принимать на веру все его свойства как аксиомы.

Вы хотите странного: вывести существование и свойства действительных чисел из ничего. Извините, но это невозможно: из ничего нельзя вывести ничего вообще. Всегда нужно начинать с какого-то набора объектов и аксиом. Вопрос только в том, с чего Вы хотите начать.
Можно начать с "голой" теории множеств (ZFC или NBG, например). Тогда Вы определяете натуральный ряд как минимальное индуктивное множество. В нём есть "нулевой элемент" $0=\varnothing$ и операция "следующий элемент" (прибавление единицы) $n+1=n\cup\{n\}$. Через эту операцию Вы определяете арифметические операции "сложение" и "умножение" и доказываете выполнение аксиом Пеано. Полезно также определить "отношение порядка" ($m\leqslant n\Longleftrightarrow m\subseteq n$) и доказать его свойства.
Затем, исходя из множества натуральных чисел, определяете множество целых чисел, операции на целых числах и отношение порядка, доказываете их свойства (получается линейно упорядоченное кольцо).
Затем определяете множество рациональных чисел с операциями и отношением порядка (линейно упорядоченное поле).
И, наконец, переходите к полю действительных чисел.

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

[EminentVictorians]

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

Вы хотите странного: вывести существование и свойства действительных чисел из ничего.

Почему из ничего? Я готов принять какие-то неопределяемые понятия и 5-10 аксиом о них. Разумеется, это должны быть не множества и не принадлежность.

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

Разумеется, каждый шаг требует знания структуры элементов, определённых на этом же шаге.

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

[Someone]

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

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

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

[dgwuqtj]

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

Допустим все происходит в ETCC-подобной теории. $\mathbb R$ - это просто объект - неопределяемое атомарное понятие без внутренней структуры. Но это же не снимает необходимость доказать, что существует стрелка типа $+ : \mathbb R \times \mathbb R \to \mathbb R$ с известными свойствами.

В ETCS (elementary theory of the category of sets) всё равно точно так же нужно доказывать существование $\mathbb R$ через дедекиндовы сечения или что-то аналогичное. Там изначально дано только $\mathbb N$.

[Mikhail_K]

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

Разумеется, это должны быть не множества и не принадлежность.

Но Вы ведь хотите говорить про $\mathbb{R}$, а также, наверное, про отдельные вещественные числа, этому $\mathbb{R}$ принадлежащие. Вот и принадлежность.
Ваша антипатия к множествам непонятна. Язык множеств - отличная и удобная штука.

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

[EminentVictorians]

Mikhail_K в сообщении #1721122 писал(а):

Но Вы ведь хотите говорить про $\mathbb{R}$, а также, наверное, про отдельные вещественные числа, этому $\mathbb{R}$ принадлежащие. Вот и принадлежность.

Я не против принадлежности, я против того, чтобы она была в фундаменте. Мне не нравится, что вокруг неё крутится вся теория множеств.

Mikhail_K в сообщении #1721122 писал(а):

Язык множеств - отличная и удобная штука.

Мне не нравится, что он слишком выразительный (слишком много слишком разных вещей можно выразить через множества). Плюс мне не нравится аксиома экстенсиональности.

Mikhail_K в сообщении #1721122 писал(а):

"Внутренняя структура" вещественных чисел может казаться искусственной (хотя мне не кажется), но никто не заставляет её зафиксировать.

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

Mikhail_K в сообщении #1721122 писал(а):

Аксиомы, такие как коммутативность сложения, можно принимать на веру изначально и ни про какую структуру не говорить

Нет, такое меня точно не устраивает.

[Mikhail_K]

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

Проблема не в фиксации, а в самой потребности иметь хоть какую-то внутреннюю структуру.

Mikhail_K в сообщении #1721122 писал(а):

Аксиомы, такие как коммутативность сложения, можно принимать на веру изначально

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

Нет, такое меня точно не устраивает.

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

[EminentVictorians]

Mikhail_K в сообщении #1721127 писал(а):

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

Ну а как можно выразить "принадлежность элементов" бесструктурному объекту? Например, в категорных терминах, через обобщенные элементы (стрелки из терминального объекта в наш бесструктурный). Вот и с операциями примерно так же: "плюс" это просто стрелка; $a + b = b + a$ - это просто коммутативность такой-то диаграммы.

[dgwuqtj]

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

Вот и с операциями примерно так же: "плюс" это просто стрелка; $a + b = b + a$ - это просто коммутативность такой-то диаграммы.

А чтобы её построить или доказать нужное вам свойство, понадобится какая-то уже имеющаяся структура (например, что ваш объект — это внутренний $\mathrm{Hom}$ от каких-то других объектов, про которые тоже что-то известно). Правда, проще всё запостулировать и работать в получившейся большой формальной теории. Которая вполне может оказаться противоречивой, но это уже ваша проблема.

[EminentVictorians]

dgwuqtj в сообщении #1721129 писал(а):

А чтобы её построить или доказать нужное вам свойство, понадобится какая-то уже имеющаяся структура (например, что ваш объект — это внутренний $\mathrm{Hom}$ от каких-то других объектов, про которые тоже что-то известно).

Имеется в виду, что потребуется какое-то определение объекта? Если да, то это я понимаю. В духе что $\mathbb R$ можно определить через то, что он является терминальным объектом в категории архимедовых линейно упорядоченных полей?

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

[dgwuqtj]

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

В духе что $\mathbb R$ можно определить через то, что он является терминальным объектом в категории архимедовых линейно упорядоченных полей?

Через дедекиндовы сечения, как подмножество булеана $\mathcal P(\mathbb Q)$, заданное формулой первого порядка. Вам же не нравится, когда дают определение без доказательства существования (а только с единственностью). Для существования в объемлющей теории (ZFC, ETCS, или что вы там придумаете) должна быть соответствующая аксиома. Большая часть аксиом ZFC — это утверждения о существовании однозначно определённых множеств. И в ETCS есть отдельно аксиомы о существовании произведения и $\mathbb N$.

Халявы не бывает.