2014 dxdy logo

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

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




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

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

 
 
 
 Re: Функциональный символ = всюду определённая функция?
Сообщение24.05.2012, 11:47 
Ну да, проще доказывать что-то для всюду определенных функций. Если хочется частично определенные — можно либо доопределить нужные функции как-нибудь и потом учитывать это всякий раз, когда про них что-то говорится, либо рассматривать не функцию, а ее график — $n$-арное отношение.

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

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

 
 
 
 Re: Функциональный символ = всюду определённая функция?
Сообщение24.05.2012, 12:49 
Да, если Вы рассматриваете функцию как отношение, то ее определенность всюду — факт, который может выполняться или не выполняться. В Вашем примере с разностью Вы на самом деле определяете не функцию, а тернарное отношение, и в некоторых моделях оно не является графиком всюду определенной функции.

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

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

 
 
 
 Re: Функциональный символ = всюду определённая функция?
Сообщение24.05.2012, 14:06 
Не нужно, поскольку по определению функция определена всюду.

 
 
 
 Re: Функциональный символ = всюду определённая функция?
Сообщение24.05.2012, 14:53 
Аватара пользователя
apriv в сообщении #575590 писал(а):
Не нужно, поскольку по определению функция определена всюду.
По какому определению? Насколько я знаю, $S(n)$ определяется несколькими аксиомами, среди которых ничего нет про всюду определённость.

 
 
 
 Re: Функциональный символ = всюду определённая функция?
Сообщение24.05.2012, 15:15 
Аватара пользователя
apriv писал(а):
В Вашем примере с разностью Вы на самом деле определяете не функцию, а тернарное отношение, и в некоторых моделях оно не является графиком всюду определенной функции.
А почему аналогично нельзя сказать, что и в аксиоматике Пеано $S$ -- это не функция, а бинарное отношение $S(x, y)$? В последнем случае $\forall x \exists y S(x,y)$ не обязано выполняться.

 
 
 
 Re: Функциональный символ = всюду определённая функция?
Сообщение24.05.2012, 19:50 
Аватара пользователя
Продолжение песни:

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

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

 
 
 
 Re: Функциональный символ = всюду определённая функция?
Сообщение24.05.2012, 22:53 
epros в сообщении #575602 писал(а):
По какому определению? Насколько я знаю, определяется несколькими аксиомами, среди которых ничего нет про всюду определённость.

Есть, конечно. По определению функции.
epros в сообщении #575756 писал(а):
Мне пояснили, что в «современной логике» каждый функциональный символ автоматически подразумевает соответствующую аксиому всюду определённости.

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

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

 
 
 
 Re: Функциональный символ = всюду определённая функция?
Сообщение25.05.2012, 10:25 
Аватара пользователя
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 писал(а):
слово «функция» подразумевает что-то всюду определенное.
Кстати, это сильно спорный философский вопрос. Например, разность несомненно является «функцией», однако ее всюду определённость имеет место только тогда, когда в качестве области значений рассматривается множество целых чисел, а не множество натуральных.

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

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

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

 
 
 
 Re: Функциональный символ = всюду определённая функция?
Сообщение25.05.2012, 15:37 
Аватара пользователя
epros в сообщении #576116 писал(а):
Xaositect, я из себя ничего не строю, а просто задаю вопрос в разделе «помогите разобраться» (ну, может ещё иногда слегка выражаю недоумение ответами).
Простите, погорячился.
epros в сообщении #576116 писал(а):
Это мне тоже дюже удивительно.
А что тут удивительного? Как раз формальное применение чисто синтаксических правил.

 
 
 [ Сообщений: 14 ] 


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