Логика первого и второго порядка

[EminentVictorians]

mihaild в сообщении #1558757 писал(а):

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

Вроде как не совсем. Там была стандартная тема, когда новички ищут самое дно в строгости математики и ожидают найти его в матлогике. Я тоже этим болел когда-то, но оно само прошло. Вы наверное помните, были темы, типа, что такое $1$, что такое $1 + 1 = 2$ и тому подобное. Это все немного перпендикулярно моему вопросу.

Меня интересует, как соотносятся формальные результаты о $ZFC$ (всякие результаты независимости типа континуум-гипотезы, мультипликативности свойства Суслина и т.п.) и математика. Вот Вы в той теме пишете

mihaild в сообщении #1555960 писал(а):

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

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

Более того, sowa же говорит и про ограничения логики первого порядка.

sowa писал(а):

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

Если логика первого порядка, как образно написал Nemiroff, рассыпает по дороге часть аксиом, с чего мы тогда так уверены, что результаты типа независимости континуум-гипотезы сколь нибудь адекватны по отношению к математике?

[Mikhail_K]

mihaild в сообщении #1558599 писал(а):

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

Мне определённо не нравится это утверждение.
Наверное, здесь имеется в виду, что аксиома индукции для натуральных чисел содержит эту самую квантификацию по предикатам.
Но это если пытаться строить теорию натуральных чисел как самостоятельную теорию, без обращения к теории множеств. Но кому вообще нужна такая теория, не позволяющая использовать аппарат теории множеств?
Более естественно строить теорию натуральных чисел в рамках ZFC. То есть определить множество натуральных чисел как любое множество, удовлетворяющее аксиомам Пеано. При этом, в аксиоме индукции уже не нужна квантификация по предикатам, потому что используется квантификация по подмножествам, а это обычные объекты в ZFC. И тогда, где может дальше вообще понадобиться логика второго порядка?
Как я понимаю, аксиоматика Пеано, если её рассматривать в рамках ZFC, а не как самостоятельную аксиоматическую систему - категорична и безо всякой логики второго порядка.

-- 28.06.2022, 23:22 --

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

Более того, sowa же говорит и про ограничения логики первого порядка.

А ссылку можно?

[EminentVictorians]

Mikhail_K, ссылку первоначально привел пианист. Вот его сообщение

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

(Оффтоп)

mihaild в сообщении #1556066 писал(а):

А можно пример?

sowa@lj
Была большая дискуссия в рамках обсуждения его поста про алгебры Калкина https://sowa.livejournal.com/92839.html
Началась с замечания https://sowa.livejournal.com/92839.html?thread=3489959
Заранее предупреждаю: много букв.

У меня какая-то ерунда с интернетом, ссылка иногда не открывается. Но та цитата sowa из моего сообщения точная.

[mihaild]

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

Там была стандартная тема, когда новички ищут самое дно в строгости математики и ожидают найти его в матлогике

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

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

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

Это в точности отрицание того, что говорит sowa. Он говорит, что на практике наверняка обнаружится, что пользуемся какими-то дополнительными средствами, не замечая этого.

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

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

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

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

Как я понимаю, аксиоматика Пеано, если её рассматривать в рамках ZFC, а не как самостоятельную аксиоматическую систему - категорична и безо всякой логики второго порядка.

Да, но сама ZFC не категорична.

[EminentVictorians]

mihaild в сообщении #1558766 писал(а):

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

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

mihaild в сообщении #1558766 писал(а):

Это в точности отрицание того, что говорит sowa. Он говорит, что на практике наверняка обнаружится, что пользуемся какими-то дополнительными средствами, не замечая этого.

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

Я постараюсь объяснить, что я имею в виду.

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

Похожая ситуация с ZFC. Есть вещественные числа. Есть утверждение из континуум гипотезы. Очевидно, что оно либо истинно, либо ложно. Но в ZFC оно недоказуемо. Опять же, на мой взгляд сей факт ничего не говорит о вещественных числах. А говорит лишь о бедности ZFC.

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

-- 29.06.2022, 13:23 --

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

множество вещественных чисел одно единственное, хорошо определенное и конкретное.

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

[kernel1983]

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

[mihaild]

EminentVictorians, а то, что из аксиом группы (существование единицы, обратного и ассоциативности) не выводится коммутативность, вас не смущает? Если нет - то почему такая дискриминация, что "группы" бывают разные а "натуральные числа" или "системы множеств" - нет?

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

Если вообще не вся логика первого порядка или даже не весь формальный метод.

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

[Nemiroff]

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

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

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

[EminentVictorians]

mihaild в сообщении #1558853 писал(а):

а то, что из аксиом группы (существование единицы, обратного и ассоциативности) не выводится коммутативность, вас не смущает?

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

mihaild в сообщении #1558853 писал(а):

"натуральные числа" или "системы множеств" - нет?

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

mihaild в сообщении #1558853 писал(а):

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

А о каких формальных системах идет речь в теореме Геделя? Явно же не о любых.

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

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

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

[Nemiroff]

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

Явно же не о любых.

О любых не слишком простых, фактически.

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

Гораздо более надежный, чем все это мероприятие с формальными системами.

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

Это разумно и правильно. Более того, это единственный способ продвинуться в математике (потому что даже для определения формальной системы вам нужны натуральные числа -- упс).

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

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

