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

[EminentVictorians]

sour в сообщении #1542259 писал(а):

Матлогика нужна чтобы слова поменьше писать.

Какие слова?

[sour]

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

[EminentVictorians]

sour в сообщении #1542317 писал(а):

Для любого, существует, принадлежит, пересесечение, объединение и т.д. и т.п.. Значками лучше это все обозначать.

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

Мне же хочется узнать, какая цель у матлогики. Ради чего все это предприятие затевалось?

[sour]

EminentVictorians
А что значит цель? У всего ли обязана быть цель? Какая цель у математики? Какая цель у жизни?

[lel0lel]

sour

(Оффтоп)

"Когда у общества нет цветовой дифференциации штанов, то нет цели, а когда нет цели…"

Благо, на нашем форуме цветовая дифференциация есть)

[Someone]

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

Мне же хочется узнать, какая цель у матлогики. Ради чего все это предприятие затевалось?

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

[EminentVictorians]

lel0lel в сообщении #1542337 писал(а):

А что значит цель?

Выберите любой раздел математики. Я какие повспоминал - везде есть понятный предмет, методы и цели.

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

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

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

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

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

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

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

[lel0lel]

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

lel0lel в сообщении #1542337 писал(а):

А что значит цель?

Выберите любой раздел математики. Я какие повспоминал - везде есть понятный предмет, методы и цели.

Это не мой вопрос, своё видение цели я обрисовал в офтопе.

[EminentVictorians]

(Оффтоп)

lel0lel, извините. Я процитировал неправильно.

[Someone]

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

Как мы рассуждаем? Я бы ответил так: с помощью обычной человеческой логики.

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

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

Зачем, например, мне знать про какое-то исчисление предикатов, чтобы согласиться с истинностью того факта, что Сократ смертен?

Извините, но задачи, стоящие перед математиками (и далеко не только перед математиками), много сложнее, чем доказательство смертности Сократа. А предикаты — это свойства объектов. Если Вы не хотите говорить о свойствах, то говорить будет не о чем. Даже в вашем примере про Сократа есть минимум два предиката.

[EminentVictorians]

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

очищенная от ненадёжных рассуждений

А вот я по умолчанию считаю, что любое логичное рассуждение человека надежно. Да, можно возразить, мол люди часто ошибаются, думая, что рассуждают логично. Например, люди раньше думали, что все непрерывные функции дифференцируемы. Я бы ответил так: ну так они и не рассуждали логично. Понятие "число", "непрерывность", "дифференцируемость" элементарно даже определены не были. Т.е. они рассуждали не логично, вот и ошиблись. Что в этом удивительного?

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

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


Про ненадежность можно еще привести в пример парадоксы, типа Рассела. Что вот, мол, обычные рассуждения привели к ерунде. Но. Мы же про непротиворечивость $ZFC$ ничего не знаем, верно? Т.е. парадоксы могут быть и там. Установить средствами $ZFC$ ее же непротиворечивость, насколько я понимаю, мы тоже не можем. Так чем же она тогда лучше?

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

Извините, но задачи, стоящие перед математиками (и далеко не только перед математиками), много сложнее, чем доказательство смертности Сократа.

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

[Someone]

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

В тех учебниках, которые я читал, была человеческая логика.

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

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

Чему Вы, собственно, удивляетесь?

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

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

Да. И сделано это с использованием математической логики. Не формализованной. Математики, видите ли, учатся рассуждать аккуратно, с использованием математической логики, но не формализованно. Вероятно, в учебнике математической логики Вы видели образцы формализованной логики. Формализацию математики без особой нужды не делают, но понимают, что можно формализовать, а что нельзя. Если рассуждение формализовать нельзя, то оно не годится.

[EminentVictorians]

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

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

А что значит "формализовать" вообще? Просто я понимаю, что значит формализовать в рамках такой то формальной теории, например $ZFC$. Тогда такую-то формулу будем считать истинной, если она является последней строчкой в своем формальном выводе. Под "формализовать" имелось в виду "формализовать в $ZFC$"?

[Someone]

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

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

Не истинной, а выводимой. Это разные понятия.

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

Под "формализовать" имелось в виду "формализовать в $ZFC$"?

Почему "в ZFC"? ZFC — это просто одна из формальных теорий. Правда, очень мощная, в ней можно интерпретировать много-много математических теорий, причём, так, что аксиомы теории станут теоремами ZFC (такая интерпретация называется моделью). Вы это имели в виду? Например, арифметика стандартно формализуется сама по себе. Хотя её можно интерпретировать в ZFC. Всякие логики тоже формализуется сами по себе. Но я поостерёгся бы утверждать, что в ZFC можно интерпретировать всё на свете.

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

[EminentVictorians]

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

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

Т.е. если я говорю "Пусть $G$ - конечная группа", получается, что я определил неформализуемый в $ZFC$ объект?

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

Да. И сделано это с использованием математической логики. Не формализованной.

Вот этот момент я тоже не понимаю. Я помню тот пример Ван дер Вардена с нигде не дифференцируемой функцией. Откуда там матлогика? Там же обычные наивные рассуждения, просто функция как функция. Просто Вы, видимо, вкладываете в слово "матлогика" иной смысл, чем я. Из процитированного фрагмента я вижу, что Вы различаете матлогику и формальную логику. А я вот не понимаю, чем они различаются. Точнее так: я под матлогикой понимаю все эти термы, формулы формальной теории и т.д. Взять теорему о полноте и корректности исчисления высказываний: каждая тавтология является теоремой и наоборот. Что тавтологии, что теоремы - это формальные записи в некотором алфавите и грамматике, удовлетворяющие определенным условиям (для тавтологий - тождественная истинность на любом логическом векторе входящих переменных, для теорем - факт того, что они выводимы). Т.е. тут чисто синтаксические штуки. Я под матлогикой вот это все понимаю.