Введение

Тип логической системы

Логика первого порядка, также известная как логика предикатов, количественная логика и исчисление предикатов первого порядка, представляет собой совокупность формальных систем, используемых в математике, философии, лингвистике и информатике. Логика первого порядка использует квантованные переменные над нелогическими объектами и позволяет использовать высказывания, содержащие переменные, так что вместо утверждений, таких как «Сократ — человек», можно иметь выражения вида «существует x, такое что x есть Сократ и x есть человек», где «существует» является квантором, а x — переменной. Это отличает её от пропозициональной логики, которая не использует кванторы или отношения; в этом смысле пропозициональная логика является основой логики первого порядка. Теория, относящаяся к какой-либо области, такая как теория множеств, теория групп или формальная теория арифметики, обычно представляет собой логику первого порядка вместе с заданной областью рассуждений (над которой варьируются квантованные переменные), конечным числом функций из этой области в себя, конечным числом предикатов, определенных в этой области, и множеством аксиом, которые считаются верными для них. Термин «теория» иногда понимается в более формальном смысле как просто множество высказываний в логике первого порядка. Термин «первый порядок» отличает логику первого порядка от логики высшего порядка, в которой предикаты имеют предикаты или функции в качестве аргументов, или в которой допускается квантификация над предикатами, функциями или обоими. В теориях первого порядка предикаты часто ассоциируются с множествами. В интерпретируемых теориях высшего порядка предикаты могут интерпретироваться как множества множеств. Существует множество дедуктивных систем для логики первого порядка, которые одновременно обоснованы, то есть все доказуемые утверждения истинны во всех моделях, и полны, то есть все утверждения, которые истинны во всех моделях, доказуемы. Хотя отношение логического следования является лишь полуразрешимым, достигнут значительный прогресс в автоматическом доказательстве теорем в логике первого порядка. Логика первого порядка также удовлетворяет ряду металогических теорем, которые делают её подходящей для анализа в теории доказательств, таких как теорема Лёвенгейма — Сколема и теорема о компактности. Логика первого порядка является стандартом для формализации математики в виде аксиом и изучается в основаниях математики. Арифметика Пеано и теория множеств Цермело — Френкеля являются аксиоматизациями теории чисел и теории множеств соответственно в логике первого порядка. Однако ни одна теория первого порядка не обладает достаточной силой для однозначного описания структуры с бесконечной областью, такой как натуральные числа или действительная прямая. Системы аксиом, которые полностью описывают эти две структуры, то есть категорические системы аксиом, могут быть получены в более сильных логиках, таких как логика второго порядка. Основы логики первого порядка были разработаны независимо Готлобом Фреге и Чарльзом Сандерсом Пирсом. Подробности об истории логики первого порядка и о том, как она стала доминирующей в формальной логике, можно найти в работе Хосе Феррейроса (2001).

Введение

В то время как логика высказываний имеет дело с простыми декларативными высказываниями, логика первого порядка дополнительно охватывает предикаты и квантификацию. Предикат принимает значение «истина» или «ложь» для конкретной сущности или сущностей в области рассуждений. Рассмотрим два предложения: «Сократ – философ» и «Платон – философ». В логике высказываний эти предложения сами по себе рассматриваются как объекты изучения и могут быть обозначены, например, переменными p и q. Они не рассматриваются как применение предиката, например, к каким-либо конкретным объектам в области рассуждений, а скорее как простое утверждение, которое либо истинно, либо ложно. Однако в логике первого порядка эти два предложения можно сформулировать как утверждения о том, что определенный индивид или нелогический объект обладает свойством. В этом примере оба предложения имеют общую форму для некоторого индивида x: в первом предложении значение переменной x – «Сократ», а во втором – «Платон». Благодаря возможности говорить о нелогических индивидах в дополнение к исходным логическим связкам, логика первого порядка включает в себя логику высказываний. Истинность формулы, такой как «x – философ», зависит от того, какой объект обозначается x, и от интерпретации предиката «является философом». Следовательно, «x – философ» само по себе не имеет определенного значения истинности – «истина» или «ложь» – и напоминает фрагмент предложения. Например, логический символ всегда представляет «и»; он никогда не интерпретируется как «или», которое представлено логическим символом. Однако нелогический символ предиката, такой как Phil(x), может быть интерпретирован как «x – философ», «x – человек по имени Филипп» или любой другой унарный предикат, в зависимости от конкретной интерпретации.

Свободные и связанные переменные

