Основания математики - элементарное рассмотрение

[Dialectic]

tatle11be в сообщении #408651 писал(а):

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

С какой это стати мышление осуществляется по логическим законам?Мы же видим, как люди рассуждают не логично, а значит, мышление не осуществляется по логическим законам. Уже из одного того, что мы можем ошибаться, и неправильно мыслить мы тем свидетельствуем, что мы не мыслим логически и наше мышление целиком им (законам) не подчинено. Или нет?

[vek88]

Dialectic в сообщении #408669 писал(а):

С какой это стати мышление осуществляется по логическим законам?Мы же видим, как люди рассуждают не логично, а значит, мышление не осуществляется по логическим законам. Уже из одного того, что мы можем ошибаться, и неправильно мыслить мы тем свидетельствуем, что мы не мыслим логически и наше мышление целиком им (законам) не подчинено. Или нет?

Уважаемый Dialectic

Мы ведь тут раскорячились между естественным интеллектом, искусственным интеллектом, математической логикой и основаниями математики. А потому, будучи так вот раскоряченными, очень тежело здесь ляпнуть что-нибудь такое, чтобы и волки сыты были, и овцы съедены.

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

Вот конкретный пример - спор о соотношении матлогики и оснований.

tatle11be в сообщении #408651 писал(а):

Но , в любом случае, это вопрос принипиальный - касается понимания иерархии между Мат.лог-й и Основ. мат-ки , а не терминологии
Или я не прав?

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

Более сложный пример на стыке программирования и ИИ - уже упоминавшийся язык ПРОЛОГ. Здесь для объяснения формы и смысла языка уже необходимо исчисление предикатов. Ну зачем, скажите на милость, мне упоминать это в контексте оснований?

А вот когда заговорим об аксиоматике теории множеств - вот тогда пожалуйста - это уже основания. Но уж к информатике или ИИ это ИМХО, практически, никак не относится.

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

С уважением,
vek88

[vek88]

Итак, кто-нибудь объяснит мне, что изменится в нашем мире в зависимости от того, куда мы засунем матлогику?

Вот epros, например, засунул ее глубоко в основания

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

Матлогика - сама лежит в основаниях математики, причём довольно глубоко

А tatle11be пока мается, и не знает, куда ее засунуть.

tatle11be в сообщении #408651 писал(а):

это вопрос принипиальный - касается понимания иерархии между Мат.лог-й и Основ. мат-ки , а не терминологии

А я ее никуда не сунул - у меня она сама по себе в статусе самостоятельного раздела математики.

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

Если уж Мюнхаузена вспомнили, то давайте вспомним Свифта - у него спорили остроконечники и тупоконечники.

Так что ИМХО - суйте, господа, матлогику, куда хотите. Ей - матлогике - от этого ни холодно, ни жарко.

[Dialectic]

vek88 в сообщении #408780 писал(а):

Итак, кто-нибудь объяснит мне, что изменится в нашем мире в зависимости от того, куда мы засунем матлогику?
Вот epros, например, засунул ее глубоко в основания

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

Матлогика - сама лежит в основаниях математики, причём довольно глубоко

А tatle11be пока мается, и не знает, куда ее засунуть.

tatle11be в сообщении #408651 писал(а):

это вопрос принипиальный - касается понимания иерархии между Мат.лог-й и Основ. мат-ки , а не терминологии

А я ее никуда не сунул - у меня она сама по себе в статусе самостоятельного раздела математики.

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

Если уж Мюнхаузена вспомнили, то давайте вспомним Свифта - у него спорили остроконечники и тупоконечники.

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

[epros]

vek88 в сообщении #408780 писал(а):

Итак, кто-нибудь объяснит мне, что изменится в нашем мире в зависимости от того, куда мы засунем матлогику?

vek88 в сообщении #408780 писал(а):

А я ее никуда не сунул - у меня она сама по себе в статусе самостоятельного раздела математики.

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

[vek88]

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

