Логика первого порядка - First-order logic

Логика первого порядка, также известная как логика предикатов , квантификационная логика и исчисление предикатов первого порядка , представляет собой набор формальных систем, используемых в математике , философии , лингвистике и информатике . Логика первого порядка использует количественные переменные над нелогическими объектами и позволяет использовать предложения, содержащие переменные, так что вместо предложений типа «Сократ - человек» можно иметь выражения в форме «существует x такое, что x - это Сократ, а x - это человек », где« существует » - это квантор, а x - переменная. Это отличает ее от логики высказываний , которая не использует кванторы или отношения ; в этом смысле логика высказываний является основой логики первого порядка.

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

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

Существует множество дедуктивных систем для логики первого порядка, которые являются как правильными (т. Е. Все доказуемые утверждения верны во всех моделях), так и полными (т. Е. Все утверждения, которые истинны во всех моделях, доказуемы). Хотя отношение логического следствия является лишь полуразрешимым , большой прогресс был достигнут в автоматизированном доказательстве теорем в логике первого порядка. Первый порядок логики также удовлетворяет несколько металогических теорем , которые делают его доступным для анализа в теории доказательств , такие , как теорема Löwenheim-сколемовской и теорема компактности .

Логика первого порядка является стандартом для формализации математики в аксиомы и изучается в основах математики . Арифметика Пеано и теория множеств Цермело – Френкеля представляют собой аксиоматизацию теории чисел и теории множеств , соответственно, в логику первого порядка. Однако никакая теория первого порядка не способна однозначно описать структуру с бесконечной областью, такой как натуральные числа или действительная линия . Системы аксиом, которые полностью описывают эти две структуры (то есть категориальные системы аксиом), могут быть получены в более сильных логиках, таких как логика второго порядка .

Основы логики первого порядка были независимо разработаны Готлобом Фреге и Чарльзом Сандерсом Пирсом . Об истории логики первого порядка и о том, как она стала доминировать в формальной логике, см. José Ferreirós (2001).

Вступление

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

Предикат принимает в качестве входных данных сущность или сущности из предметной области, в то время как выходы имеют значение Истина или Ложь . Рассмотрим два предложения: «Сократ - философ» и «Платон - философ». В логике высказываний эти предложения рассматриваются как несвязанные друг с другом и могут быть обозначены, например, такими переменными, как p и q . Предикат «является философом» встречается в обоих предложениях, которые имеют общую структуру « а является философом». Переменная a представлена ​​как «Сократ» в первом предложении и как «Платон» во втором предложении. В то время как логика первого порядка допускает использование предикатов, таких как «является философом» в этом примере, логика высказываний - нет.

Отношения между предикатами можно установить с помощью логических связок . Рассмотрим, например, формулу первого порядка «если а - философ, то а - ученый». Эта формула является условным утверждением с гипотезой « а - философ» и выводом « а - ученый». Истинность этой формулы зависит от того, какой объект обозначается символом a , и от интерпретаций предикатов «философ» и «ученый».

Кванторы можно применять к переменным в формуле. Переменная а в предыдущей формуле может быть универсально определена количественно, например, с помощью предложения первого порядка: «Для каждого а , если а - философ, то а - ученый». Квантор «для каждого» в этом предложении высказывает мысль о том , что требование « если философ, то является ученым» имеет место для всех выборов .

Отрицание приговора «Для каждого а , если философ, то является ученым» логически эквивалентна фразе «Там существует такое , что философ и не ученый». Экзистенциальный квантор «существует» выражает идею о том , что требование « философ и не ученый» имеет место для какого - то выбора .

Каждый из предикатов «философ» и «ученый» принимает одну переменную. Как правило, предикаты могут принимать несколько переменных. В предложении первого порядка «Сократ - учитель Платона» сказуемое «является учителем» принимает две переменные.

Интерпретация (или модель) формулы первого порядка определяет, что означает каждый предикат, и сущности, которые могут создавать экземпляры переменных. Эти сущности образуют область дискурса или вселенную, которая обычно должна быть непустым множеством. Например, в интерпретации с областью речи , состоящей из всех человеческих существ и предикатом «философ» понимается как «был автор Республики », в предложении «Там существует такие , что философ» видно как истинное, как засвидетельствовано Платоном.

Синтаксис

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

Алфавит

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

