Неразрешимость логики первого порядка

Работы Гильберта и Бернайса — важный этап в истории формализации логики первого порядка. Одним из главных достижений Гильберта было создание аксиоматического метода доказательства теорем. Гильберт сформулировал конечный набор аксиом, на основе которых можно было доказать любое утверждение в формальной системе. Он также предложил формальный язык, состоящий из констант, переменных, функций и предикатов, и определил правила для вывода логических следствий на его основе. Бернайс своей работой в области оснований математики укрепил результаты Гильберта, показав, что современная математика может быть построена на основе одной аксиомы множества и утверждения о существовании бесконечных множеств. Однако, наряду с другими аксиоматическими системами, аксиомы Бернайса возникли некоторые логические и теоретические проблемы. Еще одним важным вкладом Гильберта была его теория множеств, которую он изложил в своей книге «Основания геометрии» в 1899 году. Он доказал некоторые фундаментальные теоремы о множествах и привел формальные определения, включая теорию отношений и операций с множествами. Важной работой Бернайса является его теория множеств, опубликованная в 1937 году в его книге «Основания математики» [12]. Он предложил формализованное определение множества и установил связь между логическими законами и свойствами множеств. Бернайс также доказал, что многие аксиомы теории множеств, предложенной до него, могут привести к парадоксам. Таким образом, работы Гильберта и Бернайса являются важными этапами в развитии формализации логики первого порядка, которые имели огромное значение для математики, логики и философии. Они подняли множество фундаментальных вопросов и проблем, которые до сих пор изучаются и анализируются в научных кругах.

2. ФОРМАЛЬНЫЕ СИСТЕМЫ И ЛОГИКА ПЕРВОГО ПОРЯДКА: ОСНОВЫ И ПРИНЦИПЫ

2.1. Концепция формальной системы

Формальная система (или формальная теория) представляет собой результат тщательной формализации теории, которая предусматривает полное отделение от смысла слов используемого языка [13]. При этом все критерии, определяющие использование этих слов в теории, явно выражены через аксиомы и правила, позволяющие выводить одно предложение из другого. Формальная теория считается определенной, когда:
• Установлено конечное или счетное множество произвольных символов (конечные последовательности символов определяются как выражения теории);
• Определено подмножество выражений, известное как формулы;
• Выделено подмножество формул, известное как аксиомы;
• Установлено конечное количество отношений между формулами, называемых правилами вывода.
В большинстве случаев есть эффективная процедура, позволяющая определить, является ли данное выражение формулой. Обычно множество формул определяется индуктивным определением. В общем случае это множество бесконечно. Множество символов и множество формул вместе определяют язык или сигнатуру формальной теории. Обычно можно эффективно определить, является ли данная формула аксиомой; в этом случае теория называется эффективно аксиоматизированной или аксиоматической. Множество аксиом может быть конечным или бесконечным. Если множество аксиом бесконечно, оно обычно определяется с помощью конечного числа схем аксиом и правил порождения конкретных аксиом из этих схем. Аксиомы обычно классифицируются на два типа: логические аксиомы (общие для всего класса формальных теорий) и нелогические или собственные аксиомы (определяющие специфику и содержание конкретной теории). Для каждого правила вывода R и каждой формулы A можно эффективно определить, находится ли выбранный набор формул в отношении R с формулой A. Если да, то формула A называется прямым следствием этих формул по правилу R. Выводом называется любая последовательность формул такая, что каждая формула в последовательности либо является аксиомой, либо является прямым следствием некоторых предыдущих формул по одному из правил вывода.
Если для формулы можно привести цепочку выводов, которая завершается данной формулой, то такая формула определяется как теорема. Если для определенной теории возможно разработать эффективный алгоритм, который может определить, можно ли для данной формулы привести вывод, то такая теория считается разрешимой. В противоположном случае теория оценивается как неразрешимая. Теория, в которой не каждая формула является теоремой, определяется как абсолютно непротиворечивая.
Определенной дедуктивной теории приписываются следующие характеристики:
• Определены алфавит и правила создания выражений на его основе;
• Установлены правила создания формул, которые являются правильно сформулированными выражениями;
• Из общего набора формул выделяется подмножество теорем, то есть формул, для которых можно привести доказательства.
Дедуктивные теории имеют следующие свойства:
1. Противоречивость: Если все формулы в теории являются теоремами или "истинными высказываниями", теория считается противоречивой. В обратном случае она определяется как непротиворечивая. Определение противоречивости теории - одна из ключевых и порой сложных задач в области формальной логики. Противоречивая теория, как правило, теряет свою практическую и теоретическую значимость.
2. Полнота: Теория считается полной, если для каждой формулы можно вывести либо саму формулу, либо ее отрицание. Если это не так, и теория содержит утверждения, которые невозможно ни доказать, ни опровергнуть в рамках самой теории, она определяется как неполная.
3. Независимость аксиом: Если отдельную аксиому невозможно вывести из остальных аксиом, она считается независимой. В этом случае, если бы такую аксиому удалить, это бы не повлияло на теорию, так как она, по сути, избыточна. Если каждая аксиома в теории независима, система аксиом теории определяется как независимая.
4. Разрешимость: Теория считается разрешимой, если в ней понятие теоремы является эффективным. Это означает, что существует эффективный процесс (алгоритм), который может за конечное число шагов определить, является ли данная формула теоремой.

2.2. Основные понятия логики первого порядка

Логика первого порядка, также известная как исчисление предикатов, представляет собой формальное исчисление - совокупность абстрактных элементов, не связанных с внешним миром, где установлены правила обработки набора символов в строго синтаксическом интерпретации, исключая семантическое содержание [14]. Язык первопорядковой логики разрабатывается на базе сигнатуры, которая включает следующие символы:
1. Логические символы – символы логических операций ¬, ∨, ∧, ↔, →; – символы операций кванторов ∀, ∃; – служебные символы, такие как скобки и запятые.
2. Нелогические символы – набор символов предикатов, связанных с арностью, т.е. количество возможных аргументов P(n), Q(m), …, P1(n), P2(n); – символы пропозициональных переменных X, Y, Z, …, X1, X2, … (они могут быть рассмотрены как нуль-арные предикатные символы); – символы переменных объектов x, y, z, …, x1, x2,…; – символы констант объектов a, b, c, …, a1, a2, … n-арным предикатом P (x1, x2,…, xn) считается функция P: M1xM2x…xMn → {1,0}, определенная на наборах длиной n элементов какого-либо множества M= M1xM2x…xMn и возвращающая значения в области {1,0}. Множество M называется областью объекта предиката, его элементы - константами объекта. Отрицание предиката P(x1, x2,…, xn), определенного на множестве M1xM2x…xMn, называется предикат ¬P(x1, x2,…, xn), установленный на том же множестве, который на наборе (a1, a2,…, an) ∈ M1xM2x…xMn