В формуле переменная может быть свободной или связанной (или и тем, и другим). Одно из формальных определений этого понятия принадлежит Квайну: сначала определяется понятие вхождения переменной, затем – является ли данное вхождение переменной свободным или связанным, и, наконец, – является ли переменный символ в целом свободным или связанным. Чтобы различать различные вхождения одного и того же символа x, каждое вхождение переменного символа x в формуле φ отождествляется с начальным фрагментом φ до точки, в которой это конкретное вхождение символа x появляется. С.297 Далее, вхождение x считается связанным, если оно находится в области действия хотя бы одного квантора или . Наконец, x считается связанной в φ, если все вхождения x в φ являются связанными. z встречается только свободно, а w не является ни свободным, ни связанным, поскольку не встречается в формуле. Множество свободных и связанных переменных формулы не обязано быть дизъюнктным: в формуле P(x) → ∀x Q(x) первое вхождение x, как аргумент P, является свободным, а второе, как аргумент Q, – связанным. Формула логики первого порядка, не содержащая свободных вхождений переменных, называется предложением логики первого порядка. Именно такие формулы будут иметь однозначно определенные значения истинности при интерпретации. Например, истинность формулы Phil(x) должна зависеть от того, что обозначает x. Но предложение ∃x Phil(x) будет либо истинным, либо ложным в данной интерпретации.

Пример: упорядоченные абелевы группы

В математике язык упорядоченных абелевых групп имеет один символ константы 0, один символ унарной функции −, один символ бинарной функции + и один символ бинарного отношения ≤. Тогда:
Выражения +(x, y) и +(x, +(y, −(z))) являются термами. Они обычно записываются как x + y и x + y − z. Выражения +(x, y) = 0 и ≤(+(x, +(y, −(z))), +(x, y)) являются атомарными формулами. Они обычно записываются как x + y = 0 и x + y − z ≤ x + y. является формулой, которая обычно записывается как . Эта формула имеет одну свободную переменную, z. Аксиомы для упорядоченных абелевых групп могут быть выражены в виде набора предложений на этом языке. Например, аксиома, утверждающая, что группа коммутативна, обычно записывается

Семантика

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

Оценка истинных значений

Формула оценивается как истинная или ложная при заданной интерпретации и присвоении переменных μ, которое сопоставляет элемент области дискурса каждой переменной. Причина, по которой требуется присвоение переменных, заключается в том, чтобы придать значения формулам со свободными переменными, например, значение истинности этой формулы меняется в зависимости от значений, которые обозначают x и y. Во-первых, присвоение переменных μ может быть расширено на все термы языка, в результате чего каждый терм сопоставляется с единственным элементом области дискурса. Для этого используются следующие правила: Переменные. Каждая переменная x оценивается в μ(x). Функции. Если термы были оценены в элементы области дискурса, и дан n-арный символ функции f, то терм f оценивается в [здесь должно быть продолжение, отсутствующее в оригинальном тексте]. Далее, каждой формуле присваивается значение истинности. Индуктивное определение, используемое для этого присвоения, называется Т-схемой. Атомные формулы (1). Формуле присваивается значение «истина» или «ложь» в зависимости от того, выполняется ли , где – это оценки термов и – это интерпретация , которая по предположению является подмножеством . Атомные формулы (2). Формуле присваивается «истина», если и оцениваются в один и тот же объект области дискурса (см. раздел о равенстве ниже). Логические связки. Формула вида , , и т.д. оценивается в соответствии с таблицей истинности для соответствующей связки, как в пропозициональной логике. Экзистенциальный квантор. Формула истинна относительно M и μ, если существует оценка переменных, которая отличается от μ максимум в отношении оценки x, такая, что φ истинна относительно интерпретации M и присвоения переменной μ. Это формальное определение отражает идею, что истинна тогда и только тогда, когда существует способ выбрать значение для x, такое, что φ(x) выполнено. Универсальный квантор. Формула истинна относительно M и μ, если φ(x) истинна для каждой пары, составленной интерпретацией M и некоторым присвоением переменной μ, которое отличается от μ максимум в отношении значения x. Это отражает идею, что истинна, если каждый возможный выбор значения для x приводит к тому, что φ(x) истинно. Если формула не содержит свободных переменных, то есть является высказыванием, то исходное присвоение переменных не влияет на её значение истинности. Иными словами, высказывание истинно относительно M и μ тогда и только тогда, когда оно истинно относительно M и любого другого присвоения переменной. Существует второй распространенный подход к определению значений истинности, который не опирается на функции присвоения переменных. Вместо этого, при заданной интерпретации M, к сигнатуре сначала добавляется набор константных символов, по одному для каждого элемента области дискурса в M; скажем, что для каждого d в области константный символ cd фиксирован. Интерпретация расширяется таким образом, что каждому новому константному символу присваивается соответствующий элемент области. Теперь истинность количественно определенных формул определяется синтаксически следующим образом: Экзистенциальный квантор (альтернативный). Формула истинна относительно M, если существует некоторое d в области дискурса, такое, что выполняется. Здесь – это результат подстановки cd на каждое свободное вхождение x в φ. Универсальный квантор (альтернативный). Формула истинна относительно M, если для каждого d в области дискурса истинна относительно M. Этот альтернативный подход дает точно такие же значения истинности для всех высказываний, как и подход через присвоение переменных.