vek88 в сообщении #408780 писал(а):

Итак, кто-нибудь объяснит мне, что изменится в нашем мире в зависимости от того, куда мы засунем матлогику?

vek88 в сообщении #408780 писал(а):

А я ее никуда не сунул - у меня она сама по себе в статусе самостоятельного раздела математики.

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

Согласен на любые дискуссии, если от них хоть кому-нибудь хоть какая-нибудь польза.

Что касается всех разделов математики, также как многих разделов других наук (ИИ, информатика, программирование, ...), не могу представить себе их независимость от матлогики. Но это не значит, что матлогика их часть, или они - часть матлогики. Матлогика в других разделах математики и в других науках используется как математический метод для формального представления или разъяснения конкретных вопросов этих разделов математики или этих других наук.

В качестве примера снова приведу язык ПРОЛОГ (ПРОграммрование ЛОГическое, PROgramming in LOGic). Кстати, по своему опыту знаю, что многие профессиональные матлогики, например, Г.Е. Минц, живо интересовались ПРОЛОГом. Но это совсем не означает, что ПРОЛОГ - часть матлогики или наоборот. Это всего лишь означает, что ПРОЛОГ возник и развивался, как говорят, на стыке наук (программирования, ИИ, матлогики). А для матлогиков это была некоторая прикладная область, в которой они могли применить свои математические познания.

[epros]

vek88 в сообщении #408989 писал(а):

Согласен на любые дискуссии, если от них хоть кому-нибудь хоть какая-нибудь польза.

Ну, о пользе каждый судит самостоятельно.

vek88 в сообщении #408989 писал(а):

Что касается всех разделов математики, также как многих разделов других наук (ИИ, информатика, программирование, ...), не могу представить себе их независимость от матлогики.

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

[vek88]

vek88 в сообщении #408780 писал(а):

Итак, кто-нибудь объяснит мне, что изменится в нашем мире в зависимости от того, куда мы засунем матлогику?

vek88 в сообщении #408780 писал(а):

Что - кто-то из нас будет матлогику применять правильно, а кто-то нет?

На эти мои два вопроса никто не ответил.

vek88 в сообщении #408989 писал(а):

Согласен на любые дискуссии, если от них хоть кому-нибудь хоть какая-нибудь польза.

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

о пользе каждый судит самостоятельно.

По моему суждению пользы от нашей дискуссии нет. Вместо пользы пошли элементы троллинга, в частности, на мои вопросы я не получаю ответы. А ведь я задавал эти вопросы ради уточнения смысла/пользы нашей дискуссии. А вместо этого пошла подмена понятий:

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

vek88 в сообщении #408989 писал(а):

Что касается всех разделов математики, также как многих разделов других наук (ИИ, информатика, программирование, ...), не могу представить себе их независимость от матлогики.

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

[mserg]

vek88 в сообщении #408554 писал(а):

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

vek88,
Только я так и не понял, где та самая формальная система, из которой по формальным правилам можно вывести почти все остальное... Если эта система есть, то как, для примера, вводятся функция sin, понятие интеграла, случайная величиная, комплексная переменная? У меня не получается из формальной системы, которую предложил Гилберт и Ко, сделать такой формальный вывод...

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

Может быть, уважаемый epros сможет это сделать?

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

Есть еще вопросы «типов». И есть множество аксиоматических систем вплоть до определения действительных чисел и теории вероятности. Они, эти аксиоматические системы, определяются на тех самых «основаниях математики» или создаются сами по себе как-то сбоку, а потом скрещиваются друг с другом как яблоня с березой?

Повторюсь, но я просто пытаюсь представить, из какой такой формальной системы выводится почти все в современной математике.

[vek88]

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

vek88 в сообщении #408554 писал(а):

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

vek88,
Только я так и не понял, где та самая формальная система, из которой по формальным правилам можно вывести почти все остальное... Если эта система есть, то как, для примера, вводятся функция sin, понятие интеграла, случайная величиная, комплексная переменная? У меня не получается из формальной системы, которую предложил Гилберт и Ко, сделать такой формальный вывод...

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

