Нестандартные модели и основания математики

[Anton_Peplov]

kp9r4d в сообщении #1218347 писал(а):

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

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

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

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

Увы, в логике первого порядка эти проблемы неразрешимы из-за принципиальных ограничений языка. В логике второго порядка они, казалось бы, разрешимы. Но оказывается, что там - свои тараканы: логика второго порядка оччень странная штука... (вроде бы Willard Van Orman Quine
где-то даже сказал, что есть основания трактовать логику второго порядка как нечто, в строгом смысле слова "логикой" не являющееся).

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

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

arseniiv в сообщении #1218358 писал(а):

Мне кажется, нестандартные модели ZFC — это немного другое дело. Если мы всё нужное себе выразили в ZFC, то как на нас скажется их существование?

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

Господа, а давайте об этом в "Вокруг Цитатника"?

arseniiv в сообщении #1218368 писал(а):

Я бы вообще тему открыл (и всё туда сцитировал), но не знаю как назвать.

[kp9r4d]

Тогда уже и

kp9r4d в сообщении #1218366 писал(а):

Ну вот тем и мешает: ZFC ведь просто дедуктивная система, пользуясь ей мы можем сформулировать и доказать некоторое утверждение вида $\exists n\text{ Алгоритм A остановится на шаге}(n)$, гарантирует ли это, что есть конечная строка вида $1+1+1+...+1$ которая будет номером шага, на котором алгоритм $A$ остановится? Нет, не гарантирует.

[arseniiv]

Спасибо неленивому Anton_Peplov.

arseniiv в сообщении #1218381 писал(а):

А можно пример какого-нибудь конкретного утверждения?

[mihaild]

В самой $ZFC$, скорее всего, не получится (если получится - то это будет означать, что у $ZFC$ нет стандартной модели). А так - добавим к $ZFC$ акиому $\Box_{ZFC}\bot$ (ну или для любого другого алгоритма $A$, вопрос остановки которого не разрешим в $ZFC$, добавим аксиому "$A$ останавливается").

[Z1X]

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

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

Что за глупости? Понятие конечности можно выразить в теории множеств первого порядка. Если делать это без арифметики, то множество конечно тогда, когда не существует биекции между этим множеством и каким-либо собственным его подмножеством. Очевидно например, что пустое множество конечно.

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

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

Это уже какая-то полная чушь. Первое, что важно: что такое стандартная модель ZFC? Что это? Какие требования стандартности? И как понять: на самом деле может оказаться нестандартным? На самом деле — это как? Во-вторых, стандартная модель и вообще все модели задаются до изоморфизма. Модели разные, если они неизоморфны. Поэтому внутренняя структура каждого числа, арифметических операций и всей арифметики в целом не играет никакой роли. Множество конечно, если биекция отображает его на отрезок стандартного натурального ряда. Строение элементов этого отрезка нам безразлично. Отрезок задается простыми неравенствами.

arseniiv в сообщении #1218358 писал(а):

Мне кажется, нестандартные модели ZFC — это немного другое дело. Если мы всё нужное себе выразили в ZFC, то как на нас скажется их существование?

Что у вас называется нестандартной моделью ZFC?

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

В самой $ZFC$, скорее всего, не получится (если получится - то это будет означать, что у $ZFC$ нет стандартной модели).

А что у вас называется стандартной моделью ZFC?

[Someone]

Z1X в сообщении #1218447 писал(а):

Очевидно например, что пустое множество конечно.

Никаких сомнений. И множество $\{a,b,c,d,e\}$ тоже конечное. Тоже без сомнений.

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

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

Z1X в сообщении #1218447 писал(а):

множество конечно тогда, когда не существует биекции между этим множеством и каким-либо собственным его подмножеством

