Зачем нужна матлогика?

[EminentVictorians]

Mikhail_K в сообщении #1542480 писал(а):

Чем Вам не нравятся математические доказательства как предмет изучения?

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

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

[Mikhail_K]

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

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

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

Так же и с доказательствами. Хотите Вы этого или нет, но существует математически строгая теория математических доказательств, она же математическая логика. Так что, предмет изучения у неё вполне определён.

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

[Nemiroff]

(Оффтоп)

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

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

$\mathbb{R}$ чёрт знает как устроен, так что это вообще тривиально.
Вот что вещи из обычного $\mathbb{N}$ зависят от эфемерных сущностей, это сперва кажется странным. Типа BusyBeaver. Но потом возникает идея, что натуральные числа не "обычные" и "понятные", они скорее "изначальные" -- без готовых, заранее взятых натуральных чисел ничего не построить.

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

Но пока я не могу усвоить, в чем их общность или различие.

Это потому что вы не слушаете ответы, а просто повторяете одно и то же, чтоб "шороху навести".

[mihaild]

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

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

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

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

Я уверен, что доказательство у Вас (итоговое - правильное) было обычным рассуждением, а не простыней кванторов и стрелок

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

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

Контринтуитивное утверждение, как то так. Ну и разумеется, в моем понимании они оба - не парадоксы.

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

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

Я возьму в классической логике вывод сделаю с использованием закона исключенного третьего, а интуиционист не примет. Получается, что определение существует, но не для всех и не одно. Но ладно интуиционисты, а ультрафинитисты? Уже 3 разных определения получается.

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

Nemiroff в сообщении #1542471 писал(а):

Тут сперва нужно определить (конечную) последовательность.

Ну естественно понятия конечной строки в алфавите и базовые операции с такими строками считаем известными:)

[EminentVictorians]

Mikhail_K в сообщении #1542486 писал(а):

существует математически строгая теория математических доказательств, она же математическая логика.

Вот я и говорю, а точно ли она математически строгая? А обычная логика не будет ли строже формальной? Да, я наверное слишком много вопросов для одной темы задал. Матлогику я скорее всего еще немного поизучаю. Сам я там точно не разберусь, но темы постараюсь здесь более конкретные создавать.

Но послушайте мои аргументы.

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

-- 11.12.2021, 21:49 --

Nemiroff в сообщении #1542487 писал(а):

без готовых, заранее взятых натуральных чисел ничего не построить.

Вот кстати да! А не проще ли в качестве изначального, у всех людей одинаковым образом формализованного куска базовой интуиции взять натуральные числа, а не всю эту историю с формальными системами?

[Nemiroff]

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

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

Этот кусок а) не формализован одинаковым образом, б) тем не менее всё равно всегда берётся как изначальный.

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

Но почему никого не смущает, что с самого начала построения формальной теории мы пользуемся индукцией по построению формул.

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

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

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

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

[EminentVictorians]

Nemiroff в сообщении #1542493 писал(а):

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

А поподробнее этот момент пояснить можете?

[Mikhail_K]

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

Но послушайте мои аргументы.

Эти аргументы интереснее.

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

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

[maximav]

EminentVictorians
Ну возьмите хотя бы дебаты про "C" в аббревиатуре ZFC, про верхние/нижние грани, континуальность вещественных чисел, трансфинитные числа, исключение третьего и, вообще, все то, что из матлогики плавно перекочевало - давно - в основания математики. Это далеко не матанализ. Матанализ для логики - это прикладнуха. Причем сама матлогика - это не просто привычная всем логика. Там существенно буквоедство во всем. И чтобы никаких парадоксов. Вот этим перебиранием косточек она - матлогика - и занимается. Не матанализом.

[Someone]

Mikhail_K в сообщении #1542379 писал(а):

Someone в сообщении #1542365 писал(а):

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

Гм. Ну, как я понимаю, определить конечное множество в ZFC можно. Например как неравномощное любому своему собственному подмножеству (и непустое при этом).

Стандартно в теории множеств конечное множество определяют как множество, равномощное одному из натуральных чисел, причём, под "натуральным рядом" подразумевается наименьшее индуктивное множество. Определение Дедекинда равносильно стандартному в ZFC, но не равносильно ему в ZF.

Цитата:

Другое дело, что будут существовать модели, в которых определённые так "конечные" множества будут "на самом деле" бесконечными, ну так что с того?

Так об этом речь и идёт. Та же ZFC имеет нестандартные модели, в которых есть натуральные числа, бесконечные с точки зрения метатеории.

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