Может быть, уважаемый epros сможет это сделать?

(1) Я не понял содержание ответа. Это проблемы только формальной системы Гилберта с Бернайсом? Или же у всех примерно одно и то же? Или мы просто не умеем этим пользоваться?

(2) Есть еще вопросы «типов». И есть множество аксиоматических систем вплоть до определения действительных чисел и теории вероятности. Они, эти аксиоматические системы, определяются на тех самых «основаниях математики» или создаются сами по себе как-то сбоку, а потом скрещиваются друг с другом как яблоня с березой?

(3) Повторюсь, но я просто пытаюсь представить, из какой такой формальной системы выводится почти все в современной математике.

1. Да, 100 лет назад Гильберт думал, что надежное обоснование математики возможно на основе финитных формальных систем.

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

2. Вообще то ИМХО задачу аксиоматизации всей математики в рамках финитных систем никто не ставил. И понятно почему. Это, прежде всего, исключительно трудоемко. Представьте себе, что Вам поручили написать оригинальный курс матанализа - Вы ведь не сможете написать его и за год.

Кроме того, здесь, в определенном смысле, все не так как всегда. В результате Вас просто не поймут.

Хотите пример? Смотрите понятие конструктивного действительного числа в конструктивном анализе.

3. А вот какую задачу действительно ставили - эту аксиоматизация теории множеств. Смысл понятен. Поскольку понятие множества лежит в основе математических построений, вот эту основу и хотят поставить на надежное основание. В результате было построено несколько аксиоматизаций теории множеств - см. в Википедии.

Мой взгляд на весь этот огород, если кратко, состоит в следующем. В финитных формальных системах обосновать математику в принципе невозможно. А вот в подходящих нефинитных формальных системах (полные К-системы или $\Delta_1^1$-множества) все прекрасно. И даже наивная теория множеств Кантора прекрасно себя чувствует. Если, конечно, не давать некорректных определений, т.е. определений, нарушающих полноту К-систем. Простейший путь избежать некорректных определений - держаться подальше от циклических определений и/или цепочек определений.

Но и при нарушении полноты ничего страшного не случится - мы просто выйдем за пределы классической двузначной логики.

Подробности см. выше в этой теме.

[vek88]

Вот еще несколько замечаний к вопросу "о формализации всей математики".

vek88 в сообщении #409463 писал(а):

Вообще то ИМХО задачу аксиоматизации всей математики в рамках финитных систем никто не ставил. И понятно почему. Это, прежде всего, исключительно трудоемко.

По поводу трудоемкости и, я бы сказал, занудности, добавлю следующее. Вот, например, существование универсальной канонической системы Поста. Если пояснять это неформально, то все относительно просто. А вот строгое доказательство, т.е. построение в явном виде нескольких десятков аксиом и правил вывода - это, согласитесь, весьма занудно. См. стр. 28-29 Мартин-Леф Очерки по конструктивной математике.

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

vek88 в сообщении #409463 писал(а):

Кроме того, здесь, в определенном смысле, все не так как всегда.

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

А возьмем формализацию анализа в К-системе (в духе наивной теории множеств) - будет ли это чем-либо интересно? И стоит ли уродоваться с этим? ИМХО нет, поскольку мы получим в этом случае формальное представление в точности того, что мы знаем и так в традиционном матанализе.

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

Как общественность смотрит на подобную шизу? Интересно ли это кому-нибудь?

[mserg]

