Логика первого порядка - также известный как логика предикатов, квантификационная логика и исчисление предикатов первого порядка - представляет собой набор формальных систем, используемых в математика, философия, лингвистика и информатика. Логика первого порядка использует количественные переменные вместо нелогических объектов и позволяет использовать предложения, содержащие переменные, так что вместо предложений типа «Сократ - человек» можно иметь выражения в форме «существует x такое, что x - это Сократ, а x - человек», где «существует» - это квантор, а x - переменная. Это отличает его от логики высказываний, которая не использует кванторы или отношения ; в этом смысле логика высказываний является основой логики первого порядка.
Теория по теме обычно представляет собой логику первого порядка вместе с определенной областью дискурса (по которой измеряются количественные переменные), конечным числом функций из этой области в себя, конечным числом множество предикатов , определенных в этой области, и набор аксиом, которые, как считается, применимы к ним. Иногда «теория» понимается в более формальном смысле, который представляет собой просто набор предложений в логике первого порядка.
Прилагательное «первого порядка» отличает логику первого порядка от логики более высокого порядка, в которой есть предикаты, имеющие предикаты или функции в качестве аргументов, или в которых один или оба предиката кванторы или кванторы функций разрешены. В теориях первого порядка предикаты часто связаны с множествами. В интерпретируемых теориях высшего порядка предикаты могут интерпретироваться как наборы множеств.
Существует множество дедуктивных систем для логики первого порядка, которые одновременно надежны (т. Е. Все доказуемые утверждения верны во всех моделях) и полны (т.е. все утверждения, которые верны во всех моделях, доказуемы). Хотя отношение логического следствия является только полуразрешимым, большой прогресс был достигнут в автоматическом доказательстве теорем в логике первого порядка. Логика первого порядка также удовлетворяет ряду металогических теорем, которые делают ее доступной для анализа в рамках теории доказательств, таких как теорема Левенгейма – Сколема и компактность Теорема.
Логика первого порядка является стандартом для формализации математики в аксиомы и изучается в основах математики. Арифметика Пеано и теория множеств Цермело – Френкеля являются аксиоматизацией теории чисел и теории множеств, соответственно, в логику первого порядка. Однако никакая теория первого порядка не способна однозначно описать структуру с бесконечной областью, например, натуральными числами или вещественной линией. Системы аксиом, которые полностью описывают эти две структуры (то есть категориальные системы аксиом), могут быть получены в более сильных логиках, таких как логика второго порядка.
Были разработаны основы логики первого порядка независимо друг от друга Готтлоб Фреге и Чарльз Сандерс Пирс. Об истории логики первого порядка и о том, как она стала доминировать в формальной логике, см. José Ferreirós (2001).
В то время как логика высказываний имеет дело с простыми декларативными предложениями, логика первого порядка дополнительно охватывает предикаты и квантификация.
Предикат принимает объект или объекты в области дискурса в качестве входных данных, в то время как выходные данные имеют значение True или False. Рассмотрим два предложения: «Сократ - философ» и «Платон - философ». В логике высказываний эти предложения рассматриваются как не связанные между собой и могут быть обозначены, например, такими переменными, как p и q. Предикат «является философом» встречается в обоих предложениях, которые имеют общую структуру «а является философом». Переменная a представлена как «Сократ» в первом предложении и как «Платон» во втором предложении. В то время как логика первого порядка допускает использование предикатов, таких как «является философом» в этом примере, логика высказываний не позволяет.
Отношения между предикатами могут быть установлены с помощью логических связок. Рассмотрим, например, формулу первого порядка «если а - философ, то а - ученый». Эта формула представляет собой условное утверждение с гипотезой «а - философ» и выводом «а - ученый». Истинность этой формулы зависит от того, какой объект обозначается a, и от интерпретации предикатов «является философом» и «является ученым».
Квантификаторы можно применять к переменным в формуле. Переменная а в предыдущей формуле может быть универсально определена количественно, например, с помощью предложения первого порядка «Для каждого а, если а - философ, то а - ученый». универсальный квантор «для каждого» в этом предложении выражает идею о том, что утверждение «если а - философ, то а - ученый» справедливо для всех вариантов выбора а.
отрицание предложения «Для каждого а, если а - философ, то а - ученый» логически эквивалентно предложению «Существует такое, что а - философ а не ученый ". экзистенциальный квантор «существует» выражает идею о том, что утверждение «а - философ, а а - не ученый» справедливо для некоторого выбора а.
Предикаты «философ» и «ученый» принимают одну переменную. Как правило, предикаты могут принимать несколько переменных. В предложении первого порядка «Сократ - учитель Платона» предикат «является учителем» принимает две переменные.
Интерпретация (или модель) формулы первого порядка определяет значение каждого предиката и сущности, которые могут создавать экземпляры переменных. Эти сущности образуют область дискурса или вселенную, которая обычно должна быть непустым множеством. Например, в интерпретации с областью дискурса, состоящей из всех людей и сказуемого «является философом», понимаемым как «был автором Республики », предложение «Существует такое, что является философом "рассматривается как истина, о чем свидетельствует Платон.
Есть две ключевые части логики первого порядка. Синтаксис определяет, какие конечные последовательности символов являются правильно сформированными выражениями в логике первого порядка, а семантика определяет значения этих выражений.
В отличие от естественных языков, таких как английский, язык логики первого порядка является полностью формальным, так что можно механически определить, правильно ли сформировано данное выражение. Есть два ключевых типа правильно сформированных выражений: термины, которые интуитивно представляют объекты, и формулы, которые интуитивно выражают предикаты, которые могут быть истинными или ложными. Термины и формулы логики первого порядка представляют собой строки из символов, где все символы вместе образуют алфавит языка. Как и во всех формальных языках, природа самих символов выходит за рамки формальной логики; их часто считают просто буквами и знаками препинания.
Обычно символы алфавита делятся на логические символы, которые всегда имеют одинаковое значение, и нелогические символы, значение которых зависит от интерпретации.. Например, логический символ всегда представляет собой «и»; он никогда не интерпретируется как «или», что представлено логическим символом . С другой стороны, нелогический предикатный символ, такой как Phil (x), можно интерпретировать как означающий «x - философ», «x - человек по имени Филипп» или любой другой унарный предикат в зависимости от рассматриваемой интерпретации.
В алфавите есть несколько логических символов, которые различаются в зависимости от автора,но обычно включают:
Не все эти символы являются обязательными - достаточно только одного из кванторов, отрицания и конъюнкции, переменных, скобок и равенства. Существует множество незначительных вариаций, которые могут определять дополнительные логические символы:
нелогические символы представляют собой предикаты (отношения), функции и константы в области дискурса. Раньше стандартной практикой было использование фиксированного бесконечного набора нелогических символов для всех целей. Более поздняя практика заключается в использовании различных нелогических символов в зависимости от предполагаемого приложения. Следовательно, возникла необходимость дать имена набору всех нелогических символов, используемых в конкретном приложении. Этот выбор осуществляется с помощью подписи.
Традиционный подход состоит в том, чтобы иметь только один бесконечный набор нелогических символов (одна подпись) для всех приложений. Следовательно, при традиционном подходе существует только один язык логики первого порядка. Этот подход все еще распространен, особенно в философских книгах.
В современной математической логике подпись зависит от приложения. Типичные сигнатуры в математике: {1, ×} или просто {×} для групп или {0, 1, +, ×, <} for упорядоченных полей. Нет ограничений на количество нелогических символов. Подпись может быть пустой, конечной или бесконечной, даже несчетной. Несчетное количество подписей встречается, например, в современных доказательствах теоремы Левенхайма – Сколема.
В этом подходе каждый нелогический символ относится к одному из следующих типов.
. Традиционный подход может быть восстановлен в современном подходе, просто указав "пользовательскую" сигнатуру, состоящую из традиционные последовательности нелогических символов.
BNF грамматика |
---|
|
Вышеупомянутая контекстно-свободная грамматика в форме Бэкуса-Наура определяет язык синтаксически допустимых формул первого порядка с функциональными символами и символами предикатов до арности 3. Для более высоких арностей требуется необходимо соответствующим образом адаптировать. |
Пример формулы ∀x ∃x '(¬x = c) ⇒ f2 (x, x') = c ' описывает мультипликативные инверсии, когда f2' , c и c ' интерпретируются как умножение, ноль и единица соответственно. |
Правила формирования определяют термины и формулы логики первого порядка. Когда термины и формулы представлены в виде строк символов, эти правила можно использовать для написания формальной грамматики для терминов и формул. Эти правила обычно контекстно-свободные (каждая продукция имеет один символ с левой стороны), за исключением того, что набор символов может быть бесконечным и может быть много начальных символов, например переменные в случае терминов.
Набор терминов индуктивно определяется следующими правилами:
Терминами являются только выражения, которые могут быть получены конечным числом применений правил 1 и 2. Например, никакое выражение, содержащее символ предиката, не является термином.
Набор формул (также называемых правильно сформированных формул или WFF ) индуктивно определяется следующими правилами:
Только выражения, которые могут быть получены конечным числом приложений правила 1–5 являются формулами. Формулы, полученные из первых двух правил, называются атомарными формулами.
. Например,
- это формула, если f - унарный функциональный символ, P - унарный предикатный символ, а Q - троичный предикатный символ. С другой стороны, не является формулой, хотя это строка символов алфавита.
Роль круглых скобок в определении состоит в том, чтобы гарантировать, что любую формулу можно получить только одним способом - следуя индуктивному определению (т. Е. Существует уникальное дерево разбора для каждого формула). Это свойство известно как уникальная читаемость формул. Существует многосоглашений о том, где скобки используются в формулах. Например, некоторые авторы используют двоеточия или точки вместо круглых скобок или меняют места, в которых они вставляются. Определение каждого автора должно сопровождаться доказательством уникальной читаемости.
Это определение формулы не поддерживает определение функции if-then-else ite (c, a, b), где "c" - это условие, выраженное в виде формулы, которая вернет «a», если c истинно, и «b», если оно ложно. Это связано с тем, что и предикаты, и функции могут принимать только термины в качестве параметров, но первый параметр - это формула. Некоторые языки, построенные на логике первого порядка, такие как SMT-LIB 2.0, добавляют это.
Для удобства были разработаны соглашения о приоритете логических операторов, чтобы избежать необходимость писать круглые скобки в некоторых случаях. Чт Эти правила аналогичны порядку операций в арифметике. Общее соглашение:
Кроме того, дополнительная пунктуация не требуется определение может быть вставлено - для облегчения чтения формул. Таким образом, формула
может быть записана как
В некоторых полях обычно используется инфиксная нотация для двоичных отношений и функций, вместо обозначения префикса, определенного выше. Например, в арифметике обычно пишут «2 + 2 = 4» вместо «= (+ (2,2), 4)». Принято рассматривать формулы в инфиксной записи как аббревиатуры соответствующих формул в префиксной записи, ср. также структура термина и представление.
В приведенных выше определениях используется инфиксная нотация для двоичных связок, например . Менее распространенное соглашение - польская нотация, в которой пишут , и так далее перед их аргументы, а не между ними. Это соглашение выгодно тем, что позволяет отбрасывать все символы пунктуации. Таким образом, польские обозначения компактны и элегантны, но редко используются на практике, потому что их трудно читать людям. В польской нотации формула
становится «∀x∀y → Pfx¬ → PxQfyxz».
В формуле переменная может встречаться свободной или связанной (или и тем, и другим). Интуитивно понятно, что переменная может быть в формуле свободна, если она не определена количественно: в ∀y P (x, y) единственное вхождение переменной x является свободным, в то время как y является связанным. Вхождения свободных и связанных переменных в формулу индуктивно определяются следующим образом.
Например, в ∀x ∀y (P (x) → Q (x, f (x), z)) x и y встречаются только связанными, z встречается только свободен, и w не является ни тем, ни другим, потому что он не встречается в формуле.
Свободные и связанные переменные формулы не обязательно должны быть непересекающимися множествами: в формуле P (x) → ∀x Q (x) первое вхождение x в качестве аргумента P является свободным, а второе один, как аргумент Q, связан.
Формула в логике первого порядка без вхождений свободных переменных называется предложением первого порядка. Это формулы, которые будут иметь четко определенные значения истинности при интерпретации. Например, истинность такой формулы, как Phil (x), должна зависеть от того, чтопредставляет x. Но предложение ∃x Phil (x) будет либо истинным, либо ложным в данной интерпретации.
В математике язык упорядоченных абелевых групп имеет один постоянный символ 0, один унарный функциональный символ -, один двоичный функциональный символ +, и один символ двоичного отношения ≤. Тогда:
Аксиомы упорядоченных абелевых групп могут быть выражены в виде набора предложений на языке. Например, аксиома, утверждающая, что группа коммутативна, обычно записывается как
интерпретация языка первого порядка присваивает обозначение каждого нелогического символа в этом языке. Он также определяет область дискурса, которая определяет диапазон квантификаторов. В результате каждому термину назначается объект, который он представляет, каждому предикату присваивается свойство объектов и каждому предложению присваивается значение истинности. Таким образом, интерпретация придает семантическое значение терминам, предикатам и формулам языка. Изучение интерпретаций формальных языков называется формальной семантикой. Далее следует описание стандартной или тарской семантики для логики первого порядка. (Также возможно определить семантику игры для логики первого порядка, но помимо требования аксиомы выбора, семантика игры согласуется с семантикой Тарского для логики первого порядка, поэтому игра семантика здесь не рассматривается.)
Область дискурса D - это непустой набор «объектов» некоторого вида. Интуитивно формула первого порядка - это утверждение об этих объектах; например, заявляет о существовании объекта x, такого что предикат P истинен там, где он упоминается. Область дискурса - это совокупность рассматриваемых объектов. Например, можно принять как набор целых чисел.
Символ функции интерпретируется как функция. Например, если область дискурса состоит из целых чисел, символ функции f арности 2 можно интерпретировать как функцию, которая дает сумму своих аргументов. Другими словами, символ f связан с функцией I (f), которая в этой интерпретации является сложением.
Интерпретация постоянного символа - это функция из одноэлементного набора от D до D, которую можно просто идентифицировать с объектом в D. Например, интерпретация может присвоить значение до символа константы .
Интерпретация n-мерного символа предиката представляет собой набор n -наборы элементов предметной области дискурса. Это означает, что, учитывая интерпретацию, предикатный символ и n элементов предметной области, можно сказать, является ли предикат истинным для этих элементов в соответствии с данной интерпретацией. Например, интерпретация I (P) двоичного символа предиката P может представлять собой набор пар целых чисел, таких, что первое меньше второго. Согласно этой интерпретации, предикат P будет истинным, если его первый аргумент меньше второго.
Наиболее распространенный способ задания интерпретации (особенно в математике) - это указать структуру (также называемую моделью ; см. ниже). Структура состоит из непустого множества D, образующего область дискурса, и интерпретации I нелогических терминов подписи. Эта интерпретация сама по себе является функцией:
Формула оценивает, как истинная или ложная с учетом интерпретации, и присвоение переменной μ, которое связывает элемент предметной области с каждой переменной. Причина, по которой требуется присвоение формулы со свободными переменными, например, . Значение истинности формулы меняется в зависимости от того, обозначают ли x и y и того же человека.
Во-первых, универсальных единиц может быть расширено все термины языка, в результате чего каждый отображается на отдельный элемент предметной области. Для этого используются следующие правила:
Затем каждая формуле присваивается значение истинности. Индуктивное определение, используемое для этого присвоения, называется присвоение вызова, и доказано, что это значение истинности не зависит от того, какое назначение выбрано. Этот метод не работает, если вообще нет функций присваивания; его необходимо изменить, чтобы разместить пустые домены.
Таким образом, когда пустой домен разрешен, его часто следует рассматривать как особый случай. Однако большинство авторов просто исключают пустой домен по определению.
A дедуктивная система используется для демонстрации чисто синтаксической основы, что одна формула является логическим следствием другой формулы. Существует множество таких систем для логики первого порядка, включая дедуктивные системы гильбертова, естественный вывод, последовательное исчисление, метод таблиц и разрешение. У них есть общее свойство, заключающееся в том, что дедукция - это конечный синтаксический объект; формат этого объекта и способ его построения сильно различаются. Эти конечные выводы часто называются выводами в теории доказательств. Их также часто называют доказательствами, но они полностью формализованы, в отличие от естественных математических доказательств.
. Дедуктивная система надежна, если любая формула, которая может быть выведена в системе, логически верна. И наоборот, дедуктивная система полная, если можно вывести любую логически действительную формулу. Все системы, обсуждаемые в этой статье, надежны и полны. Они также разделяют свойство, позволяющее эффективно проверить, что предположительно действительный вычет на самом деле является вычетом; такие системы дедукции называются эффективными .
Ключевым свойством дедуктивных систем является то, что они являются чисто синтаксическими, так что выводы могут быть проверены без рассмотрения какой-либо интерпретации. Таким образом, здравый аргумент является правильным во всех возможных интерпретациях языка, независимо от того, относится ли эта интерпретация к математике, экономике или какой-либо другой области.
В целом логическое следствие в логике первого порядка является только полуразрешимым : если предложение A логически подразумевает предложение B, то это можно обнаружить (например, путем поиска доказательства до тех пор, пока один найден с использованием какой-либо эффективной, надежной и полной системы доказательств). Однако, если A логически не подразумевает B, это не означает, что A логически подразумевает отрицание B. Не существует эффективной процедуры, которая с учетом формул A и B всегда правильно решала, следует ли A логически B.
A правило вывода гласит, что, учитывая конкретную формулу (или набор формул) с определенным свойством в качестве гипотезы, другая конкретная формула (или набор формул) может быть получена как заключение. Правило является здравым (или сохраняющим истину), если оно сохраняет действительность в том смысле, что всякий раз, когда любая интерпретация удовлетворяет гипотезе, эта интерпретация также удовлетворяет заключению.
Например, одним из общих правил вывода является правило подстановки . Если 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 и универсальное обобщение.
Естественные системы дедукции напоминают системы гильбертова в том смысле, что дедукция - это конечный список формул. Однако системы естественной дедукции не имеют логических аксиом; они компенсируют это, добавляя дополнительные правила вывода, которые можно использовать для манипулирования логическими связками в формулах в доказательстве.
Исчисление секвенций было разработано для изучения свойств систем естественного вывода. Вместо того, чтобы работать с одной формулой за раз, он использует секвенции, которые являются выражениями формы
где A 1,..., A n, B 1,..., B k - формулы, а символ турникета используется в качестве знаков препинания для разделите две половинки. Интуитивно секвенция выражает идею, что подразумевает .
В отличие от только что описанных методов, выводы в методе таблиц не являются списками формул. Вместо этого вывод - это дерево формул. Чтобы показать, что формула A доказуема, метод таблиц пытается продемонстрировать, что отрицание A неудовлетворительно. Дерево деривации имеет в корне ; дерево разветвляется таким образом, чтобы отражать структуру формулы. Например, чтобы показать, что является неудовлетворительным, необходимо показать, что C и D оба являются неудовлетворительными; это соответствует точке ветвления в дереве с родительским элементом и дочерними элементами C и D.
Правило разрешения - это единое правило вывода, которое вместе с объединением является правильным и полным для логики первого порядка. Как и в случае с методом таблиц, формула доказывается, показывая, что отрицание формулы невыполнимо. Разрешение обычно используется в автоматическом доказательстве теорем.
Метод разрешения работает только с формулами, которые являются дизъюнкциями атомарных формул; произвольные формулы сначала необходимо преобразовать в эту форму посредством сколемизации. Правило разрешения гласит, что из гипотез и , заключение получить можно.
Многие тождества могут быть доказаны, что устанавливает эквивалентность между конкретными формулами. Эти тождества позволяют переупорядочивать формулы, перемещая кванторы по другим связкам, и полезны для помещения формул в предваряющую нормальную форму. Некоторые доказуемые тождества включают:
Существует несколько различных соглашений для использования равенства (или идентичность) в логике первого порядка. Наиболее распространенное соглашение, известное как логика первого порядка с равенством, включает в себя символ равенства как примитивный логический символ, который всегда интерпретируется как реальное отношение равенства между членами предметной области, например " два "заданных члена являются одним и тем же членом. Этот подход также добавляет некоторые аксиомы о равенстве к применяемой дедуктивной системе. Эти аксиомы равенства:
Это схемы аксиом, каждая из которых определяет бесконечный набор аксиом. Третья схема известна как закон Лейбница, «принцип заместительности», «неразличимость тождественных» или «свойство замещения». Вторая схема, включающая функциональный символ f, является (эквивалентна) частным случаем третьей схемы с использованием формулы
Многие другие свойства равенства являются следствием вышеприведенных аксиом, например:
В альтернативном подходе отношение равенства рассматривается как нелогический символ. Это соглашение известно как логика первого порядка без равенства . Если в сигнатуре включено отношение равенства, аксиомы равенства теперь должны быть добавлены к рассматриваемым теориям, если это необходимо, вместо того, чтобы считаться правилами логики. Основное различие между этим методом и логикой первого порядка с равенством состоит в том, что интерпретация теперь может интерпретировать двух различных индивидов как «равных» (хотя, согласно закону Лейбница, они будут удовлетворять точно таким же формулам при любой интерпретации). То есть отношение равенства теперь может быть интерпретировано произвольным отношением эквивалентности в области дискурса, которое конгруэнтно по отношению к функциям и отношениям интерпретации.
Когда соблюдается это второе соглашение, термин нормальная модель используется для обозначения интерпретации, в которой никакие отдельные индивиды a и b не удовлетворяют a = b. В логике первого порядка с равенством рассматриваются только нормальные модели, поэтому для модели нет другого термина, кроме нормальной модели. Когда изучается логика первого порядка без равенства, необходимо изменить формулировки результатов, такие как теорема Лёвенгейма – Сколема, чтобы рассматривались только нормальные модели.
Логика первого порядка без равенства часто используется в контексте арифметики второго порядка и других теорий арифметики более высокого порядка, где отношение равенства между наборами натуральных чисел обычно опускается..
Если теория имеет бинарную формулу A (x, y), которая удовлетворяет рефлексивности и закону Лейбница, считается, что теория имеет равенство или является теорией. с равенством. Теория может иметь не все примеры вышеупомянутых схем как аксиомы, а скорее как выводимые теоремы. Например, в теориях без функциональных символов и конечного числа отношений можно определить равенство в терминах отношений, определив два члена s и t равными, если какое-либо отношение не изменилось. заменив s на t в любом аргументе.
Некоторые Теории допускают другие специальные определения равенства:
Одна из причин для использования логики первого порядка, а не логики высшего порядка, заключается в том, что логика первого порядка имеет множество металогических свойств, которые сильнее логики не иметь. Эти результаты касаются общих свойств самой логики первого порядка, а не свойств отдельных теорий. Они предоставляют фундаментальные инструменты для построения моделей теорий первого порядка.
Теорема Гёделя, доказанная Куртом Гёделем в 1929 году, устанавливает, что существуют надежные, полные, эффективные дедуктивные системы для логики первого порядка, и таким образом, отношение логического следствия первого порядка охвачено конечной доказуемостью. Наивно, утверждение, что формула φ логически влечет за собой формулу ψ, зависит от каждой модели φ; эти модели, как правило, будут иметь произвольно большую мощность, и поэтому логическое следствие не может быть эффективно проверено путем проверки каждой модели. Однако можно перечислить все конечные дифференцирования и найти вывод ψ из φ. Если ψ логически следует из φ, такой вывод в конечном итоге будет найден. Таким образом, логическое следствие первого порядка полуразрешимо : возможно произвести эффективное перечисление всех пар предложений (φ, ψ), так что ψ является логическим следствием φ.
В отличие от логики высказываний, логика первого порядка неразрешима (хотя и полуразрешима) при условии, что в языке есть хотя бы один предикат арности не менее 2 (кроме равенство). Это означает, что не существует процедуры принятия решения, которая определяет, являются ли произвольные формулы логически действительными. Этот результат был независимо установлен Алонзо Черч и Аланом Тьюрингом в 1936 и 1937 годах соответственно, дав отрицательный ответ на Entscheidungsproblem, поставленный Дэвидом Гильбертом. и Вильгельм Аккерман в 1928 году. Их доказательства демонстрируют связь между неразрешимостью проблемы решения для логики первого порядка и неразрешимостью проблемы остановки.
Существуют системы слабее, чем полная логика первого порядка, для которой разрешимо отношение логических следствий. К ним относятся логика высказываний и монадическая логика предикатов, которая представляет собой логику первого порядка, ограниченную унарными предикатными символами и отсутствием функциональных символов. Другие логические схемы без функциональных символов, которые могут быть разрешены, - это защищенный фрагмент логики первого порядка, а также логика с двумя переменными. Класс Бернейса – Шёнфинкеля формул первого порядка также разрешим. Разрешаемые подмножества логики первого порядка также изучаются в рамках логики описания.
Теорема Левенхайма – Сколема показывает, что если первая- теория порядка мощности λ имеет бесконечную модель, тогда у нее есть модели каждой бесконечной мощности, большей или равной λ. Один из самых ранних результатов в теории моделей, он подразумевает, что невозможно охарактеризовать счетность или несчетность в языке первого порядка с помощью счетной сигнатуры. То есть не существует формулы первого порядка φ (x) такой, что произвольная структура M удовлетворяет φ тогда и только тогда, когда область дискурса M счетна (или, во втором случае, несчетна).
Теорема Лёвенгейма – Сколема означает, что бесконечные структуры не могут быть категорично аксиоматизированы в логике первого порядка. Например, не существует теории первого порядка, единственной моделью которой является действительная линия: любая теория первого порядка с бесконечной моделью также имеет модель мощности, превышающей континуум. Поскольку действительная прямая бесконечна, любая теория, которой удовлетворяет действительная прямая, также удовлетворяется некоторыми нестандартными моделями. Когда теорема Левенгейма – Сколема применяется к теориям множеств первого порядка, неинтуитивные следствия известны как парадокс Сколема.
Теорема компактности утверждает, что в наборе предложений первого порядка есть модель тогда и только тогда, когда у каждого конечного подмножества есть модель. Это означает, что если формула является логическим следствием бесконечного набора аксиом первого порядка, то она является логическим следствием некоторого конечного числа этих аксиом. Эта теорема была впервые доказана Куртом Гёделем как следствие теоремы о полноте, но со временем было получено множество дополнительных доказательств. Это центральный инструмент в теории моделей, обеспечивающий фундаментальный метод построения моделей.
Теорема компактности оказывает ограничивающее влияние на то, какие наборы структур первого порядка являются элементарными классами. Например, из теоремы компактности следует, что любая теория, имеющая сколь угодно большие конечные модели, имеет бесконечную модель. Таким образом, класс всех конечных графов не является элементарным классом (то же самое верно для многих других алгебраических структур).
Существуют также более тонкие ограничения логики первого порядка, которые подразумевает теорема компактности. Например, в информатике многие ситуации могут быть смоделированы как ориентированный граф состояний (узлов) и соединений (направленных ребер). Проверка такой системы может потребовать демонстрации того, что «плохое» состояние не может быть достигнуто из любого «хорошего» состояния. Таким образом, нужно определить, находятся ли хорошее и плохое состояния в разных связанных компонентах графа. Однако теорема компактности может использоваться, чтобы показать, что связные графы не являются элементарным классом в логике первого порядка, и что нет формулы φ (x, y) логики первого порядка в логике графов., который выражает идею о том, что существует путь от x до y. Связность может быть выражена в логике второго порядка, однако, но не только с помощью кванторов экзистенциального множества, как также отличается компактностью.
Пер Линдстрём показала, что только что обсужденные металогические свойства фактически характеризуют логику первого порядка в том смысле, что никакая более сильная логика не может обладать этими свойствами (Ebbinghaus and Flum 1994, Chapter XIII). Линдстрем определил класс абстрактных логических систем и строго определил относительную силу члена этого класса. Он установил две теоремы для систем этого типа:
Хотя логики первого порядка достаточно для формализации большая часть математики и обычно используется в информатике и других областях, но имеет определенные ограничения. К ним относятся ограничения на его выразительность и ограничения фрагментов естественных языков, которые он может описывать.
Например, логика первого порядка неразрешима, что означает невозможность создания надежного, полного и завершающего алгоритма принятия решения для доказуемости. Это привело к изучению интересных разрешимых фрагментов, таких как C 2 : логика первого порядка с двумя переменными и счетные кванторы и .
Теорема Левенгейма – Сколема показывает, что если теория первого порядка имеет любую бесконечную модель, то у нее есть бесконечные модели любой мощности. В частности, никакая теория первого порядка с бесконечной моделью не может быть категоричной. Таким образом, не существует теории первого порядка, единственная модель которой имеет набор натуральных чисел в качестве области применения или единственная модель которой имеет набор действительных чисел в качестве области определения. Многие расширения логики первого порядка, включая бесконечные логики и логики более высокого порядка, более выразительны в том смысле, что они допускают категориальную аксиоматизацию натуральных или действительных чисел. Эта выразительность, однако, имеет металогическую цену: согласно теореме Линдстрёма теорема компактности и нисходящая теорема Левенгейма – Сколема не могут выполняться ни в одной логике более сильной, чем первый порядок.
Логика первого порядка способна формализовать многие простые конструкции кванторов на естественном языке, например, «каждый человек, живущий в Перте, живет в Австралии». Но есть гораздо более сложные особенности естественного языка, которые нельзя выразить в (односортированной) логике первого порядка. «Любая логическая система, подходящая в качестве инструмента для анализа естественного языка, требует гораздо более богатой структуры, чем логика предикатов первого порядка».
Тип | Пример | Комментарий |
---|---|---|
Количественная оценка по свойствам | Если Джон удовлетворен собой, то есть по крайней мере одна общая черта, которую он имеет с Питером. | В примере требуется квантификатор по предикатам, который не может быть реализовано в односортированной логике первого порядка: Zj → ∃X (Xj∧Xp). |
Количественная оценка по свойствам | Санта-Клаус обладает всеми атрибутами садиста. | В примере требуются квантификаторы по предикатам, что не может быть реализовано в односортированной логике первого порядка: ∀X ( ∀x (Sx → Xx) → Xs). |
Предикатное наречие | Джон идет быстро. | Пример не может быть проанализирован как Wj ∧ Qj; наречия предикатов - это не то же самое, что предикаты второго порядка, такие как цвет. |
Относительное прилагательное | Джамбо - маленький слон. | Пример не может быть проанализирован как Sj ∧ Ej; Предикатные прилагательные - это не то же самое, что предикаты второго порядка, такие как цвет. |
Предикатный модификатор наречия | Джон ходит очень быстро. | - |
Модификатор относительного прилагательного | Джамбо ужасно мал. | Такое выражение, как «ужасно», когда применяется к относительному прилагательному, например, «маленький», дает новое составное относительное прилагательное «ужасно маленький». |
Предложения | Мэри сидит рядом с Джоном. | Предлог «рядом с», примененный к «Джону», дает предикатное наречие «рядом с Джоном». |
Существует множество вариантов логики первого порядка. Некоторые из них несущественны в том смысле, что они просто изменяют нотацию, не затрагивая семантику. Другие изменяют выразительную силу более значительно, расширяя семантику за счет дополнительных квантификаторов или других новых логических символов. Например, бесконечная логика допускает формулы бесконечного размера, а модальная логика добавляет символы возможности и необходимости.
Логику первого порядка можно изучать на языках с меньшим количеством логических символов, чем описано выше.
Подобные ограничения полезны в качестве метода уменьшения количества правил вывода или схем аксиом в дедуктивных системах, что приводит к более коротким доказательствам металогических результатов. Цена ограничений состоит в том, что становится труднее выражать утверждения на естественном языке в имеющейся формальной системе, потому что логические связки, используемые в операторах естественного языка, должны быть заменены их (более длинными) определениями в терминах ограниченного набора логические связки. Точно так же производные в ограниченных системах могут быть длиннее, чем производные в системах, которые включают дополнительные связки. Таким образом, существует компромисс между простотой работы в рамках формальной системы и легкостью доказательства результатов. о формальной системе.
Также возможно ограничить арность функциональных символов и предикатных символов в достаточно выразительных теориях. В принципе, можно полностью отказаться от функций арности больше 2 и предикатов арности больше 1 в теориях, которые включают функцию спаривания . Это функция арности 2, которая принимает пары элементов домена и возвращает упорядоченную пару, содержащую их. Также достаточно иметь два предикатных символа арности 2, которые определяют функции проекции упорядоченной пары на ее компоненты. В любом случае необходимо, чтобы выполнялись естественные аксиомы для функции спаривания и ее проекций.
Обычные интерпретации первого порядка имеют единую область дискурса, в пределах которой располагаются все кванторы. Многосортная логика первого порядка позволяет переменным иметь разные сортировки, которые имеют разные домены. Это также называется типизированной логикой первого порядка, а сортировки - типами (как в типе данных ), но это не то же самое, что и логика первого порядка. теория типов. Многосортированная логика первого порядка часто используется при изучении арифметики второго порядка.
Когда в теории есть только конечное число сортировок, многосортированная логика первого порядка может быть сведена к единственной сортировке сначала - логика заказа. Один вводит в теорию единственной сортировки унарный предикатный символ для каждого вида в теории множественной сортировки и добавляет аксиому, говорящую, что эти унарные предикаты разделяют область дискурса. Например, при двух сортировках добавляются символы предиката и и аксиома
Тогда элементы, удовлетворяющие , рассматриваются как элементы первого сорта, а элементы, удовлетворяющие как элементы второго сорта. Можно произвести количественную оценку по каждой сортировке, используя соответствующий символ предиката, чтобы ограничить диапазон количественной оценки. Например, чтобы сказать, что существует элемент первого сорта, удовлетворяющий формуле φ (x), пишут
Дополнительные кванторы могут быть добавлены к логике первого порядка.
Бесконечная логика допускает бесконечно длинные предложения. Например, можно разрешить конъюнкцию или дизъюнкцию бесконечного количества формул или количественную оценку по бесконечному количеству переменных. Бесконечно длинные предложения возникают в таких областях математики, как топология и теория моделей.
Бесконечно длинная логика обобщает логику первого порядка, позволяя формулам бесконечной длины. Самый распространенный способ превращения формул в бесконечность - бесконечные союзы и дизъюнкции. Однако также возможно допустить обобщенные сигнатуры, в которых символы функций и отношений могут иметь бесконечное число арностей или в которых кванторы могут связывать бесконечно много переменных. Поскольку бесконечная формула не может быть представлена конечной строкой, необходимо выбрать какое-то другое представление формул; обычное представление в этом контексте - дерево. Таким образом, формулы, по сути, отождествляются с их деревьями синтаксического анализа, а не с анализируемыми строками.
Наиболее часто изучаемые инфинитарные логики обозначаются L αβ, где α и β каждое - либо кардинальные числа, либо символ ∞. В этих обозначениях обычная логика первого порядка - это L ωω. В логике L ∞ω при построении формул разрешены произвольные конъюнкции или дизъюнкции, и существует неограниченный запас переменных. В более общем смысле логика, которая допускает соединения или дизъюнкции с менее чем κ составляющими, известна как L κω. Например, L ω1ωдопускает счетные союзы и дизъюнкции.
Набор свободных переменных в формуле L κω может иметь любую мощность, строго меньшую, чем κ, но только конечное число из них может быть в области действия любого квантора, когда формула появляется как подформула другого. В других инфинитарных логиках подформула может находиться в области бесконечности у многих кванторов. Например, в L κ∞ один универсальный или экзистенциальный квантор может одновременно связывать произвольно много переменных. Точно так же логика L κλ допускает одновременную количественную оценку менее чем λ переменных, а также конъюнкций и дизъюнкций размером меньше κ.
Логика фиксированных точек расширяет логику первого порядка, добавляя замыкание по наименьшему количеству фиксированных точек положительных операторов.
Характерной чертой логики первого порядка является то, что можно количественно оценить индивидов, но не предикаты. Таким образом,
является допустимой формулой первого порядка, но
не является в большинстве формализаций логики первого порядка. Логика второго порядка расширяет логику первого порядка, добавляя последний тип количественной оценки. Другие логики более высокого порядка допускают количественную оценку по даже более высоким типам, чем позволяет логика второго порядка. Эти более высокие типы включают отношения между отношениями, функции от отношений к отношениям между отношениями и другие объекты более высокого типа. Таким образом, «первый» в логике первого порядка описывает тип объектов, которые могут быть определены количественно.
В отличие от логики первого порядка, для которой изучается только одна семантика, существует несколько возможных семантик для логики второго порядка. Наиболее часто используемая семантика для логики второго и высшего порядка известна как полная семантика . Комбинация дополнительных кванторов и полной семантики для этих кванторов делает логику более высокого порядка более сильной, чем логику первого порядка. В частности, (семантическое) отношение логических последствий для логики второго и более высокого порядка не является полуразрешимым; не существует эффективной системы дедукции для логики второго порядка, которая была бы правильной и полной в рамках полной семантики.
Логика второго порядка с полной семантикой более выразительна, чем логика первого порядка. Например, можно создать системы аксиом в логике второго порядка, которые однозначно характеризуют натуральные числа и действительную линию. Цена этой выразительности состоит в том, что логики второго и более высокого порядка обладают меньшим количеством привлекательных металогических свойств, чем логика первого порядка. Например, теорема Левенгейма – Сколема и теорема компактности логики первого порядка становятся ложными при обобщении на логики более высокого порядка с полной семантикой.
Автоматическое доказательство теорем относится к разработке компьютерных программ, которые ищут и находят выводные (формальные доказательства) математических теорем. Поиск производных - сложная задача, поскольку пространство поиска может быть очень большим; исчерпывающий поиск всех возможных выводов теоретически возможен, но вычислительно невозможен для многих систем, представляющих интерес в математике. Таким образом, сложные эвристические функции разрабатываются, чтобы попытаться найти вывод за меньшее время, чем слепой поиск.
Связанная область автоматизированной проверки подтверждения использует компьютерные программы для проверки что доказательства, созданные человеком, верны. В отличие от сложных автоматических средств доказательства теорем, системы проверки могут быть достаточно маленькими, чтобы их правильность можно было проверить как вручную, так и с помощью автоматической проверки программного обеспечения. Эта проверка верификатора доказательства необходима, чтобы дать уверенность в том, что любой вывод, помеченный как «правильный», действительно правильный.
Некоторые средства проверки доказательств, такие как Metamath, настаивают на том, чтобы вывод в качестве входа. Другие, такие как Мицар и Изабель, берут хорошо отформатированный эскиз корректуры (который может быть очень длинным и подробным) и заполняют недостающие части, выполняя простой поиск корректуры или применяя известные процедуры принятия решений: полученный результат затем проверяется небольшим ядром ядра. Многие такие системы в первую очередь предназначены для интерактивного использования математиками-людьми: они известны как помощники по доказательству. Они также могут использовать формальные логики, которые сильнее логики первого порядка, например теорию типов. Поскольку полный вывод любого нетривиального результата в дедуктивной системе первого порядка будет чрезвычайно долгим для написания человеком, результаты часто формализуются в виде серии лемм, для которых выводы могут быть построены отдельно.
Автоматические средства доказательства теорем также используются для реализации формальной проверки в информатике. В этом случае средства доказательства теорем используются для проверки правильности программ и оборудования, такого как процессоры, по отношению к формальной спецификации. Поскольку такой анализ требует много времени и, следовательно, дорого, его обычно оставляют для проектов, в которых сбой имел бы серьезные человеческие или финансовые последствия.
Для задачи проверки модели известны эффективные алгоритмы, которые решают, удовлетворяет ли входная конечная структура формуле первого порядка, в дополнение к вычислительной сложности границы: см. Проверка модели # Логика первого порядка.