А вот Вы не слышите, что я Вам говорю: Любую сокращённую запись нужно чем-то определять. И это "что-то" непременно окажется дополнительными аксиомами.
Я слышу, просто я с этим не согласен. Рассмотрим, например, следующую строчку:
Эта строчка является формулой теории множеств. А вот строчка
- это её сокращенная запись. Символа "
" в алфавите теории множеств нету.
И что значит "Любую сокращенную запись нужно чем-то определять"? Любая сокращенная запись определяется, собственно, той записью, которую она сокращает.
Вот и в данном случае, короткая строчка
- это сокращение вот этой длинной строчки с импликациями и скобками, которая написана выше.
Поэтому, на мой взгляд, Вы здесь однозначно ошибаетесь: чтобы оперировать сокращенными записями, никаких новых аксиом добавлять не надо.
Другое дело, если Вы хотите добавить символ
в алфавит теории множеств. Тогда да, надо будет вводить новую аксиому, определяющую это самое равно. Например, такую:
Но по мне, расширять алфавит теории множеств - это примерно как пить Шато Мутон Ротшильд из пластикового стакана, не допить, а потом затушить в него сигарету. Можно, конечно, но выглядит так себе.
И мне очень любопытно посмотреть, как Вы распишете в языке теории множеств (без всяких "сокращённых записей") определения сложения и умножения.
Сложение и умножение - это просто конкретные функции вида
,
. Я парой сообщений назад приводил
ссылку на сообщение в одной из прошлых тем, где я объясняю все эти шаги, включая, как определяется функция сложения. Вот конкретный фрагмент про
.
6) Существует единственная функция
такая, что:
1)
;
2)
.
(Доказывается несложно, из основной теоремы о рекурсии)
7) Положим
.
Или Вам надо, чтобы я еще и основную теорему о рекурсии расписал?
Затем, что Вы обещали определить "модель арифметики Пеано". Стандартную, насколько я помню. И даже, вроде, предполагали, что она должна возникнуть из теории множеств неким "естественным" образом (в отличие от нестандартных моделей, как я понимаю).
Ну, модель арифметики Пеано я точно определил. И я считаю ее стандартной. Я знаю, Вы сейчас скажете, что у самой теории множеств существуют нестандартные модели, но я в это не верю. Нестандартные модели может быть и есть у какой-нибудь ZFC, но я уверен, что мой универсум множеств определен однозначно.
(Универсум)
Универсум выглядит так:
1)Множество наследственно конечных множеств принадлежит универсуму
.
2)
и
3)
,
4)
и
5) есть схема выделения
6) если
и мы поставили в соответствие каждому
некоторый единственный
, то
будет множеством (т.е., грубо говоря, образ функционального суждения (которое само не обязательно является функцией) является множеством). (схема преобразования)
7) аксиома выбора
8) аксиома регулярности
Часть аксиом может быть избыточной, но это не важно.
Вы можете сколько угодно в своём подсознании представлять, что инкремент - это
, но Ваши собеседники не телепаты и им нужно явно сказать, что в рамках определяемой Вами модели арифметики Пеано это так, и никак иначе.
Рассмотрим функцию
,
. Докажем, что
является корректно определенной функцией вида
(т.е. что
). Функцию
будем называть инкрементом. Все. Проще некуда. Разумеется, перед этим должно быть определено объединение множеств (но это базовая база, очевидно она должна идти до введения натуральных чисел).
А это я не явно сказал?