Вычисления с бесконечным алфавитом

[Munin]

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

Эээээ, не передёргивайте, "не всё на свете", а вышеперечисленное. Получение значения конечной функции по заданному аргументу - это его "вычисление". Стало быть, функция - "вычислима" или "рекурсивна". Всё это одной теорией определяется

Одной теорией - ещё не значит, что всё это синонимы. Скажем, одной теорией определяются понятия "энергия" и "импульс" - это ещё их синонимами не делает.

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

Могу потратить (поверьте, зря) время и указать учебники и даже какие-то конкретные места из них.

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

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

Дело-то в том, что это никакой вовсе не "мой подход", а вполне себе общепринятый.

Дело в том, что отдельные ваши заявления звучат настолько необычно, что я в этом сомневаюсь. Именно их и прошу подтвердить учебниками. А не всю теорию. Заваливать меня кучей материала, со словами "сами разбирайтесь", я буду считать демагогическим уходом от вопроса.

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

Вот тут Вы ошибаетесь. Ибо в рамках логики первого порядка это не легко и вообще никак не лечится.

Господи, а я сказал "в рамках логики первого порядка"? Математики считают сами себя работающими на логике второго порядка, если не высших.

[epros]

Munin в сообщении #604773 писал(а):

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

Это хорошо, это конструктивно. Давайте теперь разберёмся с тем, что именно "звучит необычно" и почему.

(Оффтоп)

Если достаточно основательно покопаться в логике, то там такое море всякого "необычного"...

Может быть необычно звучит утверждение о том, что когда мы говорим "находя значение конечной функции по заданному аргументу мы его «вычисляем»", то мы автоматически подразумеваем, что "конечная функция «вычислима»"?

Munin в сообщении #604773 писал(а):

Господи, а я сказал "в рамках логики первого порядка"? Математики считают сами себя работающими на логике второго порядка, если не высших.

Вооот. А фишка в том, что с логиками более высоких порядков - всё ещё более непросто. Логика первого порядка - по крайней мере более или менее хорошо изучена, так что абсолютное большинство хоть где-то применимых теорий формализуются именно в ней.

[Munin]

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

Давайте теперь разберёмся с тем, что именно "звучит необычно" и почему.

Все, на которые я просил ссылки. Извините, мне сейчас уже неинтересно вспоминать и лень делать подборку.

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

Может быть необычно звучит утверждение о том, что когда мы говорим "находя значение конечной функции по заданному аргументу мы его «вычисляем»", то мы автоматически подразумеваем, что "конечная функция «вычислима»"?

Всё это звучит просто бессмысленно, поскольку ещё не введено понятие "конечной функции". Я знаю функции элементарные.

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

Вооот. А фишка в том, что с логиками более высоких порядков - всё ещё более непросто.

Да запросто.

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

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

Увы, у меня другие сведения. Да, логика первого порядка по крайней мере более или менее хорошо изучена, но абсолютное большинство хоть где-то применимых теорий - ZFC, стандартная арифметика, $\mathbb{R}$ и $\mathbb{C}$ и анализ в них, и всё, что на них навешано - формализуются в логике второго порядка. В этом как раз одна из проблем оснований математики, и на неё навешиваются всякие альтернативные подходы, однако же мэйнстримного признания не получившие. Мэйнстрим - это позиция типа "в логике второго порядка, наверное, всё это как-то образуется, для этого логику второго порядка надо бы изучить получше, но пусть этим занимается кто-то другой".

[epros]

Munin в сообщении #604788 писал(а):

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

Может быть необычно звучит утверждение о том, что когда мы говорим "находя значение конечной функции по заданному аргументу мы его «вычисляем»", то мы автоматически подразумеваем, что "конечная функция «вычислима»"?

Всё это звучит просто бессмысленно, поскольку ещё не введено понятие "конечной функции".

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

Munin в сообщении #604788 писал(а):

Я знаю функции элементарные.

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

(о птичках яблоках)

- Давайте поговорим о яблоках.
- Объясните пожалуйста, что такое "яблоко"?
- Да бросьте, все же прекрасно знают, что это такое.

Вот так яблоко и не стало математическим понятием: Потому что никто не потрудился дать ему определения.

Munin в сообщении #604788 писал(а):

Увы, у меня другие сведения. Да, логика первого порядка по крайней мере более или менее хорошо изучена, но абсолютное большинство хоть где-то применимых теорий - ZFC, стандартная арифметика, $\mathbb{R}$ и $\mathbb{C}$ и анализ в них, и всё, что на них навешано - формализуются в логике второго порядка.