Обычно символы алфавита делятся на логические символы , которые всегда имеют одно и то же значение, и нелогические символы , значение которых зависит от интерпретации. Например, логический символ всегда представляет собой «и»; оно никогда не интерпретируется как «или», которое представлено логическим символом . С другой стороны, нелогический предикатный символ, такой как Phil ( x ), можно интерпретировать как означающий « x - философ», « x - человек по имени Филипп» или любой другой унарный предикат в зависимости от рассматриваемой интерпретации.

Логические символы

В алфавите есть несколько логических символов, которые различаются в зависимости от автора, но обычно включают:

  • В кванторных символах: для универсальной квантификации и для экзистенциальной квантификации
  • В логические связки : для связи , для дизъюнкции , для импликации , для biconditional , ¬ для отрицания. Иногда используются другие логические соединительные символы. Некоторые авторы используют C pq вместо и E pq вместо , особенно в контекстах, где → используется для других целей. Кроме того, подкова может заменять ; тройка может заменить ; тильда ( ~ ), N p или F p может заменять ¬ ; двойная полоса , или A pq может заменить ; и амперсанд & , K pq или средняя точка ,, могут заменять , особенно если эти символы недоступны по техническим причинам. (Вышеупомянутые символы C pq , E pq , N p , A pq и K pq используются в польской системе обозначений .)
  • Скобки, квадратные скобки и другие знаки препинания. Выбор таких символов варьируется в зависимости от контекста.
  • Бесконечный набор переменных , часто обозначаемых строчными буквами в конце алфавита x , y , z , .... Индексы часто используются для различения переменных: x 0 , x 1 , x 2 , ....
  • Символ равенства (иногда, символ идентичности ) = (см § равенства и его аксиомы ниже).

Не все эти символы требуются - достаточно только одного из кванторов, отрицания и конъюнкции, переменных, скобок и равенства. Есть множество незначительных вариаций, которые могут определять дополнительные логические символы:

  • В некоторых случаях, константа истинности T, V PQ , или , для "истинного" и F, O рда или , для "ложного" включена. Без таких логических операторов валентности 0 эти две константы можно выразить только с помощью кванторов.
  • В других случаях включаются дополнительные логические связки, такие как штрих Шеффера , D pq (И-НЕ) и исключающее или , J pq .

Нелогические символы

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

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

  1. Для любого целого п  ≥ 0, существует совокупность п - ичная или п - место , предикатные символы . Поскольку они представляют отношения между n элементами, их также называют символами отношений . Для каждой арности n у нас их бесконечное количество:
    P n 0 , P n 1 , P n 2 , P n 3 , ...
  2. Для любого целого n  ≥ 0 существует бесконечное количество n -арных функциональных символов :
    f n 0 , f n 1 , f n 2 , f n 3 , ...

В современной математической логике подпись меняется в зависимости от приложения. Типичные сигнатуры в математике: {1, ×} или просто {×} для групп или {0, 1, +, ×, <} для упорядоченных полей . Нет ограничений на количество нелогических символов. Подпись может быть пустой , конечной или бесконечной, даже неисчислимой . Бесчисленные подписи встречаются, например, в современных доказательствах теоремы Левенгейма – Сколема .

В этом подходе каждый нелогический символ относится к одному из следующих типов.

  1. Предикатный символ (или символ отношения ) с некоторой валентностью (или арностью , число аргументов) больше или равно 0. Они часто обозначаются заглавными буквами , такие как P , Q и R .
    • Отношения валентности 0 можно отождествить с пропозициональными переменными . Например, P , которое может означать любое утверждение.
    • Например, P ( x ) - это предикатная переменная валентности 1. Одна из возможных интерпретаций - « x - мужчина».
    • Q ( x , y ) - предикатная переменная валентности 2. Возможные интерпретации включают « x больше, чем y » и « x является отцом y ».
  2. Символ функции , с некоторой валентной больше или равно 0. Они часто обозначаются строчными латинскими буквами , таких как ф , г и ч .
    • Примеры: f ( x ) можно интерпретировать как «отец x ». В арифметике это может означать «-x». В теории множеств это может означать « набор степеней x». В арифметике g ( x , y ) может означать « x + y ». В теории множеств это может означать «объединение x и y ».
    • Функциональные символы валентности 0 называются постоянными символами и часто обозначаются строчными буквами в начале алфавита, такими как a , b и c . Символ a может означать Сократа. В арифметике это может означать 0. В теории множеств такая константа может обозначать пустое множество .

Традиционный подход может быть восстановлен в современном подходе, просто указав «заказную» подпись, состоящую из традиционных последовательностей нелогических символов.

Правила формирования

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

Условия

