Отделилась ли логика от математики?

[george66]

На arxiv.org два раздела "логика", один в математике, другой в computer science. В первом теория моделей (которая уже давно часть алгебры) и заповедник статей про большие кардиналы, во втором всё более свежее. Прошу тех, кому не лень, посмотреть вот эту книжку
http://gen.lib.rus.ec/search.php?req=Ty ... column=def
"Type Theory and Formal Proof", Nederpelt & Geuvers, 2014 (книжка сама по себе доходчивая) и сказать своё мнение -- это та же самая математика, где дают премии за вычисление гомотопий, или какая-то другая?

[vicvolf]

george66 в сообщении #1373217 писал(а):

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

Это скорее философский вопрос, который сродни вопросу - что Вы понимаете под математикой?

[vicvolf]

Если говорить конкретно о компьютерным доказательствах, то они относятся к тому разделу математики, где проводится доказательство. В отношении теории компьютерных доказательств, то мое личное мнение, что эту теорию можно считать разделом математической логики, а следовательно отнести к данному разделу математики. Однако, думаю, что могут быть другие мнение, которые относят эту теорию к computer science. О вкусах не спорят! Хотя есть один существенный момент - вопрос присуждения степени - физмат наук или технических.

[beroal]

george66 в сообщении #1373217 писал(а):

теория моделей (которая уже давно часть алгебры)

А я думал, что универсальная алгебра — это часть теории моделей.

(Оффтоп)

Что скажете о таком тезисе: информатика (computer science) минус прикладная психология есть раздел математики?

$$\text{информатика}\setminus \text{«прикладная психология»} \subseteq \text{математика}$$

[george66]

beroal в сообщении #1402656 писал(а):

Что скажете о таком тезисе: информатика (computer science) минус прикладная психология есть раздел математики?

Уже давно почти вся интересная математическая логика делается в computer science.

[Мастак]

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

[Munin]

george66
А computer science, по-вашему, не является ли разделом математики?

[arseniiv]

Мастак в сообщении #1414113 писал(а):

Потом на стыке - математическая логика.

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

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

[george66]

Смотря какая computer science. Если быстрая сортировка, то это раздел прикладной математики. А вот вся теория типов -- это как-то совсем перпендикулярно.

[arseniiv]

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

-- Вс сен 08, 2019 17:30:30 --

По классификации, которую приводил kry, это будут точные формальные науки (видимо, не обязательно целиком, могут быть подмножеством). В просто формальные попадают куски например философии, в просто точные, скажем, физика.

[beroal]

arseniiv в сообщении #1414129 писал(а):

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

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

[Munin]

george66 в сообщении #1414126 писал(а):

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

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

[george66]

Посмотрите книжку в начале темы (я поправил ссылку). По моему впечатлению, это не та математика, где вычисляют гомотопии и даже Воеводский не смог увлечь гомотопных математиков теорией типов.

[Munin]

Я не думаю, что вся математика "вычисляет гомотопии". Даже если посмотреть arXiv, мне кажется, математика шире.

(Честно говоря, я плохо понимаю, что означает "вычисляют гомотопии". Я знаком только с гомотопиями в топологии. Мне кажется, это достаточно узкая тема, по сравнению с математикой в целом. Хотя сам термин "гомотопии" я видел во многих других разделах математики. И не вижу, а чем он несовместим с теорией типов.)

[Red_Herring]

Старая частушка на новый лад писал(а):

А я типы изучала от утра до вечера,
Гомотопьи ж вычисляли два больших компьютерá