Действительность, удовлетворительность и логическое следствие

Если предложение φ оценивается как истинное при данной интерпретации M, то говорят, что M удовлетворяет φ; это обозначается как . Предложение называется выполнимым, если существует интерпретация, при которой оно истинно. Это несколько отличается от символа из теории моделей, где обозначает выполнимость в модели, то есть "существует подходящее присваивание значений элементам области определения переменным символам". Выполнимость формул со свободными переменными более сложна, поскольку интерпретация сама по себе не определяет истинностное значение такой формулы. Общепринятое соглашение заключается в том, что формула φ со свободными переменными , , считается удовлетворенной интерпретацией, если формула φ остаётся истинной, независимо от того, какие индивиды из области дискурса подставляются на место её свободных переменных , ,. Это эквивалентно утверждению, что формула φ выполнима тогда и только тогда, когда её универсальное замыкание выполнимо. Формула называется логически истинной (или просто истинной), если она истинна во всех интерпретациях. Эти формулы играют роль, аналогичную тавтологиям в пропозициональной логике. Формула φ является логическим следствием формулы ψ, если всякая интерпретация, делающая ψ истинной, также делает φ истинной. В этом случае говорят, что φ логически вытекает из ψ.

Теории, модели и элементарные классы первого порядка

Теория первого порядка с заданной сигнатурой — это множество аксиом, представляющих собой формулы, состоящие из символов этой сигнатуры. Множество аксиом часто конечно или рекурсивно перечислимо, в этом случае теория называется эффективной. Некоторые авторы требуют, чтобы теория также включала все логические следствия аксиом. Аксиомы считаются истинными в рамках теории, и из них могут быть выведены другие формулы, истинные в рамках этой теории. Структура первого порядка, удовлетворяющая всем формулам данной теории, называется моделью этой теории. Элементарный класс — это множество всех структур, удовлетворяющих определенной теории. Эти классы являются основным объектом изучения в теории моделей. Многие теории имеют предполагаемую интерпретацию, то есть определенную модель, которую имеют в виду при изучении теории. Например, предполагаемая интерпретация арифметики Пеано состоит из обычных натуральных чисел с их обычными операциями. Однако теорема Лёвенгейма — Сколема показывает, что большинство теорий первого порядка также имеют другие, нестандартные модели. Теория называется непротиворечивой, если из её аксиом невозможно вывести противоречие. Теория называется полной, если для каждой формулы в её сигнатуре либо сама эта формула, либо её отрицание является логическим следствием аксиом теории. Теорема о неполноте Гёделя показывает, что эффективные теории первого порядка, включающие достаточную часть теории натуральных чисел, не могут быть одновременно непротиворечивыми и полными.

Дедуктивные системы

Дедуктивная система используется для демонстрации на чисто синтаксической основе, что одна формула является логическим следствием другой формулы. Существует множество таких систем для логики первого порядка, включая дедуктивные системы в стиле Гильберта, естественную дедукцию, исчисление секвенций, метод таблиц и метод резолюций. Они имеют общее свойство: дедукция является конечным синтаксическим объектом; формат этого объекта и способ его построения могут значительно различаться. Эти конечные выводы сами по себе часто называются выводами в теории доказательств. Их также часто называют доказательствами, но они полностью формализованы, в отличие от доказательств естественного языка в математике. Дедуктивная система называется корректной, если любая формула, которая может быть выведена в системе, логически истинна. И наоборот, дедуктивная система называется полной, если каждая логически истинная формула выводима. Все системы, обсуждаемые в этой статье, являются корректными и полными. Они также обладают свойством, что можно эффективно проверить, действительно ли является выводимым предположительно корректный вывод; такие системы вывода называются эффективными. Ключевым свойством дедуктивных систем является их чисто синтаксический характер, позволяющий проверять выводы без учета какой-либо интерпретации. Таким образом, корректный аргумент верен в каждой возможной интерпретации языка, независимо от того, относится ли эта интерпретация к математике, экономике или какой-либо другой области. В общем случае, логическое следствие в логике первого порядка является лишь полуразрешимым: если предложение А логически влечет предложение В, то это можно установить (например, путем поиска доказательства до тех пор, пока оно не будет найдено, используя некоторую эффективную, корректную и полную систему доказательств). Однако, если А не влечет логически В, это не означает, что А влечет логически отрицание В. Не существует эффективной процедуры, которая, имея на вход формулы А и В, всегда правильно определяла, влечет ли А логически В.

