Связь формальной и неформальной логики

[EminentVictorians]

Выделю отдельную тему, чтобы не загромождать предыдущую.

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

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

Про пустое множество уже был разговор, но я хотел бы еще раз обсудить.

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

Вот пример доказательства в ZFC, что пустое множество единственно:

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

А Ваш вариант доказательства каков?

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

Теорема.
Пустое множество единственно.

Доказательство:
Предположим, нашлись 2 различных пустых множества $\varnothing_1$ $\ne$ $\varnothing_2$. Раз они различны, значит существует элемент $x$, принадлежащий одному из них и не принадлежащий другому. Получаем 2 варианта:
1) $x \in \varnothing_1$ и $x \notin \varnothing_2$
2) $x \in \varnothing_2$ и $x \notin \varnothing_1$

Первый случай приводит к противоречию, т.к. получается, что пустое множество $\varnothing_1$ непусто (т.к. содержит элемент $x$). По этой же причине и второй случай приводит к противоречию. Получается, что к противоречию приводит наше предположение о существовании двух различных пустых множеств. Следовательно, пустое множество единственно, чтд.

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

[Anton_Peplov]

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

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

[Mikhail_K]

EminentVictorians
Ну в Вашем примере на скриншоте вполне обычное рассуждение, только записанное без использования слов. Логика там та же самая, что и у Вас. Вас просто напугала эта громоздкость, а если не пугаться, а просто посмотреть внимательнее и разобраться, то можно даже получить от этого удовольствие. Но тут, конечно, уж слишком подробно всё расписано, это запись не для человека, а для компьютера. Важно, что можно было бы то же рассуждение написать и короче, с использованием слов, и всё равно имея в виду про себя использование аксиом логики. То есть тут не логика "нечеловеческая", а просто запись не очень человеческая, слишком скрупулёзная.

(1) означает, что существует пустое множество $x$, которому ничего не принадлежит. Это аксиома.
(2)-(5) означает, что если какое-то множество $y$ равно этому пустому множеству $x$, то игреку тоже ничего не принадлежит - просто по смыслу равенства. Замечу, что если в доказываемом утверждении (25) вместо $\leftrightarrow$ написать $\to$, то фрагмент (2)-(5) не потребуется, а смысл будет всё равно почти тот же самый.

Дальше и до самого конца идёт доказательство, что и наоборот, если какому-то множеству ничего не принадлежит, то оно равно нашему пустому множеству $x$ - это и значит, что нет двух пустых множеств. То есть из предположения (6) надо вывести $x=y$. В свою очередь, для этого сначала в (7)-(10) доказывается, что если какой-то элемент $z$ принадлежит $y$, то он принадлежит и $x$ (просто потому что по предположению игреку не может ничего принадлежать, а из лжи следует что угодно), а затем в (11)-(14) так же доказывается, что и наоборот, из принадлежности $x$ следует принадлежность $y$. Дальше в (15)-(20) на основании этого получается, что $x=y$, со ссылкой на аксиому экстенсиональности (если два множества состоят из одних и тех же элементов, то они равны). Содержательная часть доказательства на этом закончена, дальше просто происходит формирование доказываемого утверждения в том виде, в каком оно должно быть.

Словами то же самое доказательство я бы изложил так. По аксиоме пустого множества, существует пустое множество $\varnothing$. Докажем, что если $\varnothing^\prime$ тоже пустое, то $\varnothing^\prime=\varnothing$. В самом деле, из $x\in\varnothing^\prime$ (как из заведомой лжи) следует $x\in\varnothing$, и наоборот. По аксиоме экстенсиональности $\varnothing^\prime=\varnothing$. Значит, пустое множество единственно.

Для меня это одно и то же доказательство, только по-разному записанное, и логика тут одна и та же. Ваше доказательство немного другое, от противного, его тоже можно было бы записать формально, и от этого логика в нём бы не изменилась.

[EminentVictorians]

Anton_Peplov в сообщении #1699695 писал(а):

Формальные доказательства - это запись "на ассемблере".

И теперь представьте, программируете Вы на том же си шарпе, написали какой-то код. Потом к Вам приходит человек и спрашивает Вас какой-то вопрос, но не про си шарп, а про CIL (Common Intermediate Language), мол, как переведется такая-то строчка вашего C# кода в CIL. Сможете ответить? Ну, как минимум, наверное Вам придется сильно подумать. Плюс, для этого надо знать устройство компилятора C#. В общем, вопрос нетривиальный.

А в математике этой проблемы как будто нету. Вот делаю я какое-нибудь рассуждение в обычном матане ("на C#"). Потом ко мне приходит человек и говорит: "да забей ты на эти пределы, вот тебе бесконечно малые, все нормально, используй их, главное следи, чтобы все утверждения с ними формулировались в логике первого порядка". Как я должен за этим следить? Реально переводить все свои "обычные" рассуждения в простыню кванторов? Потому что это звучит примерно как от Вас требовать, чтобы Вы писали на си шарпе, а параллельно следили, чтобы потом ваша программа каким-то специальным образом распарсилась в CIL. Это же нереально...

[Mikhail_K]

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

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

А кто так говорит? Нестандартный анализ - это своеобразное развлечение специально для фанатов математической логики (хотя есть ещё подход со стороны теории ультрафильтров). Для всех остальных есть обычный математический анализ.

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

[Anton_Peplov]

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

А в математике этой проблемы как будто нету.