Ну да, это определение Дедекинда, насколько я помню. Беда в том, что оно не равносильно обычному (множество конечно, если оно равномощно натуральному числу; причём, имеются в виду не "натуральные числа вообще" (это непонятно, что такое), а конкретная модель натурального ряда, определяемая в теории множеств). Если в качестве теории множеств взять ZF (без аксиомы выбора), то возможны странные множества, в которых можно найти сколь угодно длинную конечную последовательность попарно различных элементов, но нельзя указать бесконечную последовательность. Они конечны по Дедекинду, но бесконечны в смысле обычного определения.

Z1X в сообщении #1218447 писал(а):

А что у вас называется стандартной моделью ZFC?

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

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

Вот возьмём арифметику Пеано, присоединим к её алфавиту новую константу $\hat n$ и добавим бесконечную последовательность аксиом $\hat n\neq 0$, $\hat n\neq 0'$, $\hat n\neq 0''$, $\hat n\neq 0'''$, … (штрих означает "следующее натуральное число", то есть, $0'=1$, $0''=1'=2$, …). Очевидно, если мы добавим только конечное число этих новых аксиом, то модель есть: новый символ можно отождествить с натуральным числом, которое не упоминается в добавленных аксиомах. По упомянутой теореме, модель существует и для всех указанных аксиом. Но в ней $\hat n$ есть натуральное число, не совпадающее ни с одним из натуральных чисел в первоначальной модели. Эта новая модель и будет нестандартной.

Поскольку модель арифметики Пеано вкладывается в ZFC как наименьшее индуктивное множество, мы теперь можем повторить эту конструкцию для ZFC.

[Anton_Peplov]

Z1X
Не приписывайте мне утверждения, которые я цитировал. Моя роль в этой теме сводится к тому, что я вытащил сообщения из Цитатника и создал для них отдельный топик.

[Z1X]

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

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

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

Я и теперь не понял, о чем речь. По частям:

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

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

Приведите в метаматематике определения конечности и бесконечности.

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

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

Если понятие нельзя выразить в теории первого порядка, то нельзя будет и для второго порядка. Ведь порядок всегда можно понизить, если задействовать теоретико-множественный синтаксис. Например, вы можете написать $\forall Q \forall x \ Q(x)$, а можете $\forall Q \forall x \ x\in Q$. Это одно и то же. Таким образом у вас конечность вообще не выразима.

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

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

Это чушь. Если утверждение нельзя формализовать, оно не научно. Модель арифметики первого порядка в некоторой метатеории $\mathcal M$ называется стандартной, если в этой же метатеории $\mathcal M$ существует модель арифметики второго порядка, и две модели изоморфны. Вернее, надо взять от модели второго порядка лишь числовую часть, и доказать изоморфность с первой, но это не важно. Это научно, и все это можно при необходимости аксиоматизировать. Если же стандартную модель ZFC нельзя определить так же строго, то все утверждения о ней заведомо бессмысленны.

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

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

А я не приписываю. Вы нечто процитировали, значит вы это написали в том сообщении, которое по ссылке. Здесь нет никакой ошибки.

[Mikhail_K]

(Z1X)

Z1X в сообщении #1218468 писал(а):

Это чушь.

Z1X, не нужно писать столь агрессивно. Насколько я знаю, Someone - специалист в той области, о которой идёт речь, и знает что говорит.

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

[kp9r4d]

Z1X в сообщении #1218468 писал(а):

Приведите в метаматематике определения конечности и бесконечности.

Определение зависит от метатеории, на которой метаматематику строят. Когда говорят про "теорему метаматематики" то имеют в виду то неформальное утверждение, что эту теорему можно сформулировать и доказать в любой достаточно мощной метатеории. Та же "теорема о полноте" в метаматематике построенной на $I\Sigma_1$, $PA$, $ZFC$ - это формально три разные конструкции, объединенные лишь общей идеей.

Z1X в сообщении #1218468 писал(а):

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

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

Z1X в сообщении #1218468 писал(а):

$\forall Q \forall x \ Q(x)$, а можете $\forall Q \forall x \ x\in Q$

хоть и есть некоторая "синтаксическая равноправность", но интерпретируются эти формулы по-разному.

(Оффтоп)