С континуум-гипотезой все так же, но гораздо хуже -- подмножеств у вещественных чисел много. Конечно, если вы будете перебирать подмножества, которые вы можете перебирать -- они все не более, чем счётные или континуальные. Но подмножеств слишком много -- и подавляющее большинство из них нельзя перебрать, пощупать, посмотреть или понять. При этом у теории множеств нет стандартной модели. А значит, мы не знаем, как ведут себя подмножества "на самом деле". Есть какое-то понимание -- если два множества объединить, то будет множество, например. Но это не помогает, более того, не помогает вообще ничего из того, что мы называем ZFC. Потому что нет интуитивно понятного и платонически истинного описания того, как ведут себя множества.

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

На "земных" множествах они обязаны давать одинаковые результаты.

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

-- Чт июн 30, 2022 00:34:52 --

Я вот ещё что скажу, вы в теме ранее задавали вопрос такого вида

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

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

Это всё было к ненужности формального метода -- типа "обычная логика" и так всё делает.

Тем не менее, в ещё одной теме вы делаете вот такое

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

Получилась самая обычная цепочка вложенных подпространств $\operatorname {lin} v_1 \subset ... \subset \operatorname {lin} v_n \subset ...$. Почему не гарантируется получить бесконечную цепочку, если я ее прямо предъявил?

И я (и далеко не только я) вам даже ответил

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

Вы не предъявляете бесконечную цепочку. Вы говорите, что для любого натурального числа $n$ существует цепочка длины $n$.

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

[EminentVictorians]

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

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

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

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

Это всё ещё не значит, что эту теорему вы могли бы доказать с помощью наивного понятия о натуральных числах -- наивного понятия не хватает, потому что натуральных чисел много.

А если в моем наивном представлении о натуральных числах уже заложено, что они вложены в действительные числа. Иными словами, Вы ставите знак равенства между "наивные представления о натуральных числах" = аксиомы Пеано. А по мне так нету здесь равенства.

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

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

По поводу подмножеств у меня такое мнение: если наше множество $X$ "хорошо определенное" ("земное", "имеет степень определенности 1", "хорошее" или еще как-нибудь названное с максимально положительной коннотацией), то множество $2^X$ его подмножеств, на мой взгляд, имеет такую же степень "хорошести". Для меня это не математический факт, а презумпция (такая же, как что натуральные числа единственные в своем роде). Если эта презумпция не будет выполняться в некоторой формальной системе, то -- опять же -- вина не презумпции, а формальной системы. Множество вещественных чисел у меня в категории "степень определенности = 1", так что и его подмножества тоже. Это вполне нормально соотносится с тем, что все подмножества вещественных чисел мы не сможем "обозреть". Раз уж на то пошло, у нас весь алфавит естественного языка + все возможные символы математики -- конечно множество (ну пусть даже будь оно счетное, все равно не поможет). А значит все наши математические построения и конструкции, которые мы в состоянии обозреть -- не более чем счетное множество. А на самом деле вообще конечное, людей то ведь конечное число и время жизни ограничено. Так что даже простейшее счетное множество мы не сможем обозреть полностью -- так что теперь, считать натуральные числа "плохо определенными"? Я думаю, что это уже совсем экстримизм пошел.

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

О любых не слишком простых, фактически.

А если в формальная система каждому множеству ставит его "степень определенности" из $[0, 1]$. В рамках фантазий, там могут быть аксиомы типа:
-степень определенности объединения множеств = инфимум степеней определенности составляющих множеств
-степень определенности множества равна степени определенности его булеана
...

А если вместо непрерывного отрезка $[0, 1]$ в качестве степени определенности будет какой-нибудь комбинаторно-алгебраический инвариант? Будет ли теорема Геделя распространяться на такие формальные системы? Вопрос скорее риторический, показывающий, что формальные системы могут быть абсолютно не похожими на те, к которым мы привыкли.

[пианист]

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

формальные системы могут быть абсолютно не похожими на те, к которым мы привыкли

На сегодняшний день ничего, кроме МТ, не придумали.

[Someone]

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

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

Математический анализ имеет нестандартный вариант, в котором есть бесконечно малые и бесконечно большие действительные числа. Причём, в нём верны в точности те же утверждения о стандартных действительных числах, что и в стандартном анализе. Натуральные числа в нём тоже нестандартные (есть бесконечно большие натуральные числа).

[mihaild]

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

Множество вещественных чисел у меня в категории "степень определенности = 1", так что и его подмножества тоже.

И у множества Витали тоже? Или у более чем континуального семейства попарно непересекающихся непустых подмножеств $\mathbb R$?

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

Так что даже простейшее счетное множество мы не сможем обозреть полностью -- так что теперь, считать натуральные числа "плохо определенными"?

По-моему - хорошая идея.

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

Будет ли теорема Геделя распространяться на такие формальные системы?

Теорема Гёделя распространяется на все системы, в которые можно запихнуть арифметику Робинсона. Т.е. если есть функция, которая из арифметических утверждений делает формулы вашей системы, причем из доказуемых в $Q$ делает выводимые в вашей системе (а еще ваша система не выводит противоречий и её выводы можно вычислимо проверять), то ваша система неполна.

[EminentVictorians]

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

Математический анализ имеет нестандартный вариант, в котором есть бесконечно малые и бесконечно большие действительные числа. Причём, в нём верны в точности те же утверждения о стандартных действительных числах, что и в стандартном анализе. Натуральные числа в нём тоже нестандартные (есть бесконечно большие натуральные числа).

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

mihaild в сообщении #1558956 писал(а):

И у множества Витали тоже? Или у более чем континуального семейства попарно непересекающихся непустых подмножеств $\mathbb R$?

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