Множество терминов является индуктивно определяется следующими правилами:

  1. Переменные. Любая переменная - это термин.
  2. Функции. Любое выражение f ( t 1 , ..., t n ) из n аргументов (где каждый аргумент t i является термом, а f - функциональным символом валентности n ) является термом. В частности, символы, обозначающие отдельные константы, являются нулевыми функциональными символами и, следовательно, являются терминами.

Терминами являются только выражения, которые можно получить конечным числом применений правил 1 и 2. Например, никакое выражение, содержащее символ предиката, не является термином.

Формулы

Набор формул (также называемых правильно сформированными формулами или WFF ) индуктивно определяется следующими правилами:

  1. Предикатные символы. Если P является n- мерным предикатным символом и t 1 , ..., t n являются термами, то P ( t 1 , ..., t n ) является формулой.
  2. Равенство . Если символ равенства считается частью логики, а t 1 и t 2 являются членами, то t 1 = t 2 является формулой.
  3. Отрицание. Если это формула, то это формула.
  4. Бинарные связки. Если и являются формулами, то ( ) является формулой. Подобные правила применяются к другим двоичным логическим связкам.
  5. Квантификаторы. Если - формула, а x - переменная, то (для всех x выполняется) и (существует x такой, что ) являются формулами.

Формулами являются только выражения, которые можно получить конечным числом применений правил 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 входит в φ, если и только если x входит в φ . Более того, ни в одной атомарной формуле нет связанных переменных.
Отрицание
x появляется свободным в ¬ φ тогда и только тогда, когда x встречается свободным в φ . x встречается связанной в ¬ φ тогда и только тогда, когда x встречается в φ
Бинарные связки
x появляется свободным в ( φψ ) тогда и только тогда, когда x встречается свободно либо в φ, либо в ψ . x встречается связанной в ( φψ ) тогда и только тогда, когда x встречается связанной либо в φ, либо в ψ . То же правило применяется к любой другой двоичной связке вместо →.
Квантификаторы
х происходит свободно в у ф , тогда и только тогда , когда х происходит свободно в ф и х представляет собой другой символ из г . Кроме того, x встречается связанным в y φ тогда и только тогда, когда x равен y или x встречается связанным в φ . То же правило с вместо .

Например, в ху ( Р ( х ) → Q ( х , е ( х ), г )) , х и у происходят только связаны, г происходит только свободно, и ш не является ни , потому что это не происходит в формула.

Свободные и связанные переменные формулы не обязательно должны быть непересекающимися множествами: в формуле 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 .

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

Семантика

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

Область дискурса D - это непустое множество «объектов» определенного вида. Интуитивно формула первого порядка - это утверждение об этих объектах; например, заявляет о существовании такого объекта x , что предикат P истинен там, где он упоминается. Область дискурса - это совокупность рассматриваемых объектов. Например, можно принять набор целых чисел.

Интерпретация символа функции - это функция. Например, если область дискурса состоит из целых чисел, функциональный символ f арности 2 можно интерпретировать как функцию, которая дает сумму своих аргументов. Другими словами, символ f связан с функцией, которая в этой интерпретации является сложением.

Интерпретация постоянного символа является функцией от заданного одного элемента D 0 до D , которые могут быть просто определены с объектом в D . Например, интерпретация может присвоить значение постоянному символу .

Интерпретация n -арного предикатного символа - это набор n - кортежей элементов предметной области дискурса. Это означает, что, учитывая интерпретацию, предикатный символ и n элементов области дискурса, можно сказать, является ли предикат истинным для этих элементов в соответствии с данной интерпретацией. Например, интерпретация I (P) двоичного символа предиката P может быть набором пар целых чисел, так что первое меньше второго. Согласно этой интерпретации, предикат P будет истинным, если его первый аргумент меньше второго.

Структуры первого порядка

Наиболее распространенный способ определения интерпретации (особенно в математике) - это указать структуру (также называемую моделью ; см. Ниже). Структура состоит из непустого множества D , образующего область дискурса, и интерпретации I нелогических терминов подписи. Эта интерпретация сама по себе является функцией:

  • Каждый символ функции F арности п присваивается функция от до D . В частности, каждому постоянному символу подписи присваивается индивидуум в предметной области.
  • Каждый предикат символ Р арности п присваивается отношение над или, что эквивалентно, функцией от до . Таким образом , каждый предикат символ интерпретируется булевозначной функцией на D .

Оценка истинности ценностей