Имеет смысл следующая задача: исходя из основ (теории множеств?), дать формальное определение математических понятий, функций и т.п., широко используемых в современной математике. Тогда формальным образом можно будет получать/проверять новые математические результаты. Если есть целостное формальное описание – то его смогут использовать компьютерные системы, в том числе и системы искусственного интеллекта. Если описание мат-аппарата клочкообразное, то в компьютерных системах клочки сами по себе не соединятся, как в голове человека. Компьютеру, как принято говорить, о здравом смысле ничего не известно. Общепринятые обозначения необходимы, в том числе, и для того, чтобы пользователи компьютерных систем могли «общаться» с ними на привычном математическом языке. Сам же детальный вывод результатов матанализа не нужен. Нужно, так сказать, просто обеспечить целостность формального вывода – сам вывод не нужен.

Насчет определения синуса в теории множеств, конечно, идеи есть. Сначала нужно определить понятие предела, затем понятие производной. Потом можно составить соответствующее дифференциальное уравнение и сказать, что результат его решения – это функция синус. Аналогично с другими функциями.

P.S.
В реальной жизни, с учетом требованием эффективности компьютерных систем, обеспечить реализацию формальных систем невозможно. В реальной полезной компьютерной системе будут присутствовать «ложные теоремы» и с этим нужно жить. См. например, сюда:
http://np-soft.ru/npproject/research/ai/index.htm.
Это просто инженерный набросок идей многолетней давности, поэтому строго судить не нужно. Раз в системе могут быть «ложные теоремы», то никто нам не запрещает пытаться вводить новые гипотезы (аксиомы). Если в дальнейшем выяснится, что она выводима – объявляем гипотезу теоремой. Если обнаружится, что гипотеза ложная – все результаты на ее основе должны быть пересмотрены. Если ни то, ни другое – гипотеза будет жить в «статусе аксиомы». Т.е. лично меня неполнота формальных систем нисколько не беспокоит, и «невыводимые» в формальной системе теоремы могут быть получены и использоваться в реальной жизни. Как мне кажется, просто мир формальных систем не совсем адекватно соотносится с реальностью... Но это так, мысли вслух.

[AV_77]

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

Имеет смысл следующая задача: исходя из основ (теории множеств?), дать формальное определение математических понятий, функций и т.п., широко используемых в современной математике.

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

[vek88]

AV_77 в сообщении #409641 писал(а):

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

Имеет смысл следующая задача: исходя из основ (теории множеств?), дать формальное определение математических понятий, функций и т.п., широко используемых в современной математике.

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

Согласен. Хотя на досуге, лежа на диване, полистать какой-нибудь том Бурбаки - это клево.

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

Насчет определения синуса в теории множеств, конечно, идеи есть. Сначала нужно определить понятие предела, затем понятие производной. Потом можно составить соответствующее дифференциальное уравнение и сказать, что результат его решения – это функция синус. Аналогично с другими функциями.

А чего ж тут горбатиться? Ведь это все давно определено. И замечу - прекрасно определено.

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

vek88 в сообщении #409548 писал(а):

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

Как общественность смотрит на подобную шизу? Интересно ли это кому-нибудь?

Вот я и предлагаю десяток другой этих определений записать в виде К-системы (это будет теория). А затем посмотреть, какие метатеоремы можно будет вывести из этой теории. При этом окажется, что эти метатеоремы в точности совпадут с общеизвестными теоремами этой начальной части матана (без всяких завихрений типа КДЧ и т.д.).

Этим я хочу проиллюстрировать тот факт, что математике никакого специального обоснования в общем-то и не требуется. Здравый смысл математиков и реальная практика - это и есть обоснование математики. В этом я согласен с уважаемым epros:

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

По моим понятиям основания математики обосновываются не матлогикой, а ... гхм ... практикой и здравым смыслом.

Причем реальная практика - это, в том числе, и практика инженеров, использующих математику для расчета мостов, ракет и т.д.

Так как, нам интересно на примере начал анализа увидеть, что в "наивной" математике и без всяких обоснований все прекрасно, т.е. полно и непротиворечиво?

[mserg]

Я же написал, что мне бы нужна формальная система для «компьютера». Зачем мне отвечать, что есть отличная неформальная система для людей? Вы там курите что ли?