Увы, Ваши сведения неверны. ZFC -теория первого порядка. Всякие "$\mathbb{R}$ и $\mathbb{C}$ и анализ в них, и всё, что на них навешано" формализуются в ZFC, то бишь в логике первого порядка. Касательно же "стандартной арифметики" - было приложено множество усилий к тому, чтобы дать ей более или менее адекватную формулировку в логике первого порядка, хотя выяснилось, что изначальное утверждение Пеано: "Нет других натуральных чисел", - в логике первого порядка невыразимо. И тем не менее, арифметика Пеано первого порядка была создана и успешно эксплуатируется. Так что в определённом смысле арифметика натуральных чисел - сильнее всех этих "$\mathbb{R}$ и $\mathbb{C}$ и анализа в них, и всего, что на них навешано".

А давайте проведём эксперимент. Полагаю, Вы не станете оспаривать, что физика - одна из тех наук, которые наиболее интенсивно используют математику. Вот я выскажу некое утверждение (может быть, не абсолютно бесспорное): Что ВСЕ используемые физикой математические понятия формализуемы в ZFC, т.е. в логике первого порядка, а значит необходимости использовать логику второго порядка в физике пока что нет. А Вы попытаетесь опровергнуть это утверждение примером. Уточняю: мне нужен пример не такого физического понятия, которое можно формализовать в логике второго порядка (таких полно), а пример такого, которое невозможно формализовать в логике первого порядка. И ещё уточнение на всякий случай: это понятие должно быть из теоретической физики, а не из "разговорной речи" (ибо в естественном языке можно накопать множество такого, что вообще непонятно как формализовать).

[Munin]

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

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

Во-первых, впервые слышу. Во-вторых, имхо, конечная таблица значений $\ncong$ конечная область определения.

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

А вот я никаких "элементарных" функций не знаю. Это - слово из обиходной речи, а не математический термин (в данном случае)

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

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

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

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

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

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

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

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

Вот я выскажу некое утверждение (может быть, не абсолютно бесспорное): Что ВСЕ используемые физикой математические понятия формализуемы в ZFC, т.е. в логике первого порядка, а значит необходимости использовать логику второго порядка в физике пока что нет. А Вы попытаетесь опровергнуть это утверждение примером.

А зачем? Я согласен. Физика использует математику далеко не на полную мощность. Например, что бы ни оказывалось в математике бесконечно, в физике рано или поздно оказывается конечно.

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

[epros]

Munin в сообщении #604834 писал(а):

Во-вторых, имхо, конечная таблица значений $\ncong$ конечная область определения.

Можете привести пример неравенства?

Munin в сообщении #604834 писал(а):

Надо вообще с нуля договариваться.

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

Munin в сообщении #604834 писал(а):

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

Это не я придумал. То, что вначале написал сам Пеано, потребовало формализации. Понимание математических понятий приходит к человечеству не сразу.

Munin в сообщении #604834 писал(а):

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

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

Про логику же второго порядка могу сказать только, что она - довольно странная штука, так что настороженное отношение к ней вполне объяснимо. В частности, в отличие от логики первого порядка, она неполна, т.е. вроде бы как «знает ответы» на некоторые (а может и на все) неразрешимые математические вопросы, но нам этих ответов не говорит - т.е. способа доказательства для них не существует. Всё это как-то странно и даже подозрительно...

[Munin]

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

Можете привести пример неравенства?

А, пардон, ошибся.

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

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

http://ru.wikipedia.org/wiki/Элементарные_функции
Цитата:

Элементарные функции — функции, которые можно получить с помощью конечного числа арифметических действий и композиций из следующих основных элементарных функций:


алгебраические:

степенная;
рациональная.
трансцендентные:

показательная и логарифмическая;
тригонометрические и обратные тригонометрические.

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

Это не я придумал. То, что вначале написал сам Пеано, потребовало формализации.

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

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

Про логику же второго порядка могу сказать только, что она - довольно странная штука

Ничего нового. Вы уже сказали, что она слабо изучена. Была бы не слабо изучена - была бы не странной. Была бы не странной - была бы хорошо изучена.

[мат-ламер]

