Природа натуральных чисел

[Padawan]

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

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

Как именно?

(Оффтоп)

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

[mihaild]

Padawan в сообщении #1594151 писал(а):

Как именно?

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

-- 16.05.2023, 20:00 --

Padawan в сообщении #1594151 писал(а):

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

А в чём дикость? Всю историю про нумерацию тоже нужно вести в какой-то теории.

[Padawan]

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

формула в ПНФ

Что такое ПНФ?

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

все истинные типаформулы без кванторов (это тоже определяется индукцией по построению уже логической формулы)

Ок, давайте сначала определим множество всех истинных типаформул без кванторов.

[mihaild]

Padawan в сообщении #1594156 писал(а):

Что такое ПНФ?

Предваренная нормальная форма (все кванторы в начале, формула в КНФ).

Padawan в сообщении #1594156 писал(а):

Ок, давайте сначала определим множество всех истинных типаформул без кванторов.

Опять же индуктивно.
Типатермом назовем пару (терм, функция из переменных в натуральные числа (оценка)). Значение типатерма определяется индуктивно: если терм - переменная, то значение типатерма - значение этой функции на этой переменной. Если типатерм - сумма двух типатермов, то значение - это сумма (в смысле определенного на нашей модели сложения) значений этих типатермов, и т.д.
Для типаформул: если формула в типаформуле атомарная, то она имеет вид "типатерм=типатерм" (вроде можно обойтись только равенством для предикатных символов), и она оценивается истиной если типатермы оцениваются одинаковыми значениями.
Ну и дальше отрицание-конъюнкция-дизъюнкция понятно как.

[Padawan]

А как мы зададим функцию на переменных и далее будем с ней работать? Напишите, пожалуйста, определение множества истинных типаформул вида типатерм=типатерм.

[mihaild]

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

Оценка типатермов - это функция $g$ из типатермов в натуральные числа, такая что $g(\langle x, f\rangle) = f(x)$, $g(\langle t_1 + t_2, f\rangle) = g(\langle t_1, f\rangle) +_N g(\langle t_2, f\rangle)$ и аналогично для $\cdot$. Такая функция существует и единственна.
Типаформула вида $\langle t_1 = t_2, f\rangle$ истинна, если $g(\langle t_1, f\rangle) =_N g(\langle t_2, f\rangle)$.
Здесь под $+, \cdot, =$ понимаются символы алфавита, а под $+_N, \cdot_N, =_N$ - функции и предикаты на натуральных числах.

[Padawan]

Мне непонятно, как это все записать внутри ZF. Как мы функцию на переменных опишем? Что это за объект?

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

[mihaild]

Мы заводим какое-нибудь отдельное множество $A'$, которое будет из себя изображать символы, плюс в нём выделим три элемента, которые будут из себя изображать символы $+, \cdot, =$. $A'$ без этих трех элементов обозначим $A$, это множество переменных.
Термы и формулы - это функции из начального отрезка натурального ряда в $A'$ (с нужными для синтаксической корректности свойствами).
Оценка конечного множества переменных - это функция из конечного подмножества $A'$ в натуральные числа.

ZF позволяет рассуждать об интерпретациях формул.

[epros]

Извиняюсь за поднятие этой подзаглохшей темы.

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

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

Я утверждаю, что все Ваши рассуждения в логике второго порядка формализуются в рамках ZF.

Я подумаю над примером, но это, очевидно, непростая задача.

А давайте я Вам помогу с этим. Вот здесь приведён классический пример простого утверждения естественного языка, невыразимого в логике первого порядка: "Some critics admire only one another" ("Некоторые критики восхищаются только друг другом"). Там же приведена его формализация в языке логики второго порядка и доказательство его невыразимости в логике первого порядка. Кратко: суть в том, что при замене предиката "восхищается" на простую формулу арифметики натуральных чисел получается утверждение, из которого следует существование нестандартных чисел.

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

[EminentVictorians]

epros, я был слегка не в себе, когда думал, что рассуждение с нигде не плотным множеством не формализуется в ZFC. Конечно же оно формализуется - переменные предметные, все в порядке. Но это ладно, бывает.

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

"Некоторые критики восхищаются только друг другом"

Я на своей человеческой логике расшифровываю это предложение следующим образом. Пусть $P$ - множество всех людей на планете Земля. $K \subset P$ - множество критиков. Утверждается, что существует такое подмножество $S \subset K$ критиков, что каждый элемент из $S$ восхищается всеми элементами из $S$ и только ими (в том числе и, например, собой). Я не чувствую какого-то дискомфорта по отношению к этому предложению.

Вы можете сказать, что "множество людей планеты Земля" не формализуется в ZFC и что это не математический объект. Тут я не знаю, что ответить. Я-то как бы живу в наивной теории множеств, поэтому для меня это нормальное множество.

-- 24.05.2023, 15:35 --

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

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

Хм... мне казалось, что это просто артефакт естественного языка, что мы явно не проговариваем про наш "универсум" - людей на Земле. Ну т.е. мне казалось, что "люди на Земле" - часть утверждения. Я не имел в виду "всех критиков" и тоже не знаю, что это такое. Я вообще не помню, чтобы когда-либо использовал просто "$\forall x$", а не "$\forall x \in X$" или "$\forall x (x \in X \to ...)$". В общем, я всегда использую квантор $\forall$ вместе с тем множеством, откуда мы берем эти все объекты.

[epros]

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

Я на своей человеческой логике расшифровываю это предложение следующим образом. Пусть $P$ - множество всех людей на планете Земля. $K \subset P$ - множество критиков.

Увы, никто не сказал, что критики - с планеты Земля или хотя бы из нашей Вселенной, а не из параллельных. Так что интерпретируйте как хотите.

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

Хм... мне казалось, что это просто артефакт естественного языка, что мы явно не проговариваем про наш "универсум" - людей на Земле. Ну т.е. мне казалось, что "люди на Земле" - часть утверждения. Я не имел в виду "всех критиков" и тоже не знаю, что это такое. Я вообще не помню, чтобы когда-либо использовал просто "$\forall x$", а не "$\forall x \in X$" или "$\forall x (x \in X \to ...)$". В общем, я всегда использую квантор $\forall$ вместе с тем множеством, откуда мы берем эти все объекты.

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

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

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

[zykov]

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

Дело не в том, какие бывают критики.

Тут уже буйство фантазии.
Фраза "Some critics admire only one another" всё же была про конечное множество людей-критиков.

[Anton_Peplov]

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

[epros]

zykov в сообщении #1595121 писал(а):

Фраза "Some critics admire only one another" всё же была про конечное множество людей-критиков.

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

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

[EminentVictorians]

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

Увы, никто не сказал, что критики - с планеты Земля или хотя бы из нашей Вселенной, а не из параллельных. Так что интерпретируйте как хотите.

Т.е. есть какое-то никак толком не определенное множество критиков, о котором что-то утверждается. Я не встречал в математике утверждений о никак не определенном множестве. Но если уж на то пошло:

Пусть $K$ - множество всех критиков. Утверждается, что существует такое подмножество $S \subset K$ критиков, что каждый элемент из $S$ восхищается всеми элементами из $S$ и только ими (в том числе и, например, собой). Утверждение истинно. Даже если ни одного такого критика нету, подойдет $\varnothing$. Если "существует" заменить на "существует непустое", то я не знаю, истинно это утверждение или нет (но знаю, что либо истинно, либо нет). Для этого мне нужно четкое определение кто такие критики и что значит восхищаться. Как видите, я все равно квантифицирую не в пустоту, а по какому-то множеству ($K$).

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

Anton_Peplov, отвечу чуть позже.