Формула оценивается как истинная или ложная с учетом интерпретации и присвоения переменной μ, которое связывает элемент предметной области с каждой переменной. Причина, по которой требуется присвоение переменной, состоит в том, чтобы придать значение формулам со свободными переменными, например . Значение истинности этой формулы меняется в зависимости от того, обозначают ли x и y одного и того же человека.

Во-первых, присвоение переменной μ может быть расширено на все термины языка, в результате чего каждый термин отображается на отдельный элемент предметной области. Для выполнения этого задания используются следующие правила:

  1. Переменные. Каждая переменная x оценивается как μ ( x )
  2. Функции. Учитывая термины , которые были оценены как элементы предметной области, и n- мерный функциональный символ f , этот термин оценивается как .

Затем каждой формуле присваивается значение истинности. Индуктивное определение, используемое для этого назначения, называется T-схемой .

  1. Атомарные формулы (1). С формулой связано значение истина или ложь в зависимости от того , где находятся оценка терминов и интерпретация , которая по предположению является подмножеством .
  2. Атомарные формулы (2). Формула присваивается верно , если и оценить тот же объект домена дискурса (см раздел равенства ниже).
  3. Логические связки. Формула в форме , и т.д. оценивается в соответствии с таблицей истинности для связки в вопросе, как и в логике высказываний.
  4. Экзистенциальные кванторы. Формула истинна согласно M и если существует оценка переменных, которая отличается только от оценки x и такая, что φ истинно согласно интерпретации M и присвоению переменной . Это формальное определение отражает идею, которая истинна тогда и только тогда, когда есть способ выбрать значение для x, такое, что φ ( x ) удовлетворяется.
  5. Универсальные кванторы. Формула истинна согласно M, и если φ ( x ) истинно для каждой пары, составленной посредством интерпретации M и некоторого присвоения переменной, которое отличается только от значения x . Это отражает идею, которая верна, если каждый возможный выбор значения для x заставляет φ ( x ) быть истинным.

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

Существует второй распространенный подход к определению значений истинности, который не полагается на функции присваивания переменных. Вместо этого, учитывая интерпретацию M , сначала к подписи добавляют набор постоянных символов, по одному для каждого элемента области дискурса в M ; говорят, что для каждого d в области постоянный символ c d фиксирован. Интерпретация расширяется так, что каждый новый постоянный символ присваивается соответствующему элементу домена. Теперь истина для количественных формул определяется синтаксически следующим образом:

  1. Кванторы существования (альтернативные). Формула истинна согласно M, если в области дискурса существует такое d , которое имеет место. Вот результат замены c d на каждое свободное вхождение x в φ.
  2. Универсальные кванторы (альтернативные). Формула верна в соответствии с М , если для каждого г в области речи, правда , по любому из M .

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

Валидность, выполнимость и логическое следствие

Если предложение φ оценивается как True при данной интерпретации M , говорят, что M удовлетворяет φ; это обозначено . Предложение считается выполнимым, если есть какое-то толкование, при котором оно истинно.

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

Формула является логически действительной (или просто действительной ), если она верна при любой интерпретации. Эти формулы играют роль, аналогичную тавтологиям в логике высказываний.

Формула φ является логическим следствием формулы ψ, если каждая интерпретация, делающая ψ истинным, также делает истинным φ. В этом случае говорят, что φ логически следует из ψ.

Алгебраизации

Альтернативный подход к семантике логики первого порядка исходит из абстрактной алгебры . Этот подход обобщает алгебры Линденбаума – Тарского логики высказываний. Есть три способа исключить количественные переменные из логики первого порядка, которые не включают замену кванторов другими операторами термов привязки переменных:

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

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

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

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

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

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

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

Для получения дополнительной информации по этому вопросу см. Список теорий первого порядка и теории (математическая логика).

Пустые домены

Приведенное выше определение требует, чтобы область дискурса любой интерпретации была непустой. Есть настройки, такие как инклюзивная логика , где разрешены пустые домены. Более того, если класс алгебраических структур включает в себя пустую структуру (например, есть пустой объектный набор ), этот класс может быть только элементарным классом в логике первого порядка, если разрешены пустые домены или пустая структура удалена из класса. .