Правила вывода

Правило вывода утверждает, что, имея определенную формулу (или набор формул) с определенным свойством в качестве гипотезы, можно вывести другую конкретную формулу (или набор формул) в качестве заключения. Правило считается корректным (или сохраняющим истинность), если оно сохраняет валидность в том смысле, что всякий раз, когда некоторая интерпретация удовлетворяет гипотезе, эта же интерпретация удовлетворяет и заключению. Например, одним из распространенных правил вывода является правило подстановки. Если t – это терм, а φ – формула, возможно содержащая переменную x, то φ[t/x] – это результат замены всех свободных вхождений x на t в φ. Правило подстановки гласит, что для любой формулы φ и любого терма t можно вывести φ[t/x] из φ при условии, что в процессе подстановки ни одна свободная переменная t не становится связанной. (Если какая-либо свободная переменная t становится связанной, то для подстановки t вместо x сначала необходимо переименовать связанные переменные φ так, чтобы они отличались от свободных переменных t.) Чтобы понять, почему необходимо ограничение на связанные переменные, рассмотрим логически валидную формулу φ, заданную в сигнатуре (0, 1, +, ×, =) арифметики. Если t – это терм "x + 1", то формула φ[t/y] будет , которая окажется ложной во многих интерпретациях. Проблема в том, что свободная переменная x терма t стала связанной в процессе подстановки. Желаемая подстановка может быть получена путем переименования связанной переменной x в φ на что-то другое, например, z, так что формула после подстановки будет , которая снова является логически валидной. Правило подстановки демонстрирует несколько общих аспектов правил вывода. Оно полностью синтаксическое; можно определить, правильно ли оно применено, без обращения к какой-либо интерпретации. Оно имеет (синтаксически определенные) ограничения на условия применения, которые необходимо соблюдать для сохранения корректности вывода. Более того, как это часто бывает, эти ограничения необходимы из-за взаимодействия между свободными и связанными переменными, возникающего при синтаксических манипуляциях с формулами, участвующими в правиле вывода.

Системы в стиле Гильберта и естественная дедукция

Дедукция в дедуктивной системе в стиле Гильберта — это последовательность формул, каждая из которых является либо логической аксиомой, либо гипотезой, принятой для данного вывода, либо следует из предыдущих формул по правилу вывода. Логические аксиомы состоят из нескольких аксиоматических схем логически верных формул; они включают в себя значительную часть пропозициональной логики. Правила вывода позволяют оперировать кванторами. Типичные системы в стиле Гильберта имеют небольшое число правил вывода и несколько бесконечных схем логических аксиом. Обычно в качестве правил вывода используются только modus ponens и всеобщее обобщение. Системы натуральной дедукции схожи с системами в стиле Гильберта тем, что дедукция представляет собой конечную последовательность формул. Однако системы натуральной дедукции не содержат логических аксиом; они компенсируют это добавлением дополнительных правил вывода, позволяющих манипулировать логическими связками в формулах при доказательстве.

Последовательный анализ

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

где A1, …, An, B1, …, Bk – формулы, а символ "турникета" используется в качестве знака препинания для разделения двух частей. Интуитивно, секвенция выражает идею, что влечет за собой .

Метод Таблеа

В отличие от описанных выше методов, выводы в методе таблиц не представляют собой списки формул. Вместо этого, вывод является деревом формул. Чтобы показать, что формула А доказуема, метод таблиц пытается продемонстрировать, что отрицание А невыполнимо. Дерево вывода имеет корень; ветвление дерева отражает структуру формулы. Например, чтобы показать, что невыполнимо, требуется показать, что C и D каждое невыполнимо; это соответствует точке ветвления в дереве, где родитель – , а дочерние элементы – C и D.

