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

[epros]

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

Слово «определение» ни разу не встретилось в вашем ответе.

Так это был не ответ, а вопрос Вам, и не про "определение", а про то, что Вы собираетесь заменять в языке.

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

Слева от “<=>” видим обозначения предела, справа – то, что под пределом понимается. Так даются определения в математике. После введения понятия предела, можно им пользоваться (левой частью). Если не вводить определение предела, то пришлось бы всегда пользоваться выражением из правой части. Что неправильно в моем понимании, и где ваш термин для «определения».

Ничего неправильного кроме того, что это не "в языке", а в прикладной теории (которая определяет пределы). И это определение с формальной точки зрения записывается аксиомой оной теории.

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

[mserg]

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

[epros]

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

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

Что-то я не понял этого аргумента. Ну, не используйте эту аксиому — и обойдётесь без неё.

[_hum_]

Господа, давайте уточним вопрос. До сегодняшнего дня я считал, что вся современная математика акиоматизируема, то есть, существует какой-то вариант фиксированной формальной системы со своим раз и навсегда заданным набором аксиом и правилами вывода (типа теории множеств + логики предикатов + геометрии), которая позволяет выразить любой математический результат через понятия этой теории. Например, всякую математическую теорему позволяет представить в виде корректной формулы, выводимой по правилам вывода из аксиом.
Я ошибался?
Если не ошибался, тогда вопрос, а как в таком случае обстоят дела с представлением (средствами этой теории) определений новых математических понятий? Первичные понятия (как, например, множество, пустое множество) в формальной теории, насколько я понимаю, фиксируются в самом языке (в cинтаксисе, допускающем, например, использование (определенным образом) конструкций вида $ \emptyset$ или $\{ \emptyset\}$, кои можно рассматривать как обозначения соответствующих первично-неопределяемых понятий - пустого множества и множества, содержащего пустое множество). А как быть с определениями остальных понятий современной математики? Неужели они все, действительно, лишь "синтаксический сахар" для сокращенного обозначения некоторой синтаксически корректной конструкции формальной теории, как, например, натуральные числа в теории множеств:

$0 ::= \emptyset$

$1 ::= \{ \emptyset\}$

$2 ::= \{ \emptyset, \{ \emptyset\}\}$

...

$n+1 ::= n \cup \{n\}$.


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

Если же ошибся в целом, то как обстоят дела на самом деле, и что тогда означает "аксиоматизируемость математики"?

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

У Рассела был такой оператор $\iota$. Терм $\iota x.F(x)$ означал объект, для которого выполняется $F$, если он единственен. Аксиома для использования этой штуки была что-то типа $G(\iota x . F(x)) \Leftrightarrow \exists ! x (F(x)) \& \forall y (F(y)\to G(y))$ (по смыслу такая, с конкретной формулировкой могу врать)

А это не есть просто попытка в аксиоматику засунуть часть синтаксиса? И еще, Вы говорите, что это Рассел использовал, а теперь как дела обстоят?

[Sonic86]

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

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

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

[mserg]

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

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

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

Что-то я не понял этого аргумента. Ну, не используйте эту аксиому — и обойдётесь без неё.

Ну, минимум аксиом – это как бы альфа и омега связности и надежности всей математики. Аксиомы – это минимум предположений – все остальное (ну хорошо, почти все) должно выводиться из них. Никакие другие промежуточные аксиомы не нужны (или не должны быть нужны). «Лишние» аксиомы – это нонсенс. На это я и как бы намекаю – определение предела это не аксиома.
------
На счет того, где все выводится из одной аксиоматической теории – ответ уже был. Это Бурбаки. Начинается с языка. Аксиоматическая система кажется ZCF. И далее разворачивается остальная математика.

[Xaositect]

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

Ну, минимум аксиом – это как бы альфа и омега связности и надежности всей математики. Аксиомы – это минимум предположений – все остальное (ну хорошо, почти все) должно выводиться из них. Никакие другие промежуточные аксиомы не нужны (или не должны быть нужны). «Лишние» аксиомы – это нонсенс. На это я и как бы намекаю – определение предела это не аксиома.

Минимальность списка аксиом и их независимость - это как раз вещь самая необязательная.
Мы можем добавить новые символы и аксиомы и доказать, что это не расширяет множество доказуемых утверждений, не содержащих новых символов. Это называется "консервативное расширение".

-- Чт май 16, 2013 18:35:29 --

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

ZCF

ZFC, Zermelo-Fraenkel set theory with Choice

[mserg]

Т.е. определение предела - это аксиома?

[Xaositect]

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

