Введение

Форма логики, позволяющая квантифицировать по предикатам. В логике и математике логика второго порядка является расширением логики первого порядка, которая, в свою очередь, является расширением логики высказываний. Логика второго порядка, в свою очередь, расширяется логикой высших порядков и теорией типов. Логика первого порядка квантифицирует только переменные, область значений которых – индивиды (элементы области рассуждений); логика второго порядка, помимо этого, квантифицирует по отношениям. Например, предложение второго порядка утверждает, что для любой формулы P и любого индивида x, либо Px истинно, либо ¬Px истинно (это закон исключённого третьего). Логика второго порядка также включает квантификацию по множествам, функциям и другим переменным (см. раздел ниже). И логика первого, и логика второго порядка используют понятие области рассуждений (часто называемой просто "областью" или "универсумом"). Область – это множество, над которым квантифицируются отдельные элементы.

Синтаксис и фрагменты

Синтаксис логики второго порядка определяет, какие выражения являются корректными формулами. В дополнение к синтаксису логики первого порядка, логика второго порядка включает множество новых сортов (иногда называемых типами) переменных. Это:

Сорт переменных, область значений которых – множества индивидов. Если S – переменная этого сорта, а t – терм первого порядка, то выражение t ∈ S (также записывается как S(t) или St для сокращения записи) является атомарной формулой. Множества индивидов также можно рассматривать как унарные отношения на области. Для каждого натурального числа k существует сорт переменных, область значений которых – все k-арные отношения на индивидах. Если R – такая k-арная переменная отношения, а t1, …, tk – термы первого порядка, то выражение R(t1, …, tk) является атомарной формулой. Для каждого натурального числа k существует сорт переменных, область значений которых – все функции, принимающие k элементов области и возвращающие один элемент области. Если f – такая k-арная переменная функции, а t1, …, tk – термы первого порядка, то выражение f(t1, …, tk) является термом первого порядка. Каждая из только что определенных переменных может быть подвергнута универсальной и/или экзистенциальной квантификации для построения формул. Таким образом, существует множество видов кванторов, по два для каждого сорта переменных. Предложение в логике второго порядка, как и в логике первого порядка, является корректной формулой, не содержащей свободных переменных (любого сорта). Можно обойтись без введения переменных функций в приведенном выше определении (и некоторые авторы поступают именно так), поскольку k-арную переменную функции можно представить переменной отношения арности k+1 и соответствующей формулой, обеспечивающей однозначность "результата" в k+1-м аргументе отношения. (Shapiro 2000, p. 63)

Монадическая логика второго порядка (MSO) – это ограничение логики второго порядка, в котором допускается только квантификация по унарным отношениям (т.е. множествам). Следовательно, квантификация по функциям, в силу эквивалентности отношениям, как описано выше, также не допускается. Логика второго порядка без этих ограничений иногда называется полной логикой второго порядка, чтобы отличать ее от монадической версии. Монадическая логика второго порядка особенно используется в контексте теоремы Курселя, алгоритмической метатеоремы в теории графов. Теория MSO для полного бесконечного двоичного дерева (S2S) является разрешимой. В отличие от этого, полная логика второго порядка над любым бесконечным множеством (или MSO-логика над, например, (,+)) может интерпретировать истинную арифметику второго порядка. Как и в логике первого порядка, логика второго порядка может включать нелогические символы в конкретном языке второго порядка. Однако они ограничены тем, что все термы, которые они образуют, должны быть либо термами первого порядка (которые могут быть подставлены вместо переменной первого порядка), либо термами второго порядка (которые могут быть подставлены вместо переменной второго порядка соответствующего сорта). Формула в логике второго порядка называется формулой первого порядка (и иногда обозначается как Σ₀ или Π₀), если ее кванторы (которые могут быть универсальными или экзистенциальными) охватывают только переменные первого порядка, хотя она может содержать свободные переменные второго порядка. Формула Σ₁ (экзистенциальной логики второго порядка) – это формула, которая дополнительно содержит некоторые экзистенциальные кванторы над переменными второго порядка, т.е. ∃SΦ, где Φ – формула первого порядка. Фрагмент логики второго порядка, состоящий только из экзистенциальных формул второго порядка, называется экзистенциальной логикой второго порядка и обозначается как ESO, как Σ₁, или даже как ∃SO. Фрагмент формул Π₁ определяется дуально, он называется универсальной логикой второго порядка. Более выразительные фрагменты определяются для любого k > 0 посредством взаимной рекурсии: Σₖ имеет вид ∃SΦ, где Φ – формула Πₖ, и аналогично, Πₖ имеет вид ∀SΦ, где Φ – формула Σₖ. (См. аналитическую иерархию для аналогичного построения арифметики второго порядка.)