Резолюция

Правило разрешения — это единое правило вывода, которое вместе с унификацией является корректным и полным для логики первого порядка. Как и в методе таблиц, формула доказывается путем показа того, что ее отрицание является невыполнимым. Резолюция широко используется в автоматическом доказательстве теорем. Метод резолюции работает только с формулами, являющимися дизъюнкциями атомарных формул; произвольные формулы должны быть предварительно преобразованы в эту форму посредством сколемизации. Правило разрешения утверждает, что из гипотез и , можно вывести заключение .

Логика первого порядка без равенства

Альтернативный подход рассматривает отношение равенства как нелогический символ. Эта конвенция известна как логика первого порядка без равенства. Если отношение равенства включено в сигнатуру, то аксиомы равенства теперь должны быть добавлены к рассматриваемым теориям, если это необходимо, вместо того чтобы считаться правилами логики. Основное различие между этим методом и логикой первого порядка с равенством заключается в том, что интерпретация теперь может интерпретировать два различных индивида как "равные" (хотя, в соответствии с законом Лейбница, они будут удовлетворять одним и тем же формулам при любой интерпретации). Иными словами, отношение равенства теперь может быть интерпретировано произвольным отношением эквивалентности на области определения, которое согласовано с функциями и отношениями данной интерпретации. Когда применяется эта вторая конвенция, термин "нормальная модель" используется для обозначения интерпретации, в которой никакие различные индивиды a и b не удовлетворяют равенству a = b. В логике первого порядка с равенством рассматриваются только нормальные модели, поэтому для модели, отличной от нормальной, нет отдельного термина. При изучении логики первого порядка без равенства необходимо изменять формулировки результатов, таких как теорема Лёвенхайма — Сколема, чтобы рассматривать только нормальные модели. Логика первого порядка без равенства часто используется в контексте арифметики второго порядка и других теорий арифметики высшего порядка, где отношение равенства между множествами натуральных чисел обычно опускается.

Металлологические свойства

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

Полная информация и нерешительность

Теорема полноты Гёделя, доказанная Куртом Гёделем в 1929 году, устанавливает существование корректных, полных и эффективных дедуктивных систем для логики первого порядка, и, следовательно, отношение логического следования в логике первого порядка определяется конечной доказуемостью. Интуитивно, утверждение о том, что формула φ логически влечет формулу ψ, зависит от каждой модели φ; эти модели, как правило, могут иметь произвольно большие кардинальности, и поэтому логическое следование нельзя эффективно проверить, рассматривая каждую модель. Однако можно перечислить все конечные выводы и искать вывод ψ из φ. Если ψ логически следует из φ, то такой вывод в конечном итоге будет найден. Таким образом, логическое следование в логике первого порядка является полуразрешимым: возможно эффективно перечислить все пары предложений (φ, ψ), такие что ψ является логическим следствием φ. В отличие от пропозициональной логики, логика первого порядка является неразрешимой (хотя и полуразрешимой), при условии, что язык содержит хотя бы один предикат арности не менее 2 (за исключением равенства). Это означает, что не существует алгоритма, который определял бы, являются ли произвольные формулы логически истинными. Этот результат был независимо установлен Алонзо Черчем и Аланом Тьюрингом в 1936 и 1937 годах соответственно, давая отрицательный ответ на Entscheidungsproblem, сформулированный Давидом Гильбертом и Вильгельмом Аккерманном в 1928 году. Их доказательства демонстрируют связь между неразрешимостью задачи о разрешимости для логики первого порядка и неразрешимостью задачи об остановке. Существуют системы, более слабые, чем полная логика первого порядка, для которых отношение логического следования является разрешимым. К ним относятся пропозициональная логика и монадическая логика предикатов, которая представляет собой логику первого порядка, ограниченную унарными символами предикатов и не содержащую символов функций. Другие разрешимые логики без символов функций включают охраняемый фрагмент логики первого порядка, а также логику двух переменных. Класс формул первого порядка Бернейса — Шёнфинкеля также является разрешимым. Разрешимые подмножества логики первого порядка также изучаются в рамках логик описаний.

Теорема ЛёвенхаймаШколема

