Функциональный символ = всюду определённая функция?

[epros]

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

Мне это кажется каким-то бредом. Может я чего-то не понимаю?

[apriv]

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

[epros]

Тут дело вот в чём: Я полагаю, что всюду определённость функции - это нетривиальный факт, который нужно доказывать. В частности, всюду определённость функции инкремента $S(n)$ в арифметике натуральных чисел - без добавления в теорию соответствующей аксиомы недоказуема. А мне говорят, что «семантика» уже подразумевает всюду определённость всего, для чего в теории предусмотрен функциональный символ. Какая, на фиг, семантика? Невозможность доказать всюду определённость - чисто синтаксический факт.

Например, добавив к арифметике Пеано бинарный функциональный символ «$-$» и аксиому $\forall k,m,n ~ (k = m - n \leftrightarrow k + n = m)$, мы получим теорию, в которой будет доказуемо, что $\nexists k ~ (k = 0 - 1)$. Т.е. функция разности в этой теории не всюду определена. И это чисто синтаксический факт. Как его можно отрицать с помощью каких-то «семантических» соображений?

[apriv]

Да, если Вы рассматриваете функцию как отношение, то ее определенность всюду — факт, который может выполняться или не выполняться. В Вашем примере с разностью Вы на самом деле определяете не функцию, а тернарное отношение, и в некоторых моделях оно не является графиком всюду определенной функции.

[epros]

Я рассматриваю функцию чисто формально: как нечто, определяемое функциональным символом $f$ и набором аксиом. А всюду определённость - как доказанное утверждение $\forall x \exists y ~ y = f(x)$.

Так значит, нужна всё же в арифметике Пеано аксиома $\forall x \exists y ~ y = S(x)$?

[apriv]

Не нужно, поскольку по определению функция определена всюду.

[epros]

apriv в сообщении #575590 писал(а):

Не нужно, поскольку по определению функция определена всюду.

По какому определению? Насколько я знаю, $S(n)$ определяется несколькими аксиомами, среди которых ничего нет про всюду определённость.

[svv]

apriv писал(а):

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

А почему аналогично нельзя сказать, что и в аксиоматике Пеано $S$ -- это не функция, а бинарное отношение $S(x, y)$? В последнем случае $\forall x \exists y S(x,y)$ не обязано выполняться.

[epros]

Продолжение песни:

Мне пояснили, что в «современной логике» каждый функциональный символ автоматически подразумевает соответствующую аксиому всюду определённости.

Что за фигня? Нафига это нужно? По-моему, это только создает проблемы с формализацией частично определенных функций. Т.е. придётся доопределять, например, разность между меньшим и большим числами нулями: $\nexists z ~ (z + x = y) \to y - x = 0$. А если мне эта лишняя аксиома в теории не нужна?

[apriv]

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

По какому определению? Насколько я знаю, определяется несколькими аксиомами, среди которых ничего нет про всюду определённость.

Есть, конечно. По определению функции.

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

Мне пояснили, что в «современной логике» каждый функциональный символ автоматически подразумевает соответствующую аксиому всюду определённости.

Что за фигня? Нафига это нужно? По-моему, это только создает проблемы с формализацией частично определенных функций. Т.е. придётся доопределять, например, разность между меньшим и большим числами нулями

Зато это не создает проблем при доказательстве теорем относительно этих аксиоматических систем — про всюду определенные функции доказывать все проще, чем следить за областью определения. Разность можно доопределять, а можно говорить, что это тернарное отношение, см. выше. Ничего страшного при этом не произойдет — в обычной математике разность и так не является функцией на квадрате натуральных чисел, потому что слово «функция» подразумевает что-то всюду определенное.

[epros]

apriv в сообщении #575888 писал(а):

Есть, конечно. По определению функции.

По какому ещё «определению функции»? Вы о формальной теории говорите или о чём? В формальной теории не бывает никаких «определений функций», ибо она определяется набором аксиом. Так что аксиома всюду определённости либо есть в этом наборе, либо её там нет.

apriv в сообщении #575888 писал(а):

Зато это не создает проблем при доказательстве теорем относительно этих аксиоматических систем — про всюду определенные функции доказывать все проще, чем следить за областью определения.

Не вижу никаких проблем. Либо теория позволяет доказать наличие значения у функции, либо нам придётся обойтись без этого.

apriv в сообщении #575888 писал(а):

Разность можно доопределять, а можно говорить, что это тернарное отношение, см. выше.

Вы сейчас пытаетесь навязать мне Ваш собственный вариант аксиоматики. А я хочу пользоваться своим. Имею я право просто добавить к арифметике Пеано аксиому $\forall k,m,n ~ (k=m-n \leftrightarrow k+n=m)$ и рассматривать ТАКУЮ теорию? Или она автоматически будет считаться противоречивой, потому что в ней можно доказать $\nexists k ~ (k=0-1)$, а из мифического «определения функции» следует, что $\exists k ~ (k=0-1)$?

-- Пт май 25, 2012 11:35:26 --

apriv в сообщении #575888 писал(а):

слово «функция» подразумевает что-то всюду определенное.

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

[Xaositect]

epros, не стройте из себя альта. Есть общепринятая терминология, в которой функции всюду определены И в аксиомах PA нет $\forall x \exists y (y = s(x))$. Хотите где-нибудь у себя частичные функции --- напишите аккуратно об этом в первом параграфе или сошлитесь куда-нибудь, например, http://imps.mcmaster.ca/doc/mech-trad-approach.pdf .

[epros]

Xaositect, я из себя ничего не строю, а просто задаю вопрос в разделе «помогите разобраться» (ну, может ещё иногда слегка выражаю недоумение ответами). «Функция» может означать что угодно, но вопрос здесь был не о концептуальном представлении о функциях, а о синтаксических аспектах формальных теорий: Здесь, собственно, нет никаких «функций», а есть только «функциональные символы».

Мне интересно, в силу каких именно аксиом я обязан, вводя в теорию функциональный символ (например, «-»), заботиться о всюду определённости? Мне тут сказали, что из $f(0)=f(0)$ (это следует из аксиом эквивалентности) можно вывести $\exists x ~ x=f(0)$ - якобы соответствующее правило вывода можно применять ТАКИМ образом. Это мне тоже дюже удивительно.

[Xaositect]

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

Xaositect, я из себя ничего не строю, а просто задаю вопрос в разделе «помогите разобраться» (ну, может ещё иногда слегка выражаю недоумение ответами).

Простите, погорячился.

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

Это мне тоже дюже удивительно.

А что тут удивительного? Как раз формальное применение чисто синтаксических правил.