2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




На страницу Пред.  1, 2, 3, 4  След.
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 19:12 
Аватара пользователя
mserg в сообщении #724660 писал(а):
«Лишние» аксиомы – это нонсенс. На это я и как бы намекаю – определение предела это не аксиома.
Почему «лишние»? Без них мы бы не узнали, что означает определяемое слово. Значит не лишнее.

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

mserg в сообщении #724660 писал(а):
Аксиоматическая система кажется ZCF. И далее разворачивается остальная математика.
Объявлять ZFC заменой всей математики — это слегка перебор.

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 19:14 
Xaositect
Да, спасибо, этот вариант понятен (Кстати, вопрос, современная математика таким путем и идет - выполняя консервативное расширение на каждое новое понятие?)

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


epros в сообщении #724736 писал(а):
Объявлять ZFC заменой всей математики — это слегка перебор.

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

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 19:15 
Аватара пользователя
epros в сообщении #724736 писал(а):
И если определение предела не аксиома, то что? Я понимаю, что можно принять соглашение заменять одну комбинацию символов другой, но где и в какой форме, интересно, Вы собираетесь это соглашение записать?
В метатеории можно записать. Типа в формальной теории у нас ограниченный язык, но в мы будем рассматривать также "расширенный" язык формул, которые определенным алгоритмом переводятся в правильно построенные формулы теории. Вот этот алгоритм и есть совокупность определений новых символов.

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

_hum_ в сообщении #724738 писал(а):
Но еще остается вопрос, а если не расширять теорию (оставаясь, например, в ZFC + логика предикатов), что в ней тогда будет отвечать определению отношения ? Незамкнутая логическая формула ? Если да, то можно ли это обобщить, сказав, что определения в формальной теории математики представляют собой ни что иное, как некоторые незамкнутые логические формулы?
Можно сказать. Где-то я даже встречал специальный термин для формулы с "дырками", в которые можно подставлять термы.

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 19:18 
Тогда еще вопрос. «Новый символ» – его же можно заменить номером. А номеров в одном языке можно наделать сколько надо. Так в чем счастье в создании новых языков?

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 19:21 
Аватара пользователя
mserg в сообщении #724743 писал(а):
Тогда еще вопрос. «Новый символ» – его же можно заменить номером. А номеров в одном языке можно наделать сколько надо. Так в чем счастье в создании новых языков?
Да, можно еще и так. Но тогда эквивалентность, говорящая, а что же номер означает, должна быть в посылках любой теоремы, этот символ использующей.

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 19:27 
Аватара пользователя
mserg в сообщении #724724 писал(а):
И плюс, в этом языке можно давать определения.
Вы так и не объяснили что это значит.

Xaositect в сообщении #724739 писал(а):
epros в сообщении #724736 писал(а):
И если определение предела не аксиома, то что? Я понимаю, что можно принять соглашение заменять одну комбинацию символов другой, но где и в какой форме, интересно, Вы собираетесь это соглашение записать?
В метатеории можно записать. Типа в формальной теории у нас ограниченный язык, но в мы будем рассматривать также "расширенный" язык формул, которые определенным алгоритмом переводятся в правильно построенные формулы теории. Вот этот алгоритм и есть совокупность определений новых символов.
Да я понимаю, что есть разные варианты. Например, можно добавить правило вывода, которое заменяет части формул. Я просто хотел услышать от mserg его вариант.Потому что с моей точки зрения все эти построения на уровне метатеории по сути всё равно являются способом определить новую (расширенную) теорию.

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 19:47 
Xaositect в сообщении #724739 писал(а):
Где-то я даже встречал специальный термин для формулы с "дырками", в которые можно подставлять термы.
Не в $\lambda$-исчислении? Там это называлось контекст. Как в других местах, не знаю.

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 19:50 
Аватара пользователя
_hum_ в сообщении #724738 писал(а):
Гл еще остается вопрос, а если не расширять теорию (оставаясь, например, в ZFC + логика предикатов), что в ней тогда будет отвечать определению отношения $<$ ? Незамкнутая логическая формула $\exists z (x + z = y)$? Если да, то можно ли это обобщить, сказав, что определения в формальной теории математики представляют собой ни что иное, как некоторые незамкнутые логические формулы?
А в чём ценность решения «не расширять»? Например, известно, что в ZFC можно вывести всю арифметику, включая не только сложения и умножения, но и возведения в степени, отношение порядка и т.д. При этом, разумеется, имеется в виду, что соответствующим арифметическим выражениям будут сопоставлены формулы ZFC. Можно их не заменять и каждый раз в предложении на тысячи символов высматривать эти формулы, кои тоже могут быть в сотни символов. А можно заменить и этим существенно упростить себе жизнь.

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

