Так ли уж бесполезна матлогика?

[x-code]

Я айтишник/программист, и моими любымими курсами в ВУЗе были как раз таки Дискретная математика и Мат.логика! Просто обожал их. С удовольствием бы изучал углубленно, но на тот момент таких шикарных возможностей в изучении чего угодно через интернет не было, а направление обучения было все-же немного другим (хотя тоже интересным).
А оказывается есть еще и "неклассические логики" - модальная логика, нечеткая логика, многозначная логика, линейная логика, интуиционисткая логика и т.д. И еще всякие символьные вычисления, компьютерные доказательства теорем и т.д. , но увы я всё это не изучал.

[Red_Herring]

Моя точка зрения: матлогика нужна, но в каком объеме? Я бы сказал, существенно в меньшем, чем сейчас. Профессиональному математику (не матлогику) нужно уметь свободно оперировать с логическими конструкциями, включающие кванторы, а вот выводимость и прочее ни к чему. К сожалению, структура любого университетского курса довольно жесткая, и таких маленьких курсов, как нужно, нет. В университетах США/Канады гибкости еще неизмеримо меньше: обычно 2-3 ч лекций, и м.б. 1-2 ч. туториалов в неделю (если говорить о математике, и родственных дисциплинах). И матлогики в качестве обязательного курса нет.

[drzewo]

Просто из личного опыта.

(Оффтоп)

Немного логики есть в начале первого тома <<Анализ >> Лорана Шварца и первого тома Зорича. Еще студентом я понял, что мне необходимо в этом разобраться. До сих пор мне этого хватает для занятий анализом и дуфурами. Многие мои товарищи и в таком объеме логику не изучали -- им хватает интуиции.

[mishatv]

<script>alert('sdf')<\script>

[Ende]

mishatv
Вы, товарищ, что имели в виду?

[Geen]

Ende в сообщении #1655319 писал(а):

Вы, товарищ, что имели в виду?

Форум взломать пытается...

[george66]

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

[EminentVictorians]

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

поэтому скоро математики будут друг другу ставить баллы за красоту идеи (как в фигурном катании)

По-моему, нормальный подход.

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

Я говорю, что есть пруфчекинг

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

[dgwuqtj]

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

поэтому скоро математики будут друг другу ставить баллы за красоту идеи (как в фигурном катании)

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

[george66]

Было бы полезно поучить пруфчекеру Metamath. Это несложно, увлекательно и хорошо проясняет, чем вообще занимается математическая логика и какая от неё может быть польза математику. А так, математическая логика от математики оторвалась и ушла в computer science.

[EminentVictorians]

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

и какая от неё может быть польза математику

А в общих чертах рассказать можете?

[george66]

Раньше математики "решали трудные задачи". С некоторых пор стали "выдумывать прекрасное". Чтобы математика окончательно не превратилась в абстрактное искусство, надо больше работать лопатой. Вот Metamath позволяет с нуля записывать всяческие аксиомы, правила вывода и доказательства на очень простом языке. В силу своей низкоуровневости он неудобен практически (грубо говоря, как писать большие программы на ассемблере), но тренировка очень хорошая. А то будет по Вербицкому "А вот я придумал inf-гомотопии с подвывертом!" Судьи "6.0! 6.0! 6.0!"

[Klein]

Red_Herring в сообщении #1654470 писал(а):

Моя точка зрения: матлогика нужна, но в каком объеме? Я бы сказал, существенно в меньшем, чем сейчас. Профессиональному математику (не матлогику) нужно уметь свободно оперировать с логическими конструкциями, включающие кванторы, а вот выводимость и прочее ни к чему. К сожалению, структура любого университетского курса довольно жесткая, и таких маленьких курсов, как нужно, нет. В университетах США/Канады гибкости еще неизмеримо меньше: обычно 2-3 ч лекций, и м.б. 1-2 ч. туториалов в неделю (если говорить о математике, и родственных дисциплинах). И матлогики в качестве обязательного курса нет.

Сейчас выбираем учебную программу бакалавра по математике для 16 летнего в Австралии.
Остановились на Австралийском Национальном Университете.

Первый год 4 предмета в каждом семестре. Принимают отличников. Студентов из верхней группы 5% по общим результатам и 1-2% по математике.

Первый курс.
Первый семестр

Анализ и Линейная Алгебра.
Дискретная математика (несколько лекций по математической логике)
Статистика
И отдельный предмет
Решение задач и доказательства. Пару обязательных книг, в том числе книга Пойа.
Задачи из разных областей математики со строгими доказательствами.

This course focuses on the language of mathematical arguments. Rather than attacking advanced topics, we will use simple mathematics to develop an understanding of how results are established. We begin with clearly stated and plausible assumptions or axioms and then develop a more and more complex theory from them. The course, and the lecturer, will have succeeded if you finish the course able to construct valid arguments of your own and to criticise those that are presented to you.
https://programsandcourses.anu.edu.au/course/math2222

Студенты утверждают, что предмет сложный и по уровню задач и по объему работы.

Во втором семестре тоже похожий предмет с задачами и доказательствами с уклоном на темы из дискретной математике.
---

И еще интересный момент. На факультете Arts and Social Sciences в Сиднейском университете (один из ведущих ВУЗов страны и старейший университет в Австралии (1850г)) на кафедре философии 5 предметов по логике
1 курс – вступление, 2 курс– 2 предмета, 3 курс – 2 предмета.
https://www.njjsmith.com/philosophy/tea ... ylogic.pdf

На достойном уровне. По сравнению с тем что предлагают на многих учебных программах по математике это намного лучше.
Почему так?

[EminentVictorians]

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

А то будет по Вербицкому "А вот я придумал inf-гомотопии с подвывертом!" Судьи "6.0! 6.0! 6.0!"

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

Но вообще говоря, я пока как-то не очень понял основной посыл. Вопрос был про пользу матлогики. Ну приходим мы к математику и говорим ему: "Ты занимаешься какой-то фигней, иди лучше в metamath покопайся". Знаете, как-то не вдохновляет. Где польза то?

[мат-ламер]

EminentVictorians в сообщении #1665310 писал(а):

Вопрос был про пользу матлогики.

EminentVictorians в сообщении #1665310 писал(а):

Где польза то?

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

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