Однако есть несколько трудностей с пустыми доменами:

  • Многие общие правила вывода действительны только тогда, когда требуется, чтобы область дискурса была непустой. Одним из примеров является правило о том , что означает , когда х не является свободной переменной в . Это правило, которое используется для преобразования формул в предваренную нормальную форму , работает в непустых доменах, но не работает, если пустой домен разрешен.
  • Определение истины в интерпретации, использующей функцию присваивания переменной, не может работать с пустыми доменами, потому что нет функций присваивания переменных, диапазон которых пуст. (Точно так же нельзя назначать интерпретации постоянным символам.) Это определение истинности требует, чтобы нужно было выбрать функцию присвоения переменной (μ выше) до того, как можно будет определить значения истинности даже для атомарных формул. Затем значение истинности предложения определяется как его значение истинности при любом присвоении переменной, и доказывается, что это значение истинности не зависит от того, какое присвоение выбрано. Этот метод не работает, если вообще нет функций присваивания; его необходимо изменить для размещения пустых доменов.

Таким образом, когда пустой домен разрешен, его часто следует рассматривать как особый случай. Однако большинство авторов просто исключают пустой домен по определению.

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

Дедуктивная система используется для демонстрации, на чисто синтаксической основе, что одна формула является логическим следствием другой формуле. Существует множество таких систем для логики первого порядка, включая дедуктивные системы гильбертовского стиля , естественную дедукцию , секвенциальное исчисление , метод таблиц и разрешение . У них есть общее свойство, заключающееся в том, что дедукция - это конечный синтаксический объект; формат этого объекта и способ его построения сильно различаются. Эти конечные выводы сами часто называют выкладки в теории доказательств. Их также часто называют доказательствами, но они полностью формализованы, в отличие от математических доказательств на естественном языке .

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

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

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

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

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

Например, одним из распространенных правил вывода является правило подстановки . Если 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 ∨ ¬b) ∧ b) → a.

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

разрешение

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

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

Подтверждаемые личности

Можно доказать многие тождества, которые устанавливают эквивалентность между конкретными формулами. Эти тождества позволяют переупорядочивать формулы, перемещая кванторы по другим связкам, и полезны для преобразования формул в предваренную нормальную форму . Некоторые доказуемые личности включают:

(где не должно быть свободного места )
(где не должно быть свободного места )

Равенство и его аксиомы

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

  1. Рефлексивность . Для каждой переменной х , х = х .
  2. Подмена функций. Для всех переменных х и у , и любого символа функции F ,
    x = yf (..., x , ...) = f (..., y , ...).
  3. Подстановка формул . Для любых переменных x и y и любой формулы φ ( x ), если φ 'получается заменой любого числа свободных вхождений x в φ на y , так что они остаются свободными вхождениями y , то
    x = y → (φ → φ ').

Это схемы аксиом , каждая из которых определяет бесконечный набор аксиом. Третья схема известна как закон Лейбница , «принцип подстановочности», «неразличимость тождественных» или «свойство замещения». Вторая схема, включающая функциональный символ f , является (эквивалентна) частным случаем третьей схемы с использованием формулы

x = y → ( f (..., x , ...) = z → f (..., y , ...) = z).

Многие другие свойства равенства являются следствием вышеприведенных аксиом, например:

  1. Симметрия. Если x = y, то y = x .
  2. Транзитивность. Если x = y и y = z, то x = z .

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

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

Когда соблюдается это второе соглашение, термин " нормальная модель" используется для обозначения интерпретации, в которой никакие отдельные индивиды a и b не удовлетворяют a = b . В логике первого порядка с равенством рассматриваются только нормальные модели, поэтому для модели нет другого термина, кроме нормальной модели. Когда изучается логика первого порядка без равенства, необходимо изменить формулировки результатов, такие как теорема Левенгейма – Сколема, так, чтобы рассматривались только нормальные модели.

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

Определение равенства в теории

Если в теории есть бинарная формула A ( x , y ), удовлетворяющая рефлексивности и закону Лейбница, то говорят, что теория имеет равенство или является теорией с равенством. Теория может иметь не все примеры вышеупомянутых схем как аксиомы, а скорее как выводимые теоремы. Например, в теориях без функциональных символов и с конечным числом отношений можно определить равенство в терминах отношений, определяя два члена s и t равными, если какое-либо отношение не изменяется, заменяя s на t в любой аргумент.

Некоторые теории допускают другие специальные определения равенства:

  • В теории частичных порядков с одним символом отношения ≤ можно определить s = t как сокращение для stts .
  • В теории множеств с одним отношением ∈ можно определить s = t как сокращение для x ( sxtx ) ∧ ∀ x ( xsxt ) . Тогда это определение равенства автоматически удовлетворяет аксиомам равенства. В этом случае следует заменить обычную аксиому экстенсиональности , которую можно сформулировать как альтернативную формулировку , которая гласит, что если множества x и y имеют одинаковые элементы, то они также принадлежат одним и тем же множествам.

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

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

Полнота и неразрешимость

Теорема Гёделя о полноте , доказанная Куртом Гёделем в 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 ), пишут