Z1X в сообщении #1218447 писал(а):

Что за глупости?

Z1X в сообщении #1218468 писал(а):

Это чушь. Если утверждение нельзя формализовать, оно не научно.

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

[Z1X]

kp9r4d в сообщении #1218482 писал(а):

Определение зависит от метатеории, на которой метаматематику строят. Когда говорят про "теорему метаматематики" то имеют в виду то неформальное утверждение, что эту теорему можно сформулировать и доказать в любой достаточно мощной метатеории.

Не обязательно доказывать, просто сформулируйте теорему

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

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

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

kp9r4d в сообщении #1218482 писал(а):

Это неправда. Логика первого порядка имеет гораздо меньше выразительной силы, чем логика второго порядка.

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

kp9r4d в сообщении #1218482 писал(а):

хоть и есть некоторая "синтаксическая равноправность", но интерпретируются эти формулы по-разному.

А какова вообще интерпретация формул второго порядка, если их не сводить к теоретико-множественным утверждениям? Можете определить? Я глубоко сомневаюсь, что такое автономное определение интерпретации вообще существует.

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

Z1X, не нужно писать столь агрессивно. Насколько я знаю, Someone - специалист в той области, о которой идёт речь, и знает что говорит.

kp9r4d в сообщении #1218482 писал(а):

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

Я обязательно сменю тон (и могу даже извиниться перед специалистом), если на мои замечания специалист даст аргументированный ответ (особенно про неаксиоматизируемость понятия стандартной модели). Но если чушь реально окажется чушью, а глупость - глупостью, то и менять ничего не надо. Подождем ответа.

[grizzly]

Z1X в сообщении #1218502 писал(а):

Подождем ответа.

Подождём. Я надеюсь, ответ будет адекватным.

[Someone]

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

Насколько я знаю, Someone - специалист в той области, о которой идёт речь, и знает что говорит.

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

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

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

В логике второго порядка я и сам ни бум-бум, а что касается метаматематики, то я с этим энакомился в основном по книге Расёвой и Сикорского "Математика метаматематики" и по книгам Клини "Математическая логика" и "Введение в метаматематику". Есть ещё "Справочная книга по математической логике" в четырёх томах. Это сборник статей разных авторов на основные темы, связанные с математической логикой и метаматематикой. Однако всё это далеко от "популярного".

Z1X в сообщении #1218468 писал(а):

Приведите в метаматематике определения конечности и бесконечности.

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

Z1X в сообщении #1218468 писал(а):

вы можете написать $\forall Q \forall x \ Q(x)$, а можете $\forall Q \forall x \ x\in Q$. Это одно и то же.

Нет. Второе требует, как минимум, двухсортной логики. И я не уверен, что это вполне равносильно логике второго порядка.

Z1X в сообщении #1218468 писал(а):

Если утверждение нельзя формализовать, оно не научно.

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

Z1X в сообщении #1218468 писал(а):

Если же стандартную модель ZFC нельзя определить так же строго, то все утверждения о ней заведомо бессмысленны.

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

(Z1X)

Z1X в сообщении #1218468 писал(а):

Вы нечто процитировали, значит вы это написали в том сообщении, которое по ссылке. Здесь нет никакой ошибки.

Ошибка есть. Вы должны были процитировать так, чтобы было видно, кто на самом деле это написал. Например, так:

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

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

Господа, а давайте об этом в "Вокруг Цитатника"?

arseniiv в сообщении #1218368 писал(а):

Я бы вообще тему открыл (и всё туда сцитировал), но не знаю как назвать.

[mihaild]

Z1X в сообщении #1218468 писал(а):

Если утверждение нельзя формализовать, оно не научно.

Под утверждением понимается же замкнутая формула? Можно определение "научной формулы"?

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

мы не можем полностью формализовать даже арифметику

А что это значит? Что у нас будут "интуитивно истинные", но недоказуемые утверждения?

[Someone]

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

А что это значит? Что у нас будут "интуитивно истинные", но недоказуемые утверждения?

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