Семантика

Семантика логики второго порядка устанавливает значение каждого предложения. В отличие от логики первого порядка, которая имеет только одну стандартную семантику, для логики второго порядка обычно используются две различные семантики: стандартная семантика и семантика Хенкина. В каждой из этих семантик интерпретации кванторов первого порядка и логических связок такие же, как и в логике первого порядка. Различаются лишь области определения кванторов над переменными второго порядка (Väänänen 2001). В стандартной семантике, также называемой полной семантикой, кванторы простираются на все множества или функции соответствующего типа. Таким образом, как только область определения переменных первого порядка установлена, значение остальных кванторов фиксируется. Именно эта семантика придает логике второго порядка ее выразительную силу, и она будет предполагаться на протяжении всей статьи. Леон Хенкин (1950) определил альтернативный вид семантики для теорий второго и высшего порядков, в котором значение областей высшего порядка частично определяется явной аксиоматизацией, основанной на теории типов, свойств множеств или функций, над которыми определены кванторы. Семантика Хенкина – это разновидность многосортированной семантики первого порядка, где существует класс моделей аксиом, а не фиксированная семантика, ограничивающаяся только стандартной моделью, как в стандартной семантике. Модель в семантике Хенкина предоставляет набор множеств или набор функций в качестве интерпретации областей высшего порядка, который может быть собственным подмножеством всех множеств или функций данного типа. Для своей аксиоматизации Хенкин доказал, что теоремы о полноте и компактности Гёделя, справедливые для логики первого порядка, переносятся на логику второго порядка с семантикой Хенкина. Поскольку теоремы Сколема-Лёвенхайма также применимы к семантике Хенкина, теорема Линдстрема утверждает, что модели Хенкина являются лишь замаскированными моделями первого порядка. Для теорий, таких как арифметика второго порядка, существование нестандартных интерпретаций областей высшего порядка – это не просто недостаток конкретной аксиоматизации, полученной из теории типов, которую использовал Хенкин, а необходимое следствие теоремы о неполноте Гёделя: аксиомы Хенкина нельзя дополнить, чтобы гарантировать, что стандартная интерпретация является единственной возможной моделью. Семантика Хенкина обычно используется при изучении арифметики второго порядка. Юко Вэнанен (2001) утверждал, что выбор между моделями Хенкина и полными моделями для логики второго порядка аналогичен выбору между ZFC и V в качестве основы теории множеств: «Как и в логике второго порядка, мы не можем по-настоящему выбрать, аксиоматизировать ли математику, используя V или ZFC. Результат одинаков в обоих случаях, поскольку ZFC является лучшей попыткой на сегодняшний день использовать V в качестве аксиоматизации математики».

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

Логика второго порядка более выразительна, чем логика первого порядка. Например, если область определения – множество всех действительных чисел, в логике первого порядка можно утверждать существование аддитивной обратной для каждого действительного числа, записав ∀x ∃y (x + y = 0), но для утверждения свойства наименьшей верхней границы для множеств действительных чисел требуется логика второго порядка, которое гласит, что каждое ограниченное, непустое множество действительных чисел имеет супремум. Если область определения – множество всех действительных чисел, то следующее предложение второго порядка (разбитое на две строки) выражает свойство наименьшей верхней границы:

Эта формула является прямой формализацией утверждения "для каждого множества A". Можно показать, что любое упорядоченное поле, удовлетворяющее этому свойству, изоморфно полю действительных чисел. С другой стороны, множество предложений первого порядка, истинных для действительных чисел, имеет произвольно большие модели в силу теоремы о компактности. Таким образом, свойство наименьшей верхней границы не может быть выражено никаким набором предложений в логике первого порядка. (Фактически, каждое вещественно замкнутое поле удовлетворяет тем же предложениям первого порядка в данной сигнатуре, что и действительные числа.) В логике второго порядка можно записать формальные предложения, утверждающие, что "область определения конечна" или "область определения имеет счетную кардинальность". Чтобы утверждать, что область определения конечна, используйте предложение, утверждающее, что каждая сюръективная функция из области определения в себя инъективна. Чтобы утверждать, что область определения имеет счетную кардинальность, используйте предложение, утверждающее, что между любыми двумя бесконечными подмножествами области определения существует биекция. Из теоремы о компактности и теоремы Лёвенхайма-Школема вверх следует, что невозможно охарактеризовать конечность или счетность соответственно в логике первого порядка. Определенные фрагменты логики второго порядка, такие как ESO, также более выразительны, чем логика первого порядка, хотя они строго менее выразительны, чем полная логика второго порядка. ESO также обладает эквивалентностью перевода с некоторыми расширениями логики первого порядка, допускающими нелинейное упорядочение зависимостей кванторов, например, логикой первого порядка, расширенной кванторами Хенкина, логикой независимости Хинтикки и Санду, а также логикой зависимости Вейнянена.

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

Дедуктивная система логики — это набор правил вывода и логических аксиом, определяющих, какие последовательности формул составляют корректные доказательства. Для логики второго порядка можно использовать несколько дедуктивных систем, однако ни одна из них не является полной для стандартной семантики (см. ниже). Каждая из этих систем является надёжной, то есть любое предложение, которое может быть доказано с её помощью, логически верно в соответствующей семантике. Наиболее слабая дедуктивная система, которую можно использовать, состоит из стандартной дедуктивной системы для логики первого порядка (например, натурального вывода), дополненной правилами подстановки для термов второго порядка. Эта дедуктивная система обычно используется при изучении арифметики второго порядка. Дедуктивные системы, рассмотренные Шапиро (1991) и Хенкином (1950), добавляют к расширенной дедуктивной схеме первого порядка как аксиомы понимания, так и аксиомы выбора. Эти аксиомы надёжны для стандартной семантики второго порядка. Они также надёжны для семантики Хенкина, ограниченной моделями Хенкина, удовлетворяющими аксиомам понимания и выбора.

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

Можно попытаться свести теорию второго порядка действительных чисел, с полной семантикой второго порядка, к теории первого порядка следующим образом. Сначала расширяем область определения от множества всех действительных чисел до двухсортированной области, причем вторая сортировка содержит все множества действительных чисел. Добавляем новый бинарный предикат в язык: отношение принадлежности. Затем предложения второго порядка становятся предложениями первого порядка, при этом кванторы второго порядка теперь относятся ко второй сортировке. Это сведение можно попытаться осуществить в односортированной теории, добавив унарные предикаты, указывающие, является ли элемент числом или множеством, и принимая область определения как объединение множества действительных чисел и множества степеней множества действительных чисел. Но обратите внимание, что область определения была определена так, чтобы включать все множества действительных чисел. Это требование нельзя свести к предложениям первого порядка, как показывает теорема Лёвенхайма — Сколема. Эта теорема подразумевает, что существует некоторое счетно бесконечное подмножество действительных чисел, элементы которого мы будем называть внутренними числами, и некоторое счетно бесконечное множество множеств внутренних чисел, элементы которого мы будем называть «внутренними множествами», так что область определения, состоящая из внутренних чисел и внутренних множеств, удовлетворяет тем же предложениям первого порядка, что и область определения действительных чисел и множеств действительных чисел. В частности, она удовлетворяет своего рода аксиоме наименьшей верхней границы, которая, по сути, гласит: каждое непустое внутреннее множество, имеющее внутреннюю верхнюю границу, имеет наименьшую внутреннюю верхнюю границу. Счетность множества всех внутренних чисел (в сочетании с тем фактом, что они образуют плотно упорядоченное множество) подразумевает, что это множество не удовлетворяет полной аксиоме наименьшей верхней границы. Счетность множества всех внутренних множеств подразумевает, что оно не является множеством всех подмножеств множества всех внутренних чисел (поскольку теорема Кантора подразумевает, что множество всех подмножеств счетного бесконечного множества является несчетным бесконечным множеством). Эта конструкция тесно связана с парадоксом Сколема. Таким образом, теория первого порядка действительных чисел и множеств действительных чисел имеет множество моделей, некоторые из которых счетны. Однако теория второго порядка действительных чисел имеет только одну модель. Это следует из классической теоремы о том, что существует только одно архимедово полное упорядоченное поле, а также из того факта, что все аксиомы архимедово полного упорядоченного поля выразимы в логике второго порядка. Это показывает, что теорию второго порядка действительных чисел нельзя свести к теории первого порядка, в том смысле, что теория второго порядка действительных чисел имеет только одну модель, а соответствующая теория первого порядка имеет множество моделей. Существуют более радикальные примеры, показывающие, что логика второго порядка со стандартной семантикой более выразительна, чем логика первого порядка. Существует конечная теория второго порядка, единственной моделью которой являются действительные числа, если выполняется гипотеза континуума, и которая не имеет модели, если гипотеза континуума не выполняется (см. Shapiro 2000, с. 105). Эта теория состоит из конечной теории, характеризующей действительные числа как полное архимедово упорядоченное поле, плюс аксиома, утверждающая, что область определения имеет первую несчётную кардинальность. Этот пример иллюстрирует, что вопрос о том, является ли предложение в логике второго порядка непротиворечивым, чрезвычайно сложен. Дополнительные ограничения логики второго порядка описаны в следующем разделе.

