Являются ли множества и символы строительными блоками математики?

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

Итак, давайте посмотрим, что мы можем построить нециклически и в каком порядке.

Естественный язык

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

Натуральные числа и строки

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

Спецификация программы

Выберите любой разумный язык программирования. Программа -- это строка , задающая последовательность действий , каждое из которых -- либо базовый шаг манипулирования строкой , либо условный переход . На основном этапе манипуляции со строками мы можем обращаться к любым строкам по имени . Изначально все строки с именами в программе пусты, кроме строки с именем$input$, который содержит входные данные для программы. Условный переход позволяет нам проверить, верно ли какое-то базовое условие (скажем, число не равно нулю), и перейти к другому шагу программы, если оно верно. Мы можем легко реализовать$k$-кратное повторение последовательности действий с использованием счетчика натуральных чисел, установленного на$k$перед этой последовательностью и уменьшается на$1$после последовательности и переход к началу последовательности до тех пор, пока$k$отличен от нуля. Выполнение программы на входе просто следует за программой (с$input$содержащий ввод в начале) до тех пор, пока мы не достигнем конца, после чего программа, как говорят, останавливается , и все, что хранится в строке с именем$output$будет считаться результатом работы программы. (Возможно, что программа никогда не достигает конца, и в этом случае она не останавливается. Обратите внимание, что в этот момент мы не хотим (пока) утверждать, что каждое выполнение программы либо останавливается, либо не останавливается. В особых случаях мы могли бы заметить, что он не остановится, но если мы не можем сказать, то пока просто скажем: «Мы не знаем».)

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

Формальная спецификация системы

Теперь мы можем использовать программы для представления формальной системы. В частности, полезная формальная система$T$есть язык $L$, представляющий собой примитивно-рекурсивный набор строк, который здесь называется предложениями над$T$, некоторые из которых считаются доказуемыми$T$. Часто$T$поставляется с дедуктивной системой , которая состоит из правил , определяющих, какие предложения вы можете доказать на основе уже доказанных предложений. Мы могли бы выразить каждое правило в форме "$φ_1,φ_2,...,φ_k \vdash ψ$", в котором говорится, что если вы уже доказали$φ_1,φ_2,...,φ_k$то вы можете доказать$ψ$. Правил может быть даже бесконечно много, но главная особенность полезного$T$заключается в том, что существует одна-единственная примитивно-рекурсивная программа, которую можно использовать для проверки одного дедуктивного шага , а именно единственного применения любого из правил. Конкретно для такого$T$есть примитивная рекурсивная программа$P$который принимает строку$x$если$x$кодирует последовательность предложений$φ_1,φ_2,...,φ_k,ψ$такой, что$φ_1,φ_2,...,φ_k \vdash ψ$.

Поскольку все полезные формальные системы имеют такую ​​программу, мы можем проверить чье-либо утверждение, что предложение$φ$доказуемо более$T$, если они обеспечивают всю последовательность дедуктивных шагов, что является одной из возможных форм доказательства .

До сих пор мы видели, что все, что нам нужно с философской точки зрения, — это способность выполнять (конечное число) строковых манипуляций, и мы можем добраться до точки, где мы можем проверять доказательства над любой полезной формальной системой. Сюда входят системы первого порядка PA и ZFC. В этом смысле мы, очевидно, можем делать то же, что и ZFC, но вопрос о том, имеют ли наши манипуляции со строками какое-либо значение , не может быть решен без более строгой онтологической приверженности.

Теоремы Гёделя о неполноте

На этом этапе мы уже можем «получить» теоремы Гёделя о неполноте как во внешней, так и во внутренней форме. В обоих случаях нам дана полезная формальная система$T$это также может доказать все, что может доказать PA (при соответствующем переводе). Учитывая любое предложение$P$над$T$, мы можем построить предложение$Prov_T(P)$над$T$что хотел сказать "$P$доказуемо более$T$". Тогда мы позволим$Con(T) = ¬Prov_T(\bot)$. Чтобы «получить» внешнюю форму (если$T$доказывает$Con(T)$затем$T$доказывает$\bot$), мы можем явно написать программу, которая получает на вход любое доказательство$Con(T)$над$T$производит в качестве вывода доказательство$\bot$над$T$. И чтобы «получить» внутреннюю форму, мы можем явно записать доказательство над$T$приговора»$Con(T) \rightarrow \neg Prov_T(Con(T))$". (См . это для более точных формулировок такого рода результатов.)