Теорема Лёвенхейма-Сколема показывает, что если теория первого порядка кардинальности λ имеет бесконечную модель, то она имеет модели каждой бесконечной кардинальности, большей или равной λ. Один из самых ранних результатов в теории моделей, она подразумевает, что невозможно охарактеризовать счетность или несчетность на языке первого порядка с счетной сигнатурой. Иными словами, не существует формулы первого порядка φ(x), такой что произвольная структура M удовлетворяет φ тогда и только тогда, когда область определения M счетна (или, во втором случае, несчетна). Теорема Лёвенхейма-Сколема подразумевает, что бесконечные структуры нельзя категорически аксиоматизировать в логике первого порядка. Например, не существует теории первого порядка, единственной моделью которой является вещественная прямая: любая теория первого порядка с бесконечной моделью также имеет модель кардинальности, превышающей мощность континуума. Поскольку вещественная прямая бесконечна, любая теория, удовлетворяемая вещественной прямой, также удовлетворяется некоторыми нестандартными моделями. Применение теоремы Лёвенхейма-Сколема к теориям множеств первого порядка приводит к неинтуитивным следствиям, известным как парадокс Сколема.

Теорема компактности

Теорема компактности утверждает, что множество предложений первого порядка имеет модель тогда и только тогда, когда каждое конечное подмножество этого множества имеет модель. Это означает, что если формула является логическим следствием бесконечного множества аксиом первого порядка, то она является логическим следствием некоторого конечного числа этих аксиом. Эта теорема была впервые доказана Куртом Гёделем как следствие теоремы о полноте, но впоследствии было получено множество дополнительных доказательств. Это центральный инструмент в теории моделей, предоставляющий фундаментальный метод построения моделей. Теорема компактности накладывает ограничения на то, какие коллекции структур первого порядка являются элементарными классами. Например, теорема компактности подразумевает, что любая теория, имеющая произвольно большие конечные модели, имеет бесконечную модель. Следовательно, класс всех конечных графов не является элементарным классом (то же самое справедливо и для многих других алгебраических структур). Существуют также более тонкие ограничения логики первого порядка, вытекающие из теоремы компактности. Например, в информатике многие ситуации можно смоделировать как ориентированный граф состояний (узлов) и связей (ориентированных ребер). Проверка такой системы может потребовать доказательства того, что из любого "хорошего" состояния нельзя достичь ни одного "плохого" состояния. Таким образом, необходимо определить, находятся ли хорошие и плохие состояния в разных связных компонентах графа. Однако теорема компактности может быть использована для доказательства того, что связные графы не являются элементарным классом в логике первого порядка, и в логике графов не существует формулы φ(x, y) логики первого порядка, выражающей идею о существовании пути из x в y. Связность, однако, может быть выражена в логике второго порядка, но не только с помощью экзистенциальных кванторов множеств, поскольку она также обладает свойством компактности.

Теорема Линдстрем

Пер Линдстрем показал, что металогические свойства, которые мы только что обсудили, фактически характеризуют логику первого порядка в том смысле, что никакая более мощная логика не может обладать этими свойствами (Ebbinghaus and Flum 1994, Глава XIII). Линдстрем определил класс абстрактных логических систем и дал строгое определение относительной силы элементов этого класса. Он доказал две теоремы для систем этого типа: логическая система, удовлетворяющая определению Линдстрема и содержащая логику первого порядка, а также удовлетворяющая теореме Лёвенхайма-Школема и теореме о компактности, должна быть эквивалентна логике первого порядка. Логическая система, удовлетворяющая определению Линдстрема, обладающая полуразрешимым отношением логического следования и удовлетворяющая теореме Лёвенхайма-Школема, должна быть эквивалентна логике первого порядка.

Ограничения

Хотя логики первого порядка достаточно для формализации значительной части математики, и она широко используется в информатике и других областях, она имеет определенные ограничения. К ним относятся ограничения в выразительности и ограничения в описании фрагментов естественных языков. Например, логика первого порядка является неразрешимой, то есть не существует звучного, полного и завершающегося алгоритма для определения доказуемости. Это привело к изучению интересных разрешимых фрагментов, таких как C2: логика первого порядка с двумя переменными и кванторами подсчета и .

Выразительность

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

Формализация естественных языков

Логика первого порядка способна формализовать многие простые количественные конструкции в естественном языке, такие как "каждый человек, живущий в Перте, живет в Австралии". Таким образом, логика первого порядка используется в качестве основы для языков представления знаний, таких как FO(.). Тем не менее, существуют сложные особенности естественного языка, которые не могут быть выражены в логике первого порядка. "Любая логическая система, которая подходит в качестве инструмента для анализа естественного языка, нуждается в гораздо более богатой структуре, чем логика предикатов первого порядка".