История и спорная стоимость

Предикатная логика была введена в математическое сообщество К. С. Пирсом, который ввёл термин «логика второго порядка» и чья нотация наиболее близка к современной форме (Путнам, 1982). Однако сегодня большинство изучающих логику лучше знакомы с работами Фреге, который опубликовал свои труды за несколько лет до Пирса, но они оставались менее известными, пока Бертран Рассел и Альфред Норт Уайтхед не сделали их знаменитыми. Фреге использовал различные переменные для различения квантификации над объектами и квантификации над свойствами и множествами; однако он не считал, что занимается двумя разными видами логики. После открытия парадокса Рассела стало ясно, что в его системе что-то не так. В конечном итоге логики обнаружили, что ограничение логики Фреге различными способами — до того, что сейчас называется логикой первого порядка, — устраняет эту проблему: в логике первого порядка нельзя квантифицировать над множествами и свойствами. Стандартная иерархия порядков логик восходит к этому времени. Было установлено, что теорию множеств можно сформулировать как аксиоматизированную систему в рамках аппарата логики первого порядка (ценой некоторой потери полноты, но не столь серьёзной, как парадокс Рассела), и это было сделано (см. теорию множеств Цермело — Френкеля), поскольку множества имеют решающее значение для математики. Арифметика, мереология и множество других мощных логических теорий могут быть сформулированы аксиоматически без обращения к какому-либо более сложному логическому аппарату, чем квантификация первого порядка, и это, наряду с приверженностью Гёделя и Сколема логике первого порядка, привело к общему снижению интереса к логике второго (или более высокого) порядка. Это отрицание активно поддерживали некоторые логики, в частности У. В. Куайн. Куайн придерживался мнения, что в предикатных предложениях, таких как Fx, «x» следует понимать как переменную или имя, обозначающее объект, и, следовательно, над ним можно квантифицировать, как в «Для всех вещей верно, что…», а «F» следует понимать как сокращение для неполного предложения, а не как имя объекта (даже не абстрактного объекта, такого как свойство). Например, это может означать «… является собакой». Но не имеет смысла предполагать, что мы можем квантифицировать над чем-то подобным. (Эта позиция вполне согласуется с собственными аргументами Фреге о различии между понятием и объектом). Таким образом, использование предиката в качестве переменной означает, что он занимает место имени, которое должны занимать только индивидуальные переменные. Этот вывод был отвергнут Джорджем Булосом. В последние годы логика второго порядка переживает некоторое возрождение, чему способствовала интерпретация Булосом квантификации второго порядка как множественной квантификации над той же областью объектов, что и квантификация первого порядка (Булос, 1984). Булос также указывает на заявленную невыразимость в логике первого порядка предложений, таких как «Некоторые критики восхищаются только друг другом» и «Некоторые из людей Фианчетто вошли на склад, не сопровождаемые никем другим», которые, по его мнению, можно выразить только всей силой квантификации второго порядка. Однако обобщённая квантификация и частично упорядоченная (или разветвлённая) квантификация могут быть достаточными для выражения определённого класса предположительно невыразимых в логике первого порядка предложений, и они не используют квантификацию второго порядка.