.

Дополнительные кванторы

К логике первого порядка могут быть добавлены дополнительные кванторы.

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

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

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

Бесконечная логика обобщает логику первого порядка, позволяя создавать формулы бесконечной длины. Самый распространенный способ превращения формул в бесконечность - бесконечные союзы и дизъюнкции. Однако также возможно допустить обобщенные сигнатуры, в которых символы функций и отношений могут иметь бесконечное количество арностей или в которых кванторы могут связывать бесконечно много переменных. Поскольку бесконечная формула не может быть представлена ​​конечной строкой, необходимо выбрать другое представление формул; обычное представление в этом контексте - дерево. Таким образом, формулы, по сути, отождествляются с их деревьями синтаксического анализа, а не с анализируемыми строками.

Наиболее часто изучаемые инфинитарные логики обозначаются L αβ , где α и β - либо кардинальные числа, либо символ ∞. В этих обозначениях обычная логика первого порядка - это L ωω . В логике L ∞ω при построении формул разрешены произвольные конъюнкции или дизъюнкции, и существует неограниченный запас переменных. В более общем смысле, логика, которая допускает конъюнкции или дизъюнкции с менее чем κ составляющими, известна как L κω . Например, L ω 1 ω допускает счетные конъюнкции и дизъюнкции.

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

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

  • Интуиционистская логика первого порядка использует интуиционистское, а не классическое исчисление высказываний; например, ¬¬φ не обязательно эквивалентно φ.
  • Модальная логика первого порядка позволяет описывать другие возможные миры, а также этот условно истинный мир, в котором мы живем. В некоторых версиях набор возможных миров варьируется в зависимости от того, в каком из возможных миров обитает человек. В модальной логике есть дополнительные модальные операторы со значениями, которые можно неформально охарактеризовать как, например, «необходимо, чтобы φ» (верно во всех возможных мирах) и «возможно, что φ» (верно в некотором возможном мире). При стандартной логике первого порядка у нас есть один домен, и каждому предикату присваивается одно расширение. С модальной логикой первого порядка у нас есть функция предметной области, которая назначает каждому возможному миру его собственный домен, так что каждый предикат получает расширение только относительно этих возможных миров. Это позволяет нам моделировать случаи, когда, например, Алекс - философ, но мог бы быть математиком, а мог бы не существовать вовсе. В первом возможном мире P ( a ) истинно, во втором P ( a ) ложно, а в третьем возможном мире вообще нет a в области.
  • Нечеткие логики первого порядка - это расширения первого порядка нечетких логик высказываний, а не классическое исчисление высказываний .

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

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

Логики высшего порядка

Характерной чертой логики первого порядка является то, что можно количественно оценить индивидов, но не предикаты. Таким образом

является законной формулой первого порядка, но

нет, в большинстве формализаций логики первого порядка. Логика второго порядка расширяет логику первого порядка, добавляя последний тип количественной оценки. Другие логики более высокого порядка позволяют количественное определение даже для более высоких типов, чем позволяет логика второго порядка. Эти более высокие типы включают отношения между отношениями, функции от отношений к отношениям между отношениями и другие объекты более высокого типа. Таким образом, «первый» в логике первого порядка описывает тип объектов, которые могут быть количественно определены.

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

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

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

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

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

Некоторые верификаторы доказательств, такие как Metamath , настаивают на том, чтобы на входе была полная деривация. Другие, такие как Мицар и Изабель , берут хорошо отформатированный эскиз доказательства (который все еще может быть очень длинным и подробным) и заполняют недостающие части, выполняя простой поиск доказательств или применяя известные процедуры принятия решения: полученный вывод затем проверяется небольшое ядро ​​ядра. Многие такие системы в первую очередь предназначены для интерактивного использования математиками-людьми: они известны как помощники по доказательству . Они также могут использовать формальные логики, которые сильнее логики первого порядка, например теорию типов. Поскольку полный вывод любого нетривиального результата в дедуктивной системе первого порядка будет чрезвычайно длинным для человека, чтобы написать, результаты часто формализуются в виде серии лемм, для которых выводы могут быть построены отдельно.

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

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

Смотрите также

Примечания

использованная литература

внешние ссылки