Загвоздка в том, что предложение "$Prov_T(P)$совершенно бессмысленно, если мы не имеем представления об интерпретации предложения в$T$, чего мы до сих пор полностью избегали, так что все чисто синтаксически. Мы перейдем к основной форме значения в следующем разделе.

Базовая теория моделей

Допустим, мы хотим иметь возможность утверждать, что любая данная программа на данном входе либо останавливается, либо не останавливается. Мы можем сделать это, если примем LEM (закон исключенного третьего) . Теперь мы можем выразить основные свойства о$T$, например, является ли оно непротиворечивым (не доказывает как предложение, так и его отрицание), и является ли оно полным (всегда доказывает либо предложение, либо его отрицание). Это придает смысл теоремам Гёделя о неполноте. Из внешней формы, если$T$действительно последователен, то он не может доказать$Con(T)$Несмотря на то$Con(T)$соответствует через перевод утверждению о натуральных числах, которое истинно тогда и только тогда, когда$T$согласуется.

Но если мы в дальнейшем хотим иметь возможность говорить о наборе строк, принимаемых программой (а не только о примитивно-рекурсивных), мы, по сути, просим более сильную аксиому понимания множества, в данном случае$Σ^0_1$-понимание (не только$Δ^0_0$-понимание). Область реверсивной математики включает изучение различий между такими слабыми теоретико-множественными аксиомами, и в связанной статье Википедии упоминаются эти и другие понятия, о которых я буду говорить позже, но гораздо лучшей ссылкой является этот краткий документ Генри Тауснера . С$Σ^0_1$-понимание можно говорить о совокупности всех предложений, доказуемых на протяжении$T$, тогда как раньше мы могли говорить о каком-то одном таком предложении, а не о всей совокупности как об одном объекте.

Теперь для доказательства теоремы о компактности даже для (классической) логики высказываний нам нужно еще больше, а именно WKL (слабая лемма Кенига) . А поскольку теорема о компактности является тривиальным следствием теоремы о полноте (скажем, для естественной дедукции), WKL также требуется для доказательства теоремы о полноте. То же самое относится и к логике первого порядка.

Прыжки Тьюринга

Теперь с философской точки зрения не имеет смысла иметь только$Σ^0_1$-понимание. В конце концов, это в каком-то смысле эквивалентно наличию оракула для решения проблемы остановки (для обычных программ), которая представляет собой первый прыжок Тьюринга . Проблема остановки неразрешима , а это означает, что нет программы, которая всегда останавливалась бы при любом вводе.$(P,x)$и принимает если$P$останавливается на$x$. Позволяя$Σ^0_1$-понимание, мы в некотором смысле получаем доступ к такому оракулу. Но тогда, если мы рассмотрим расширенные программы, которым разрешено использовать первый прыжок Тьюринга (он получит ответ за один шаг), проблема остановки для этих программ снова будет неразрешима ни одной из них, но мы можем представить себе оракула. для этого тоже, что является вторым прыжком Тьюринга. Поскольку мы разрешили первое, нет действительно веской причины запрещать второе. И так далее.

Конечным результатом является то, что мы могли бы также принять полное арифметическое понимание (мы можем построить любой набор строк или натуральных чисел, определяемый формулой, где все кванторы находятся над натуральными числами или строками). И с металогической точки зрения мы также должны иметь полную схему индукции второго порядка , потому что мы уже предполагаем, что мы принимали только предположения, которые справедливы для стандартных натуральных чисел, а именно те, которые могут быть выражены в форме$1+1+\cdots+1$".

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

Теория высших моделей

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

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

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

Множества в теориях множеств

Наконец, ваш вопрос может быть основан на распространенном заблуждении, что в ZFC у вас есть понятие «набор». Не совсем. ZFC - это просто еще одна формальная система, в которой нет символа, обозначающего «набор». Просто аксиомы ZFC были составлены таким образом, что кажется разумным предположить, что они верны для некоторого расплывчатого понятия «множества» в естественном языке. Внутри ZFC каждый квантификатор распространяется на всю область, поэтому нельзя говорить о множествах, как будто существуют другие виды объектов. Если мы используем метасистему, не имеющую наборов, то модель ZFC может вообще не иметь никаких «наборов», что бы ни означал «набор»!

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

В нетрадиционной теории множеств NFU есть и множества, и urelements (экстенсиональность применима только к множествам), поэтому здесь можно говорить о множествах. Но NFU в любом случае не очень удобная система.

И на этом мой ответ также остановится.