Тип Пример Комментарий
Количественное определение свойств Если Иоанн самодоволен, то есть по крайней мере одна вещь, которую он имеет общего с Петром. Пример требует квантора над предикатами, который не может быть реализован в односортной логике первого порядка:
Количественное определение над свойствами Санта-Клаус обладает всеми атрибутами садиста. Пример требует кванторов над предикатами, который не может быть реализован в односортной логике первого порядка:
Предикативное наречие Джон быстро ходит. Пример нельзя проанализировать как; предикативные наречия – это не то же самое, что предикаты второго порядка, такие как цвет.
Относительное прилагательное Джамбо – маленький слон. Пример нельзя проанализировать как; предикативные прилагательные – это не то же самое, что предикаты второго порядка, такие как цвет.
Предикативный наречный модификатор Джон ходит очень быстро.
Относительный модификатор прилагательного Джамбо ужасно мал. Выражение, такое как "ужасно", при применении к относительному прилагательному, такому как "маленький", приводит к новому составному относительному прилагательному "ужасно маленький".
Предлоги Мэри сидит рядом с Джоном. Предлог "рядом с" при применении к "Джону" приводит к предикативному наречию "рядом с Джоном".

Ограничения, расширения и изменения

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

Многосортированная логика

Обычные интерпретации логики первого порядка имеют единую область дискурса, над которой варьируют все кванторы. Многосортная логика первого порядка позволяет переменным принадлежать к различным сортам, каждый из которых имеет свою область. Это также называют типизированной логикой первого порядка, где сорт называется типом (как в типе данных), но это не то же самое, что теория типов первого порядка. Многосортная логика первого порядка часто используется при изучении арифметики второго порядка. Если в теории конечное число сортов, многосортную логику первого порядка можно свести к логике первого порядка с единственным сортом. Для этого в теорию с единственным сортом вводят унарный предикатный символ для каждого сорта в многосортной теории и добавляют аксиому, утверждающую, что эти унарные предикаты разбивают область дискурса. Например, если есть два сорта, добавляют предикатные символы и и аксиому: Тогда элементы, удовлетворяющие , рассматриваются как элементы первого сорта, а элементы, удовлетворяющие , – как элементы второго сорта. Можно квантифицировать по каждому сорту, используя соответствующий предикатный символ для ограничения области квантификации. Например, чтобы сказать, что существует элемент первого сорта, удовлетворяющий формуле φ(x), записывают:
.

Дополнительные количественные показатели

Дополнительные кванторы могут быть добавлены в логику первого порядка. Иногда полезно сказать, что "P(x) истинно для ровно одного x", что может быть выражено как ∃!x P(x). Эта нотация, называемая квантификацией уникальности, может рассматриваться как сокращение формулы вида 1=∃x (P(x) ∧ ∀y (P(y) → (x = y))). Логика первого порядка с дополнительными кванторами имеет новые кванторы Qx, с значениями, такими как "существует много x, таких что ". Также см. разветвленные кванторы и плюральные кванторы Джорджа Булоса и других. Ограниченные кванторы часто используются в изучении теории множеств или арифметики.

Бесконечная логика

Бесконечная логика допускает бесконечно длинные предложения. Например, можно допустить конъюнкцию или дизъюнкцию бесконечного числа формул или квантификацию по бесконечному числу переменных. Бесконечно длинные предложения возникают в таких областях математики, как топология и теория моделей. Бесконечная логика обобщает логику первого порядка, позволяя формулы бесконечной длины. Наиболее распространенный способ, которым формулы могут становиться бесконечными, – это бесконечные конъюнкции и дизъюнкции. Однако также возможно допустить обобщенные сигнатуры, в которых символам функций и отношений разрешено иметь бесконечную арность, или в которых кванторы могут связывать бесконечно много переменных. Поскольку бесконечную формулу нельзя представить конечной строкой, необходимо выбрать другое представление формул; обычно в этом контексте используется дерево. Таким образом, формулы, по сути, отождествляются с их деревьями разбора, а не со строками, которые разбираются. Наиболее часто изучаемые бесконечные логики обозначаются Lαβ, где α и β – либо кардинальные числа, либо символ ∞. В этой нотации обычная логика первого порядка – Lωω. В логике L∞ω при построении формул допускаются произвольные конъюнкции или дизъюнкции, и существует неограниченное количество переменных. В более общем случае логика, допускающая конъюнкции или дизъюнкции с числом составляющих, меньшим κ, известна как Lκω. Например, Lω1ω допускает счетные конъюнкции и дизъюнкции. Множество свободных переменных в формуле Lκω может иметь любую кардинальность, строго меньшую κ, однако только конечное число из них может находиться в области действия любого квантора, когда формула является подформулой другой. В других бесконечных логиках подформула может находиться в области действия бесконечного числа кванторов. Например, в Lκ∞ один универсальный или экзистенциальный квантор может связывать произвольное число переменных одновременно. Аналогично, логика Lκλ допускает одновременную квантификацию по числу переменных, меньшему λ, а также конъюнкции и дизъюнкции размером меньше κ.