Т.е. определение предела - это аксиома?

Можно понимать и так.
Можно, как Вы говорите: что последовательность символов $\lim x_n = x$ - это сокращение для длинной формулы с кванторами, а формулы формальной теории этих символов не содержат.
А можно и так, что определение предела - это аксиома, и после введения этой аксиомы мы начинаем работать в консервативном расширении исходной теории.

[mserg]

Сначала говорят, что аксиома принимается без доказательств. Потом говорят, что добавление аксиом должно сопровождаться доказательством (в консервативном расширении). Я понимаю, что математика – наука строгая, но должны же быть какие-то пределы…

Так все же, что есть определение, чем оно отличается от аксиом? В чем суть разница?

[_hum_]

Sonic86 в сообщении #724650 писал(а):

С тех пор и считают, что аксиоматизации математика полностью не поддается

Хм...А как тогда доказывается истинность математических утверждений, если, Вы говорите, в той же формальной теории множеств+логики предикатов некоторые из них могут оказаться невыводимы из ее аксиом? Как тогда вообще происходит развитие математики, и в чем состоит работа математиков, если смотреть "с высоты птичьего полета"?

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

На счет того, где все выводится из одной аксиоматической теории – ответ уже был. Это Бурбаки. Начинается с языка. Аксиоматическая система кажется ZCF. И далее разворачивается остальная математика.

Книга Бурбаки разве начиналась с определения формальной грамматики языка ZFC, логики с последующей точной формулировкой правил вывода? Давно это было, но даже намека на это в моей памяти не осталось. По-моему, там все тоже "на пальцах", как в большинстве учебников по ФАН.

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

Re: Как в аксиом. подходе формализуются определения ? Сообщение Чт май 16, 2013 18:34:12
mserg в сообщении #724660 писал(а):
Ну, минимум аксиом – это как бы альфа и омега связности и надежности всей математики. Аксиомы – это минимум предположений – все остальное (ну хорошо, почти все) должно выводиться из них. Никакие другие промежуточные аксиомы не нужны (или не должны быть нужны). «Лишние» аксиомы – это нонсенс. На это я и как бы намекаю – определение предела это не аксиома.
Минимальность списка аксиом и их независимость - это как раз вещь самая необязательная.
Мы можем добавить новые символы и аксиомы и доказать, что это не расширяет множество доказуемых утверждений, не содержащих новых символов. Это называется "консервативное расширение".

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

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

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

Т.е. определение предела - это аксиома?

Можно понимать и так.
Можно, как Вы говорите: что последовательность символов $\lim x_n = x$ - это сокращение для длинной формулы с кванторами, а формулы формальной теории этих символов не содержат.
А можно и так, что определение предела - это аксиома, и после введения этой аксиомы мы начинаем работать в консервативном расширении исходной теории.

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

[Xaositect]

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

Сначала говорят, что аксиома принимается без доказательств. Потом говорят, что добавление аксиом должно сопровождаться доказательством (в консервативном расширении). Я понимаю, что математика – наука строгая, но должны же быть какие-то пределы…

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

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

Так все же, что есть определение, чем оно отличается от аксиом? В чем суть разница?

С точки зрения работы с ними - никакой разницы.

-- Чт май 16, 2013 19:26:29 --

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

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

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

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

Давайте я приведу пример.
Допустим, я хочу взять какую-нибудь общепринятую аксиоматику арифметики Пеано, в ней нет символа $\leqslant$. Я хочу этот символ определить, причем я хочу, чтобы это был именно символ формальной теории, нравится мне так.
И вот я говорю: давайте введем новый символ $\leqslant$ и такую аксиому: $\forall x \forall y (x\leqslant y \leftrightarrow \exists z (x + z = y))$.
Дальше я говорю: если у нас есть доказательство, которое использует символ $\leqslant$, то я могу по свойству эквивалентных формул любую подформулу вида $A\leqslant B$ заменить на подформулу $\exists t (A + t = B)$, где $t$ - новая переменная. Это значит, что множество доказуемых утверждений, не использующих $\leqslant$, остается тем же, то есть расширение консервативно.
Теперь по поводу моделей. Я говорю, что для любой модели исходной теории существует модель новой теории, в которой все старые символы имеют ту же интерпретацию (просто определяю интерпретацию нового предикатного символа). И наоборот, любая модель новой теории автоматически является моделью старой. То есть опять же, если формула без $\leqslant$ была истинна в любой модели исходной теории, то она будет истинна и в любой модели новой, и наоборот.

[arseniiv]

(2 _hum_.)

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

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

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

[mserg]

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

[Xaositect]

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

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

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