_hum_ в сообщении #724738 писал(а):
Не всей математикой, а формальной системой для всей математики.
Я это и имел в виду: сие есть слишком смелое заявление.

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 19:53 
Аватара пользователя
_hum_ в сообщении #724738 писал(а):
Кстати, вопрос, современная математика таким путем и идет - выполняя консервативное расширение на каждое новое понятие?
Современная математика не парится по этому поводу, поскольку считает, что любой из уже трех подмеченных путей (подстановки в метатеории, консервативные расширения, добавление всех используемых определений в посылки) работает и работает одинаково, а писать формальные заклинания не нужно - если кому-то надо, сам напишет.

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 20:04 
epros в сообщении #724753 писал(а):
mserg в сообщении #724724 писал(а):
И плюс, в этом языке можно давать определения.
Вы так и не объяснили что это значит.

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

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 20:38 
Аватара пользователя
mserg в сообщении #724777 писал(а):
надо взять подвыражение какой-нибудь теоремы, назначить ему символ, перечислить свободные переменные или что там еще надо? Пользование: подстановка определения в теоремы - с помощью алгоритма унификации. Как-то так.
Это понятно, что использование такого определения заключается в замене в формулах чего-то на что-то. Вопрос в том, в какой форме Вы хотите записать само это определение.

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

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 21:37 
epros в сообщении #724770 писал(а):
А в чём ценность решения «не расширять»?

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

epros в сообщении #724770 писал(а):
Например, известно, что в ZFC можно вывести всю арифметику, включая не только сложения и умножения, но и возведения в степени, отношение порядка и т.д.

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

epros в сообщении #724770 писал(а):
Я это и имел в виду: сие есть слишком смелое заявление.

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

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

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

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

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

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 22:51 
_hum_ в сообщении #724826 писал(а):
минимальность дает возможность обозресть и понять, что же на самом деле происходит в математике
Многие вещи можно определять по-разному, и, подставляя вместо них их громоздкие выражения, как можно хоть что-то понять?

_hum_ в сообщении #724826 писал(а):
Я когда-то пытался это понять, но на моменте представления в ZFC операции сложения любых двух натуральных чисел наткнулся на то, что без рекурсии вроде бы не обойтись. В то же время в формальной теории рекурсия вроде бы нигде не может участвовать (разве что в определении синтаксиса языка теории посредством формальных грамматик). И опять для меня началось "размытие" понятия языка теории и метаязыка. Если у вас все прошло хорошо, поделитесь соображениями.
Неоднократно вспоминаемые аксиомы сложения арифметики Пеано таковы:$$\begin{array}{c} a + 0 = a, \\ a + b' = (a + b)'. \end{array}$$Что не так?

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

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение16.05.2013, 23:06 
Аватара пользователя
_hum_ в сообщении #724826 писал(а):
Я когда-то пытался это понять, но на моменте представления в ZFC операции сложения любых двух натуральных чисел наткнулся на то, что без рекурсии вроде бы не обойтись. В то же время в формальной теории рекурсия вроде бы нигде не может участвовать (разве что в определении синтаксиса языка теории посредством формальных грамматик). И опять для меня началось "размытие" понятия языка теории и метаязыка. Если у вас все прошло хорошо, поделитесь соображениями.
А можете конкретные затруднения сформулировать? Переписывать построение модели PA в ZFC мне лень.

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

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

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

 
 
 
 Re: Как в аксиом. подходе формализуются определения ?
Сообщение17.05.2013, 00:16 
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 писал(а):
Конечно, для доказательства разных свойств сложения (коммутативности, например) сначала придётся использовать соответствующую аксиому индукции.

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

 
 
 [ Сообщений: 55 ]  На страницу Пред.  1, 2, 3, 4  След.


Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group