Неклассическая и модальная логика

Интуиционистская логика первого порядка использует интуиционистские, а не классические рассуждения; например, ¬¬φ не обязательно эквивалентно φ и ¬∀x.φ в общем случае не эквивалентно ∃x.¬φ. Модальная логика первого порядка позволяет описывать другие возможные миры, а также этот контингентно истинный мир, в котором мы находимся. В некоторых версиях множество возможных миров меняется в зависимости от того, в каком возможном мире находится наблюдатель. Модальная логика имеет дополнительные модальные операторы, значения которых можно неформально охарактеризовать, например, как "необходимо, чтобы φ" (истинно во всех возможных мирах) и "возможно, что φ" (истинно в некотором возможном мире). В стандартной логике первого порядка у нас есть один домен, и каждому предикату присваивается одно расширение. В модальной логике первого порядка у нас есть функция домена, которая присваивает каждому возможному миру свой собственный домен, так что каждое свойство получает расширение только относительно этих возможных миров. Это позволяет моделировать случаи, когда, например, Алекс – философ, но мог бы быть математиком, и мог бы вообще не существовать. В первом возможном мире P(a) истинно, во втором P(a) ложно, а в третьем возможном мире в домене вообще нет a. Нечеткие логики первого порядка являются расширениями первого порядка пропозициональной нечеткой логики, а не классического пропозиционального исчисления.

Логика фиксированной точки

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

Автоматизированное доказательство теоремы и формальные методы

Автоматическое доказательство теорем относится к разработке компьютерных программ, которые осуществляют поиск и находят выводы (формальные доказательства) математических теорем. Поиск выводов – сложная задача, поскольку пространство поиска может быть очень большим; исчерпывающий поиск каждого возможного вывода теоретически возможен, но вычислительно нереализуем для многих систем, представляющих интерес для математики. Поэтому разрабатываются сложные эвристические функции, чтобы попытаться найти вывод за время, меньшее, чем при слепом поиске. Связанная область – автоматизированная проверка доказательств – использует компьютерные программы для проверки корректности доказательств, созданных человеком. В отличие от сложных автоматических доказывающих теорем, системы верификации могут быть достаточно малы, чтобы их корректность можно было проверить как вручную, так и с помощью автоматизированной проверки программного обеспечения. Эта валидация проверяющего доказательства необходима для обеспечения уверенности в том, что любой вывод, помеченный как «корректный», действительно корректен. Некоторые проверяющие доказательства, такие как Metamath, требуют в качестве входных данных полный вывод. Другие, такие как Mizar и Isabelle, принимают хорошо отформатированный эскиз доказательства (который все еще может быть очень длинным и подробным) и заполняют недостающие части, выполняя простые поиски доказательств или применяя известные процедуры принятия решений: полученный вывод затем проверяется небольшим ядром ("ядром"). Многие из таких систем предназначены главным образом для интерактивного использования математиками: они известны как ассистенты доказательства. Они также могут использовать формальные логики, более сильные, чем логика первого порядка, такие как теория типов. Поскольку полное выведение любого нетривиального результата в дедуктивной системе первого порядка будет чрезвычайно длинным для написания человеком, результаты часто формализуются в виде серии лемм, для которых выводы могут быть построены отдельно. Автоматические доказывающие теоремы также используются для реализации формальной верификации в информатике. В этом контексте доказывающие теоремы используются для проверки корректности программ и аппаратного обеспечения, такого как процессоры, относительно формальной спецификации. Поскольку такой анализ занимает много времени и, следовательно, дорог, он обычно резервируется для проектов, в которых сбой может иметь серьезные последствия для людей или финансов. Для задачи проверки моделей известны эффективные алгоритмы, определяющие, удовлетворяет ли заданная конечная структура формуле первого порядка, а также границы вычислительной сложности: см.