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

[epros]

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

«Лишние» аксиомы – это нонсенс. На это я и как бы намекаю – определение предела это не аксиома.

Почему «лишние»? Без них мы бы не узнали, что означает определяемое слово. Значит не лишнее.

И если определение предела не аксиома, то что? Я понимаю, что можно принять соглашение заменять одну комбинацию символов другой, но где и в какой форме, интересно, Вы собираетесь это соглашение записать?

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

Аксиоматическая система кажется ZCF. И далее разворачивается остальная математика.

Объявлять ZFC заменой всей математики — это слегка перебор.

[_hum_]

Xaositect
Да, спасибо, этот вариант понятен (Кстати, вопрос, современная математика таким путем и идет - выполняя консервативное расширение на каждое новое понятие?)

Но еще остается вопрос, а если не расширять теорию (оставаясь, например, в ZFC + логика предикатов), что в ней тогда будет отвечать определению отношения $<$ ? Незамкнутая логическая формула $\exists z (x + z = y)$? Если да, то можно ли это обобщить, сказав, что определения в формальной теории математики представляют собой ни что иное, как некоторые незамкнутые логические формулы?

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

Объявлять ZFC заменой всей математики — это слегка перебор.

Не всей математикой, а формальной системой для всей математики.

[Xaositect]

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

И если определение предела не аксиома, то что? Я понимаю, что можно принять соглашение заменять одну комбинацию символов другой, но где и в какой форме, интересно, Вы собираетесь это соглашение записать?

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

-- Чт май 16, 2013 20:18:32 --

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

Но еще остается вопрос, а если не расширять теорию (оставаясь, например, в ZFC + логика предикатов), что в ней тогда будет отвечать определению отношения ? Незамкнутая логическая формула ? Если да, то можно ли это обобщить, сказав, что определения в формальной теории математики представляют собой ни что иное, как некоторые незамкнутые логические формулы?

Можно сказать. Где-то я даже встречал специальный термин для формулы с "дырками", в которые можно подставлять термы.

[mserg]

Тогда еще вопрос. «Новый символ» – его же можно заменить номером. А номеров в одном языке можно наделать сколько надо. Так в чем счастье в создании новых языков?

[Xaositect]

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

Тогда еще вопрос. «Новый символ» – его же можно заменить номером. А номеров в одном языке можно наделать сколько надо. Так в чем счастье в создании новых языков?

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

[epros]

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

И плюс, в этом языке можно давать определения.

Вы так и не объяснили что это значит.

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

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

И если определение предела не аксиома, то что? Я понимаю, что можно принять соглашение заменять одну комбинацию символов другой, но где и в какой форме, интересно, Вы собираетесь это соглашение записать?

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

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

[arseniiv]

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

Где-то я даже встречал специальный термин для формулы с "дырками", в которые можно подставлять термы.

Не в $\lambda$-исчислении? Там это называлось контекст. Как в других местах, не знаю.

[epros]

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

Гл еще остается вопрос, а если не расширять теорию (оставаясь, например, в ZFC + логика предикатов), что в ней тогда будет отвечать определению отношения $<$ ? Незамкнутая логическая формула $\exists z (x + z = y)$? Если да, то можно ли это обобщить, сказав, что определения в формальной теории математики представляют собой ни что иное, как некоторые незамкнутые логические формулы?

А в чём ценность решения «не расширять»? Например, известно, что в ZFC можно вывести всю арифметику, включая не только сложения и умножения, но и возведения в степени, отношение порядка и т.д. При этом, разумеется, имеется в виду, что соответствующим арифметическим выражениям будут сопоставлены формулы ZFC. Можно их не заменять и каждый раз в предложении на тысячи символов высматривать эти формулы, кои тоже могут быть в сотни символов. А можно заменить и этим существенно упростить себе жизнь.

Тем более, что консервативность соответствующего расширения ZFC доказывается элементарно.

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

Не всей математикой, а формальной системой для всей математики.

Я это и имел в виду: сие есть слишком смелое заявление.

[Xaositect]

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

Кстати, вопрос, современная математика таким путем и идет - выполняя консервативное расширение на каждое новое понятие?

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

[mserg]

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

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

И плюс, в этом языке можно давать определения.

Вы так и не объяснили что это значит.

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

[epros]

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

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

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

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

[_hum_]

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

А в чём ценность решения «не расширять»?

В том, что "за деревьями становится виден лес" - минимальность дает возможность обозресть и понять, что же на самом деле происходит в математике.

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

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

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

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

Я это и имел в виду: сие есть слишком смелое заявление.

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

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

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

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

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

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

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

[arseniiv]

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

минимальность дает возможность обозресть и понять, что же на самом деле происходит в математике

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

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

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

Неоднократно вспоминаемые аксиомы сложения арифметики Пеано таковы:

$$\begin{array}{c} a + 0 = a, \\ a + b' = (a + b)'. \end{array}$$

Что не так?

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

[Xaositect]

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

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

А можете конкретные затруднения сформулировать? Переписывать построение модели PA в ZFC мне лень.

-- Пт май 17, 2013 00:20:25 --

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

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

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

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

[_hum_]

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

А можете конкретные затруднения сформулировать?

Ну, я хотел попытаться выразить на языке теории множеств натуральные числа и операции над ними. Сами объекты натуральных чисел вроде бы задаются легко - это подъязык языка множеств, в форме Бакуса-Наура задающийся грамматикой наподобие:
$<\mathrm{number}> \quad::=\quad \emptyset \quad |\quad '\{'<\mathrm{number}>, '\{'<\mathrm{number}>'\}''\}'$.

Тогда операция следования $s: n \mapsto n+1$ и отношение сравнения $m < n$ легко выражаются через конструкции:
$s(n) \rightarrow \{n,\{n\}\},\,m < n \rightarrow m \in n,$
а вот какой конструкции языка теории множеств соответствует сложение $m + n$ я так и не смог понять.

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

Истинность в любой модели для логики предикатов эквивалентна выводимости.

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

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

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

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