Извиняюсь, что встреваю в спор, и прошу ногами не пинать. В своё время у меня был какой-то интерес к автоматическому доказательству теорем и даже осилил книгу Ченя и Ли на эту тему. Но вот что заметил. В этой книге авторы ограничились только теориями первого порядка. Попытался применить их методы к простейшим математическим понятиям, и понял, что даже самое элементарное не могу выразить в логике первого порядка. Как пример - не знаю как в этой логике записать аксиому полной математической индукции (аксиоматика целых чисел). Интерес мой к этой теме как-то поувял. Недавно смотрел обзоры по системам автоматического доказательства теорем. Они почти все сейчас основаны на логике высших порядков. Одна из популярных систем так и называется - HOL. Захотел что-нибудь популярно почитать о логике высших порядков, но в популярных учебниках ничего не нашёл. Если подскажете, что можно почитать. буду признателен. Обычно учебники строятся как-то странно. Сначала рассказывается о логике первого порядка и доказываются содержательные вещи о таких теориях. Кратко объясняется, что такое логика высших порядков, и выясняется, что для неё много не докажешь. Затем в книгах идёт приложения логики к конкретным вещам. И выясняется, что уже для арифметики нужна логика второго порядка. Может я чего не так понимаю.

[epros]

Munin в сообщении #605046 писал(а):

http://ru.wikipedia.org/wiki/Элементарные_функции

Это понятие не из теории вычислимости. Подмена понятий?

Munin в сообщении #605046 писал(а):

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

Когда Пеано это писал, понятий о разных порядках логики ещё не сложилось.

мат-ламер в сообщении #605080 писал(а):

не знаю как в этой логике записать аксиому полной математической индукции (аксиоматика целых чисел)

Аксиома индукции - это не самое элементарное понятие, её невыразимость логикой первого порядка - факт известный.

мат-ламер в сообщении #605080 писал(а):

Если подскажете, что можно почитать. буду признателен.

Не знаю как насчёт популярной, но вот хорошая вещь по логике второго порядка: Shapiro, S. Foundations without Foundationalism: A Case for Second-order Logic.

мат-ламер в сообщении #605080 писал(а):

выясняется, что для неё много не докажешь.

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

[Munin]

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

Это понятие не из теории вычислимости. Подмена понятий?

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

Вычислимость таких функций меня интересует. А не рассматривать их - не интересует. Это будет слишком скучно.

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

Когда Пеано это писал, понятий о разных порядках логики ещё не сложилось.

Ну понятно, Пеано во всём виноват. И он же заставил последующие поколения математиков назвать то, к чему он не имеет никакого отношения, своим именем.

Оставим это. Я про то, что называется именем Пеано, и выражается в логике второго порядка, а в первой - нет, как и было доказано. Готов называть это хоть трамваем.

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

Аксиома индукции - это не самое элементарное понятие

Зато достаточно логичное, чтобы её признавать и использовать в практической деятельности.

[epros]

Munin в сообщении #605181 писал(а):

Вычислимость таких функций меня интересует.

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

Munin в сообщении #605181 писал(а):

Зато достаточно логичное, чтобы её признавать и использовать в практической деятельности.

Кто ж спорит, на практике применяется. Вопрос только в полноте того, к чему она может применяться. Например, применив индукцию только к одному свойству натуральных чисел (что любое число либо нуль, либо имеет натурального предшественника), мы получим арифметику Робинсона - уже теорию, неполную Гёделевском смысле. Если применять индукцию только к примитивно-рекурсивным формулам, то получим примитивно-рекурсивную арифметику: достаточно сильную теорию, но всё же слабее арифметики Пеано. Если применять индукцию к любым формулам арифметики, то как раз получим арифметику Пеано первого порядка. Привлечение логики второго порядка потребуется только в том случае, если мы захотим применить индукцию вообще к любым свойствам чисел, включая невыразимые формулами языка.

[Munin]

Спасибо. Я в ступоре.

[мат-ламер]

(Оффтоп)

epros. Спасибо за ссылку.

[мат-ламер]

(Оффтоп)

epros. Спасибо за ссылку.

[A_J]

epros, извините что поднимаю относительно старую тему, но то что вы изложили очень интересно.
В этой связи у меня возник вопрос, и возможно вы сможете на него ответить. Вопрос такой - если мы возьмем вместо R множество всех вычислимых действительных чисел, и попробуем на этой базе построить "классический" анализ, то что из этого выйдет, и выйдет ли вообще что-нибудь путное? В частности интересно, что произойдет с такими понятиями как придел, интеграл, etc.

Можно ли получившийся в результате "конструктивный анализ" читать студентам вместе (или вместо) классического? Что становится проще а что сложнее при таком подходе? Что можно почитать на эту тему?