Еще как есть. Чтобы формализовать доказательство какой-нибудь теоремы Вейерштрасса из стандартного учебника по матану, мне тоже, как минимум, придется сильно подумать. Особенно без навыка в деле формализации доказательств. Вы же сами жалуетесь, что формальная запись доказательства тривиальнейшей теоремы о единственности пустого множества Вас "вымораживает". И не только Вас, а всех. Это не удобочитаемый для человека язык. Поэтому до сих пор формализовано не так уж много доказательств. Даже не знаю, все ли теоремы, входящие, скажем, в учебник Зорича, уже формализованы.

[dgwuqtj]

Формальные доказательства нужны вообще не для того, чтобы их выписывать. Они нужны для доказательств каких-то метаутверждений. Например, есть теорема Джекобсона: любое (ассоциативное и с единицей) кольцо $R$, удовлетворяющее тождеству $x^n = x$ для фиксированного $n \geq 2$, коммутативно. Оно доказывается через всякую структурную теорию колец.

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

[EminentVictorians]

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

А кто так говорит?

Так весь смысл нестандартно анализа в элементарной эквивалентности $\mathbb R$ и $^*\mathbb R$. А элементарная эквивалентность - это формальное понятие, про формальные объекты (что истинны одни и те же замкнутые формулы). Подход Нельсона (через IST) - та же пертушка. Смысл в том, что IST консервативна над ZFC, но чтобы эту консервативность не сломать - это надо супер аккуратно следить, какие там формулы внутренние, какие не внутренние, какие кванторы что связывают и тд. Это совсем не тот "неформальный" стиль, к которому привыкли обычные студенты, читающие обычного Зорича.

[EminentVictorians]

dgwuqtj в сообщении #1699703 писал(а):

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

По типу "Теорема Гудстейна недоказуема в арифметике Пеано первого порядка"?

dgwuqtj в сообщении #1699703 писал(а):

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

Это и есть результат, который дала матлогика? То есть не факт справедливости теоремы Джекобсона, а факт возможности её доказательства элементарными средствами?

[dgwuqtj]

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

По типу "Теорема Гудстейна недоказуема в арифметике Пеано первого порядка"?

Да. Чтобы не терять время на поиски доказательства.

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

То есть не факт справедливости теоремы Джекобсона, а факт возможности её доказательства элементарными средствами?

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

[EminentVictorians]

dgwuqtj в сообщении #1699712 писал(а):

Чтобы не терять время на поиски доказательства.

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

У меня такая аналогия возникла. Можно ли сказать, что SDG - это тоже своего рода идея применить матлогику, только не к алгебре (как в случае с той теоремой Джекобсона), а к дифференциальной геометрии? То есть мы хотим исследовать обычную категорию гладких многообразий. Но мы поступим иначе. Мы выяснили, что существуют топосы, в которые можно хорошо (т.е. full and faithful) вложить эту нашу категорию гладких многообразий (ну и для которых выполняется аксиома Кока-Ловера, но это пока не важно). И дальше мы вместо того, чтобы работать с категорий гладких многообразий, будем работать с каким нибудь из таких топосов. Более того, я понимаю так, что можно синтетически работать с любым из этих топосов (особенно если не выходить за рамки дифференцирования). Это примерно как если мы хотим получать утверждения только на основе аксиом группы, то можно представлять в голове любую группу, какую нам хочется.

Ну и получается, что если работать во "внутреннем языке" топоса (или как это правильно назвать - "внутренняя теория"?), то мы будем получать результаты, которые перенесутся на нашу категорию гладких многообразий. Так то ведь, по идее, вложение (пусть даже и full and faithful) не обязано переносить все свойства, но оно должно переносить "категорные свойства". А вот для того, что бы гарантировать, что в наших рассуждениях будут фигурировать только "категорные свойства", для этого и надо работать в слабом внутреннем языке топоса. Т.е матлогика нужна для того, чтобы четко обрисовать круг средств, которые можно использовать "внутри" топоса и которые как бы "категорные", т.е. они перенесутся на категорию гладких многообразий. Так примерно?

[dgwuqtj]

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

Так примерно?

Я в SDG не разбираюсь, так что сказать не могу. Похоже на правду. Есть ли у этого практические применения — неясно.

[EminentVictorians]

dgwuqtj в сообщении #1699720 писал(а):

Похоже на правду.

Спасибо. Мне пока какие-то слишком технические детали не нужны, мне бы просто в самых общих чертах понять, о чем речь.

Я пока вижу так, что во всей этой ситуации работает старая добрая математическая идея расширения той области, в которой мы находимся. У нас есть $\mathbb R$, мы его расширили до $\mathbb C$, поделали что-то в $\mathbb C$, а затем проинтерпретировали результат с точки зрения $\mathbb R$. Почему мы можем так делать? Потому что у нас есть инъективный гомоморфизм $f : \mathbb R \to \mathbb C$. Этот гомоморфизм ведь тоже не переносит все свойства. Он переносит только алгебраические свойства. Строго говоря, мы должны писать как-то так: $f^{-1}((2 + 3i) + (5 - 3i)) = f^{-1}(7 + 0i) = f^{-1}(f(7)) = 7$. Но мы же так не пишем, мы пишем просто $(2 + 3i) + (5 - 3i) = (7 + 0i) = 7$, потому что чтобы работать с гомоморфизмом, не обязательно таскать саму функцию, можно просто научиться правильно злоупотреблять нотацией и все будет нормально.

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

[dgwuqtj]

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

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

Вы же можете отличить произвольное математическое рассуждение от доказательства, использующего только тождественные преобразования? Тут то же самое, надо просто следить, что не используется ничего лишнего: ни теории множеств (с конструкциями типа булеана), ни доказательств от противного. Просто нужно практиковаться.

Другое дело, что без точных формулировок или без «учителя» (в каком-то смысле) сложно понимать, сработает ли придуманное вами рассуждение в интуиционистской логике.