Как в аксиом. подходе формализуются определения ?

[Xaositect]

_hum_ в сообщении #724913 писал(а):

Для логики предикатов - да, а, например, для теории множеств, я так понимаю, уже же нет.

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

[_hum_]

Xaositect в сообщении #724914 писал(а):

_hum_ в сообщении #724913 писал(а):

Для логики предикатов - да, а, например, для теории множеств, я так понимаю, уже же нет.

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

Хм, значит, арифметика в такой класс теорий не попадает (по результату Геделя, в ней же не все истинные формулы выводимы)? И значит, она не выражаема средствами ZFC?
(Может, если слишком глупые вопросы, посоветуете хорошую книгу, где бы достаточно строго и полно эти вопросы рассматривались?)

[Xaositect]

_hum_ в сообщении #724915 писал(а):

Хм, значит, арифметика в такой класс теорий не попадает (по результату Геделя, в ней же не все истинные формулы выводимы)? И значит, она не выражаема средствами ZFC?

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

[_hum_]

Xaositect в сообщении #724916 писал(а):

_hum_ в сообщении #724915 писал(а):

Хм, значит, арифметика в такой класс теорий не попадает (по результату Геделя, в ней же не все истинные формулы выводимы)? И значит, она не выражаема средствами ZFC?

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

Ого. Не знал такого. Так почему же тогда все носятся с результатом Геделя, ведь по сути важны именно те утверждения, которые в любой модели истинны, а по сказанному Вами, они в точности совпадают с множеством выводимых. Ну и все тогда, все остальное не имеет смысла рассматривать.

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

[Xaositect]

_hum_ в сообщении #724913 писал(а):

а вот какой конструкции языка теории множеств соответствует сложение $m+n$ я так и не смог понять.

Например, можно построить график функции сложения, а сказать, что $m+n$ соответствует применению этой функции. Для этого вначале сказать, что по нашему определению множества натуральных чисел справедлив принцип индукции $\forall z (z\subset \omega\& \varnothing\in z \& \forall k (k\in z\to k\cup\{k\}\in z) \to z = \omega)$, а потом рассмотреть множество $\{k\in\omega | \exists f (f\subset\omega^2 \& (\varnothing, k)\in f \& (i, s)\in f \to (i\cup\{i\}, s\cup\{s\})\in f)\}$, по индукции оно равно $\omega$, т.е. $\forall k \exists f_k (\dots)$, а дальше график сложения это объединение частей $\{(k, l, f_k(l)) | l\in\omega\}$, нужны будет аксиомы замены и объединения.

[epros]

_hum_ в сообщении #724826 писал(а):

И опять для меня началось "размытие" понятия языка теории и метаязыка.

Не понял, в чём размытие? Например, символы $+$ и $0$ определены в языке арифметики. И строка $x+0=x$ является предложением языка арифметики. А когда мы записываем такое определение: "$+$ является бинарным инфиксным функциональным символом языка арифметики", то оно оказывается предложением мета-языка.

_hum_ в сообщении #724826 писал(а):

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

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

_hum_ в сообщении #724826 писал(а):

Брр. Я чего-то недопонимаю, зачем менять теорию. Вы ведь не меняете грамматику русского языка, когда вводите с помощью него определение нового понятия?

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

[arseniiv]

_hum_ в сообщении #724913 писал(а):

arseniiv в сообщении #724871 писал(а):

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

Извиняюсь, а как эта аксиома формулируется на языке теории множеств?

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


Задам тоже вопрос: если бы натуральные числа образовывали собственно класс, обойтись без схемы в ZFC было бы нельзя (а в NBG можно)?

[apriv]

_hum_ в сообщении #724920 писал(а):

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

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

[Doil-byle]

_hum_ в сообщении #724738 писал(а):

Но еще остается вопрос, а если не расширять теорию (оставаясь, например, в ZFC + логика предикатов), что в ней тогда будет отвечать определению отношения $<$ ?

Можно на обычном языке множеств: $E=\{(u,v):u \in v \}$, $x < y \Leftrightarrow (x,y) \in E$.

_hum_ в сообщении #724888 писал(а):

arseniiv в сообщении #724871 писал(а):

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

Извиняюсь, а как эта аксиома формулируется на языке теории множеств?

$\forall x (x \subset \mathbb{N} \wedge 0 \in x \wedge \forall y (y \in x \rightarrow y+1 \in x) \rightarrow x= \mathbb{N})$. Только в теории множеств это теорема.

_hum_ в сообщении #724920 писал(а):

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

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

[mserg]

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

mserg в сообщении #724777 писал(а):

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

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

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

Среди узкого круга лиц Вы будете абсолютно правы. Представление же народных масс, несколько иное. Поясню.
Читаем, что есть определение в математике из Гильберта и Бернайса «Основание математики». Определение в узком смысле слова есть

Цитата:

«простое разъяснение знаков с помощью введения символа, служащего сокращением для составного выражения.

Формализация «явного определения» (т.е. определения в узком смысле). Сие есть

Цитата:

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

(Есть там еще рекурсивные определения, но не будем тут.)

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

И начинается «консервативное расширение», «прикладная теория», «метатеории» и куча всего очень ценного и важного для лиц определенного круга. Если не так – поправьте.

А теперь, как на «самом деле» народные массы (к которым я отношусь) представляют себе «картину мира».
* Формальная теория единожды задается как принято у приличных людей (как написано в томах из библиотеки)
* Но, допускаются еще определения – это часть языка и формальной теории. Не верите? См. название темы.
* Определение используется аналогично аксиомам, но таковыми не являются. Поэтому список аксиом неизменен.
* Для обозначения функций и пр. используются не «символы», а имена. Например,sin – это не символ, а имя в виде слова из трех букв. Поэтому алфавит единожды определен и неизменен. Когда говорят о добавлении символа, то подразумевают создание имени из букв алфавита.
А раз так, то определения не приводят ни к изменению языка, ни к созданию новых теорий. Есть одна теория, в основе которой аксиомы. А вся остальная математика может быть получена в рамках одной формальной теории.
Незамутненное сознание представляет собой программу, в которой эта система запрограммирована. Методом «поиска в ширину» можно выйти на почти любой правильный математический результат.

Не может нормальный человек понять, зачем каждый раз, когда дается определение, нужна новая теория и изменение языка. Плюс к тому, непонятно, где правила для создания метатеории (в метаметатеории видимо, а для этой еще выше, и т.д. – т.е. нигде). И т.д.

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