Оптимальный метаязык для описания математики

[Yuichi196883]

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

[dgwuqtj]

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

[epros]

Yuichi196883 в сообщении #1711274 писал(а):

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

Можно и без этого понятия. До Кантора, кстати, как-то обходились.

Yuichi196883 в сообщении #1711274 писал(а):

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

А чем именно язык "наивной" теории множеств отличается, например, от языка не наивной ZFC?

[EminentVictorians]

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

До Кантора, кстати, как-то обходились.

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

[Anton_Peplov]

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

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

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

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

До Кантора, кстати, как-то обходились.

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

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

[EminentVictorians]

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

Да, но до Кантора понятие множества всегда применялось к чему-то конкретному: множество чисел, множество точек...

А силлогизмы? Силлогизм про Сократа - это такое рассуждение: все $x$, принадлежащие $A$ (люди), так же принадлежат и $B$ (смертные). Данный s (Сократ) принадлежит $A$ (т.е. он человек). Значит $s \in B$ (Сократ смертен). Очевидно, древние понимали, что так рассуждать можно не только про людей, но и вообще. А "вообще" - это и есть абстрагирование от деталей. То есть они вполне нормально рассуждали о множествах, просто слово это не произносили, и современных значков типа $\cap\cup\subset$ не было. Хотя не удивлюсь, если у них какие-нибудь синонимы для множеств тоже были (собрания, совокупности, общности или что-то типа того). Но это надо оригиналы читать.

[epros]

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

То есть они вполне нормально рассуждали о множествах, просто слово это не произносили

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

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

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

А по-моему это, которое неизбежно вылезет, не множество, а предикат.

[EminentVictorians]

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

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

Я кстати ждал такое возражение. Вы думаете древние не связывали с предикатом "быть человеком" множество человеков?

[epros]

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

Я кстати ждал такое возражение. Вы думаете древние не связывали с предикатом "быть человеком" множество человеков?

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

[dgwuqtj]

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

Вы думаете древние не связывали с предикатом "быть человеком" множество человеков?

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

[epros]

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

Уже скорее класс человеков.

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

[dgwuqtj]

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

Например, как вопрос о принадлежности к человекам должен разрешаться на недельном зародыше?

Так же, как и истинность предиката на этом зародыше. Конечно, классы — это уже не чисто логическое понятие, но всё же лучше, чем множества.

[epros]

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

Так же, как и истинность предиката на этом зародыше.

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

[EminentVictorians]

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

А с какой стати должны были связывать именно со множеством?

Потому что это психологически естественно. Я 2 года не мог понять, что такое предикат, а потом понял минут за 5, когда тему множеств освоил.

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

Вот возьмём всё тот же пресловутый пример из логики второго порядка: "Некоторые критики восхищаются только друг другом".

Мы это уже как-то обсуждали, но я так и не понял, что тут такого особенного в этих критиках. Вот цитата:

Цитата:

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

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

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

[epros]

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

Потому что это психологически естественно. Я 2 года не мог понять, что такое предикат, а потом понял минут за 5, когда тему множеств освоил.

Очень странно ссылаться на какую-то "психологическую естественность", ибо это сугубо индивидуальная и неуловимая штука. Например, я понимаю за 5 минут , что такое "множество", только после того, как мне продемонстрируют предикат $a \in A$, но никак не раньше.

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

Я не чувствую какого-то дискомфорта по отношению к этому предложению

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