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

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

Логика первого порядка — также называемая логикой предикатов , исчислением предикатов , квантификационной логикой — представляет собой совокупность формальных систем, используемых в математике , философии , лингвистике и информатике . Логика первого порядка использует квантифицированные переменные над нелогическими объектами и допускает использование предложений, содержащих переменные. Вместо предложений, таких как «все люди смертны», в логике первого порядка можно иметь выражения в форме «для всех x , если x — человек, то x — смертен»; где «для всех x» — квантификатор, x — переменная, а «... — человек » и «... — смертен » — предикаты. ^[1] Это отличает ее от пропозициональной логики , которая не использует квантификаторы или отношения ; ^[2] в этом смысле пропозициональная логика является основой логики первого порядка.

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

Термин «первого порядка» отличает логику первого порядка от логики высшего порядка , в которой есть предикаты, имеющие предикаты или функции в качестве аргументов, или в которой разрешена квантификация по предикатам, функциям или и тем, и другим. ^{[4] : 56} В теориях первого порядка предикаты часто связаны с множествами. В интерпретируемых теориях высшего порядка предикаты могут интерпретироваться как множества множеств.

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

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

Основы логики первого порядка были разработаны независимо Готтлобом Фреге и Чарльзом Сандерсом Пирсом . ^[5] Об истории логики первого порядка и о том, как она стала доминировать над формальной логикой, см. Хосе Феррейрос (2001).

Введение

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

Рассмотрим два предложения « Сократ — философ» и « Платон — философ». В пропозициональной логике эти предложения сами по себе рассматриваются как индивиды исследования и могут быть обозначены, например, такими переменными, как p и q . Они не рассматриваются как применение предиката, например , к каким-либо конкретным объектам в области дискурса, вместо этого их рассматривают как чистое высказывание, которое является либо истинным, либо ложным. ^[6] Однако в логике первого порядка эти два предложения могут быть оформлены как утверждения о том, что определенный индивид или нелогический объект имеет свойство. В этом примере оба предложения имеют общую форму для некоторого индивида , в первом предложении значение переменной x равно «Сократ», а во втором предложении — «Платон». Благодаря возможности говорить о нелогических индивидах вместе с исходными логическими связками, логика первого порядка включает в себя пропозициональную логику. ^[7] ${\displaystyle {\text{isPhil}}}$ ${\displaystyle {\text{isPhil}}(x)}$ ${\displaystyle x}$

Истинность формулы, такой как « x — философ», зависит от того, какой объект обозначен x, и от интерпретации предиката «является философом». Следовательно, « x — философ» сам по себе не имеет определенного истинностного значения «истина» или «ложь» и сродни фрагменту предложения. ^[8] Отношения между предикатами могут быть установлены с помощью логических связок . Например, формула первого порядка «если x — философ, то x — ученый» является условным утверждением с « x — философ» в качестве гипотезы и « x — ученый» в качестве заключения, которое снова требует спецификации x , чтобы иметь определенное истинностное значение.

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

Отрицание предложения «Для каждого x , если x — философ, то x — ученый» логически эквивалентно предложению «Существует x такой, что x — философ, а x — не ученый». Квантор существования « существует» выражает идею о том, что утверждение « x — философ, а x — не ученый» справедливо для некоторого выбора x .

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

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

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

Синтаксис

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

Алфавит

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

Символы алфавита принято делить на логические символы , которые всегда имеют одно и то же значение, и нелогические символы , значение которых меняется в зависимости от интерпретации. ^[9] Например, логический символ всегда представляет «и»; он никогда не интерпретируется как «или», которое представлено логическим символом . Однако нелогический предикатный символ, такой как Phil( x ), может быть интерпретирован как означающий « x — философ», « x — человек по имени Филипп» или любой другой унарный предикат в зависимости от имеющейся интерпретации. ${\displaystyle \land }$ ${\displaystyle \lor }$

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

Логические символы представляют собой набор символов, которые различаются у разных авторов, но обычно включают в себя следующее: ^[10]

• Символы квантификатора : ∀ для универсальной квантификации и ∃ для экзистенциальной квантификации
• Логические связки : ∧ для конъюнкции , ∨ для дизъюнкции , → для импликации , ↔ для двуусловного , ¬ для отрицания. Некоторые авторы ^[11] используют C pq вместо → и E pq вместо ↔ , особенно в контекстах, где → используется для других целей. Более того, подкова ⊃ может заменить → ; ^[8] тройная черта ≡ может заменить ↔ ; тильда ( ~ ), N p или F p могут заменить ¬ ; двойная черта , , ^[12] или A pq могут заменить ∨ ; и амперсанд & , K pq или средняя точка ⋅ могут заменить ∧ , особенно если эти символы недоступны по техническим причинам. (Вышеупомянутые символы C pq , E pq , N p , A pq и K pq используются в польской нотации .) ${\displaystyle \|}$ ${\displaystyle +}$
• Скобки, квадратные скобки и другие знаки препинания. Выбор таких символов зависит от контекста.
• Бесконечный набор переменных , часто обозначаемый строчными буквами _в конце алфавита x , y , z , .... Для различения переменных часто используются нижние индексы _{: x0} , x1 , x2 , ....
• Символ равенства (иногда символ тождества ) = (см. § Равенство и его аксиомы ниже).

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

Другие логические символы включают в себя следующее:

• Константы истинности: T, V или ⊤ для «истины» и F, O или ⊥ для «ложи» (V и O взяты из польской нотации). Без каких-либо таких логических операторов валентности 0 эти две константы могут быть выражены только с помощью квантификаторов.
• Дополнительные логические связки, такие как черта Шеффера , D pq (НЕ-И), и исключающее ИЛИ , J pq .

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

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

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

  Пн ₀ , Пн ₁ , Пн ₂ , Пн ³ , _...^​​​

• Для каждого целого числа n  ≥ 0 существует бесконечно много символов n -арной функции :

  ф ^н ₀ , ф ^н ₁ , ф ^н ₂ , ф ^н ₃ , ...

Когда арность предикатного символа или функционального символа ясна из контекста, верхний индекс n часто опускается.

В этом традиционном подходе существует только один язык логики первого порядка. ^[13] Этот подход все еще распространен, особенно в философски ориентированных книгах.

Более поздняя практика заключается в использовании различных нелогических символов в соответствии с приложением, которое вы имеете в виду. Поэтому стало необходимым назвать набор всех нелогических символов, используемых в определенном приложении. Этот выбор осуществляется с помощью подписи . ^[14]

Типичные сигнатуры в математике — {1, ×} или просто {×} для групп , ^[3] или {0, 1, +, ×, <} для упорядоченных полей . Ограничений на количество нелогических символов нет. Сигнатура может быть пустой , конечной или бесконечной, даже несчетной . Несчетные сигнатуры встречаются, например, в современных доказательствах теоремы Лёвенгейма–Сколема .

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

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

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

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

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

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

Условия

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

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

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

Формулы

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

1. Предикатные символы . Если P — n -арный предикатный символ, а t ₁ , ..., t _n — термы, то P ( t ₁ ,..., t _n ) — формула.
2. Равенство . Если символ равенства считается частью логики, а t ₁ и t ₂ являются терминами, то t ₁ = t ₂ является формулой.
3. Отрицание . Если — формула, то — формула. ${\displaystyle \varphi }$ ${\displaystyle \lnot \varphi }$
4. Бинарные связки . Если ⁠ ⁠ ${\displaystyle \varphi }$ и ⁠ ⁠ ${\displaystyle \psi }$ являются формулами, то ( ) является формулой. Аналогичные правила применяются к другим бинарным логическим связкам. ${\displaystyle \varphi \rightarrow \psi }$
5. Квантификаторы . Если — формула, а x — переменная, то (для всех x выполняется) и (существует x такой, что ) — формулы. ${\displaystyle \varphi }$ ${\displaystyle \forall x\varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \exists x\varphi }$ ${\displaystyle \varphi }$

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

Например:

${\displaystyle \forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))}$

является формулой, если f является символом унарной функции, P — символом унарного предиката, а Q — символом тернарного предиката. Однако не является формулой, хотя это строка символов из алфавита. ${\displaystyle \forall x\,x\rightarrow }$

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

Условные обозначения

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

• ${\displaystyle \lnot }$оценивается в первую очередь
• ${\displaystyle \land }$и оцениваются следующим образом ${\displaystyle \lor }$
• Далее оцениваются квантификаторы.
• ${\displaystyle \to }$оценивается в последнюю очередь.

Более того, может быть вставлена ​​дополнительная пунктуация, не требуемая определением, — чтобы сделать формулы более удобными для чтения. Таким образом, формула:

${\displaystyle \lnot \forall xP(x)\to \exists x\lnot P(x)}$

можно записать так:

${\displaystyle (\lnot [\forall xP(x)])\to \exists x[\lnot P(x)].}$

В некоторых областях принято использовать инфиксную запись для бинарных отношений и функций вместо префиксной записи, определенной выше. Например, в арифметике обычно пишут "2 + 2 = 4" вместо "=(+(2,2),4)". Формулы в инфиксной записи принято рассматривать как сокращения соответствующих формул в префиксной записи, см. также term structure vs. representation .

Определения выше используют инфиксную запись для бинарных связок, таких как . Менее распространенной конвенцией является польская запись , в которой пишут , и так далее перед их аргументами, а не между ними. Эта конвенция выгодна тем, что позволяет отбрасывать все знаки препинания. Таким образом, польская запись компактна и элегантна, но редко используется на практике, поскольку ее трудно читать людям. В польской записи формула: ${\displaystyle \to }$ ${\displaystyle \rightarrow }$ ${\displaystyle \wedge }$

${\displaystyle \forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))}$

становится "∀x∀y→Pfx¬→ PxQfyxz".

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

В формуле переменная может встречаться свободной или связанной (или и то, и другое). Одна формализация этого понятия принадлежит Куайну: сначала определяется концепция вхождения переменной, затем определяется, является ли вхождение переменной свободным или связанным, затем определяется, является ли переменный символ в целом свободным или связанным. Чтобы различать различные вхождения одинакового символа x , каждое вхождение переменного символа x в формуле φ идентифицируется с начальной подстрокой φ до точки, в которой появляется указанный экземпляр символа x . ^{[8] стр. 297} Затем вхождение x называется связанным, если это вхождение x лежит в области действия по крайней мере одного из двух или . Наконец, x связан в φ, если все вхождения x в φ связаны. ^{[8] стр. 142--143} ${\displaystyle \exists x}$ ${\displaystyle \forall x}$

Интуитивно, переменный символ свободен в формуле, если ни в одной точке он не квантифицирован: ^{[8] стр.142--143} в ∀ y P ( x , y ) единственное вхождение переменной x свободно, а y связано. Свободные и связанные вхождения переменных в формулу определяются индуктивно следующим образом.

Атомные формулы

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

Отрицание

x встречается свободно в ¬ φ тогда и только тогда, когда x встречается свободно в φ . x встречается связанным в ¬ φ тогда и только тогда, когда x встречается связанным в φ.

Бинарные связки

x встречается свободно в ( φ → ψ ) тогда и только тогда, когда x встречается свободно либо в φ, либо в ψ . x встречается связанным в ( φ → ψ ), тогда и только тогда, когда x встречается связанным либо в φ, либо в ψ . То же правило применяется к любой другой бинарной связке вместо →.

Квантификаторы

x встречается свободно в ∀ y φ , тогда и только тогда, когда x встречается свободно в φ и x — отличный от y символ . Также x встречается связанным в ∀ y φ , тогда и только тогда, когда x есть y или x встречается связанным в φ . То же правило действует с ∃ вместо ∀ .

Например, в ∀ x ∀ y ( P ( x ) → Q ( x , f ( x ), z )) x и y встречаются только в связанном виде, ^[19] z встречается только в свободном виде, а w не является ни тем, ни другим, поскольку не встречается в формуле.

Свободные и связанные переменные формулы не обязательно должны быть непересекающимися множествами: в формуле P ( x ) → ∀ x Q ( x ) первое вхождение x как аргумента P является свободным, а второе, как аргумент Q , является связанным.

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

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

В математике язык упорядоченных абелевых групп имеет один постоянный символ 0, один унарный символ функции −, один бинарный символ функции + и один бинарный символ отношения ≤. Тогда:

• Выражения +( x , y ) и +( x , +( y , −( z ))) являются термами . Обычно они записываются как x + y и x + y − z .
• Выражения +( x , y ) = 0 и ≤(+( x , +( y , −( z ))), +( x , y )) являются атомарными формулами . Обычно они записываются как x + y = 0 и x + y − z  ≤  x + y .
• Выражение представляет собой формулу , которая обычно записывается как Эта формула имеет одну свободную переменную z . ${\displaystyle (\forall x\forall y\,[\mathop {\leq } (\mathop {+} (x,y),z)\to \forall x\,\forall y\,\mathop {+} (x,y)=0)]}$ ${\displaystyle \forall x\forall y(x+y\leq z)\to \forall x\forall y(x+y=0).}$

Аксиомы для упорядоченных абелевых групп могут быть выражены как набор предложений на языке. Например, аксиома, утверждающая, что группа коммутативна, обычно записывается ${\displaystyle (\forall x)(\forall y)[x+y=y+x].}$

Семантика

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

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

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

Область дискурса D — это непустое множество «объектов» некоторого вида. Интуитивно, при наличии интерпретации, формула первого порядка становится утверждением об этих объектах; например, утверждает существование некоторого объекта в D , для которого предикат P является истинным (или, точнее, для которого предикат, назначенный предикату символа P интерпретацией, является истинным). Например, можно взять D как множество целых чисел . ${\displaystyle \exists xP(x)}$

Нелогические символы интерпретируются следующим образом:

• Интерпретация символа n -арной функции — это функция от D ⁿ до D . Например, если областью дискурса является множество целых чисел, символ функции f арности 2 можно интерпретировать как функцию, которая возвращает сумму своих аргументов. Другими словами, символ f связан с функцией ⁠ ⁠, ${\displaystyle I(f)}$ которая в этой интерпретации является сложением.

• Интерпретация константного символа (функционального символа арности 0) — это функция от D ⁰ (множества, единственным членом которого является пустой кортеж ) до D , которую можно просто отождествить с объектом в D . Например, интерпретация может присвоить значение константному символу . ${\displaystyle I(c)=10}$ ${\displaystyle c}$

• Интерпретация n -арного предикатного символа — это набор из n -кортежей элементов D , дающих аргументы, для которых предикат истинен. Например, интерпретация бинарного предикатного символа P может быть набором пар целых чисел, таких, что первое из них меньше второго. Согласно этой интерпретации, предикат P будет истинным, если его первый аргумент меньше второго аргумента. Эквивалентно предикатным символам могут быть назначены булевы функции от D ⁿ до . ${\displaystyle I(P)}$ ${\displaystyle \{\mathrm {true,false} \}}$

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

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

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

• Переменные . Каждая переменная x вычисляется как μ ( x )
• Функции . При наличии терминов , которые были оценены как элементы области дискурса, и символа n -арной функции f , термин оценивается как . ${\displaystyle t_{1},\ldots ,t_{n}}$ ${\displaystyle d_{1},\ldots ,d_{n}}$ ${\displaystyle f(t_{1},\ldots ,t_{n})}$ ${\displaystyle (I(f))(d_{1},\ldots ,d_{n})}$

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

• Атомарные формулы (1) . Формуле присваивается значение true или false в зависимости от того , , где — оценка терминов , а — интерпретация , которая по предположению является подмножеством . ${\displaystyle P(t_{1},\ldots ,t_{n})}$ ${\displaystyle \langle v_{1},\ldots ,v_{n}\rangle \in I(P)}$ ${\displaystyle v_{1},\ldots ,v_{n}}$ ${\displaystyle t_{1},\ldots ,t_{n}}$ ${\displaystyle I(P)}$ ${\displaystyle P}$ ${\displaystyle D^{n}}$
• Атомарные формулы (2) . Формула считается истинной, если и оценивают один и тот же объект области дискурса (см. раздел о равенстве ниже). ${\displaystyle t_{1}=t_{2}}$ ${\displaystyle t_{1}}$ ${\displaystyle t_{2}}$
• Логические связки . Формула в виде , и т.д. оценивается в соответствии с таблицей истинности для рассматриваемой связки, как в пропозициональной логике. ${\displaystyle \neg \varphi }$ ${\displaystyle \varphi \rightarrow \psi }$
• Квантификаторы существования . Формула истинна согласно M и если существует оценка переменных, которая отличается от не более чем относительно оценки x и такая, что φ истинна согласно интерпретации M и назначению переменной . Это формальное определение отражает идею, что она истинна тогда и только тогда, когда существует способ выбрать значение для x таким образом, что φ( x ) выполняется. ${\displaystyle \exists x\varphi (x)}$ ${\displaystyle \mu }$ ${\displaystyle \mu '}$ ${\displaystyle \mu }$ ${\displaystyle \mu '}$ ${\displaystyle \exists x\varphi (x)}$
• Квантификаторы всеобщности . Формула истинна согласно M , и если φ( x ) истинна для каждой пары, составленной из интерпретации M и некоторого назначения переменной , которое отличается от максимум на значение x . Это отражает идею, что истинна, если каждый возможный выбор значения для x приводит к тому, что φ( x ) становится истинным. ${\displaystyle \forall x\varphi (x)}$ ${\displaystyle \mu }$ ${\displaystyle \mu '}$ ${\displaystyle \mu }$ ${\displaystyle \forall x\varphi (x)}$

Если формула не содержит свободных переменных, как и предложение, то начальное назначение переменных не влияет на его истинностное значение. Другими словами, предложение истинно согласно M и тогда и только тогда, когда оно истинно согласно M и любому другому назначению переменных . ${\displaystyle \mu }$ ${\displaystyle \mu '}$

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

• Квантификаторы существования (альтернативные) . Формула истинна согласно M , если в области дискурса существует некоторый d, такой что выполняется. Вот результат подстановки c _d для каждого свободного вхождения x в φ. ${\displaystyle \exists x\varphi (x)}$ ${\displaystyle \varphi (c_{d})}$ ${\displaystyle \varphi (c_{d})}$
• Квантификаторы всеобщности (альтернативные) . Формула истинна согласно M , если для каждого d в области дискурса истинна согласно M. ${\displaystyle \forall x\varphi (x)}$ ${\displaystyle \varphi (c_{d})}$

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

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

Если предложение φ оценивается как истинное при данной интерпретации M , говорят, что M удовлетворяет φ; это обозначается ^[20] . Предложение выполнимо , если есть некоторая интерпретация, при которой оно истинно. Это немного отличается от символа из теории моделей, где обозначает выполнимость в модели, т. е. «существует подходящее назначение значений в области ' переменным символам ". ^[21] ${\displaystyle M\vDash \varphi }$ ${\displaystyle \vDash }$ ${\displaystyle M\vDash \phi }$ ${\displaystyle M}$ ${\displaystyle \phi }$

Выполнимость формул со свободными переменными более сложна, поскольку интерпретация сама по себе не определяет истинностное значение такой формулы. Наиболее распространенное соглашение заключается в том, что формула φ со свободными переменными , ..., считается удовлетворенной интерпретацией, если формула φ остается истинной независимо от того, какие индивиды из области дискурса назначены ее свободным переменным , ..., . Это имеет тот же эффект, что и утверждение, что формула φ удовлетворена тогда и только тогда, когда удовлетворено ее универсальное замыкание . ${\displaystyle x_{1}}$ ${\displaystyle x_{n}}$ ${\displaystyle x_{1}}$ ${\displaystyle x_{n}}$ ${\displaystyle \forall x_{1}\dots \forall x_{n}\phi (x_{1},\dots ,x_{n})}$

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

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

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

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

• Цилиндрическая алгебра , Альфред Тарский и коллеги;
• Полиадическая алгебра Пола Халмоша ;
• Логика предикатных функторов , в основном принадлежащая Уилларду Куайну .

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

Тарский и Дживант (1987) показали, что фрагмент логики первого порядка, не имеющий атомарного предложения , лежащего в области действия более трех квантификаторов, имеет ту же выразительную силу, что и алгебра отношений . ^{[23] : 32–33} Этот фрагмент представляет большой интерес, поскольку он достаточен для арифметики Пеано и большинства аксиоматических теорий множеств , включая каноническую ZFC . Они также доказывают, что логика первого порядка с примитивной упорядоченной парой эквивалентна алгебре отношений с двумя упорядоченными парными проекционными функциями . ^{[24] : 803}

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

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

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

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

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

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

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

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

• Многие общие правила вывода действительны только тогда, когда требуется, чтобы домен дискурса был непустым. Одним из примеров является правило, утверждающее, что подразумевает, когда x не является свободной переменной в . Это правило, которое используется для приведения формул в предваренную нормальную форму , является обоснованным в непустых доменах, но необоснованным, если пустой домен разрешен. ${\displaystyle \varphi \lor \exists x\psi }$ ${\displaystyle \exists x(\varphi \lor \psi )}$ ${\displaystyle \varphi }$
• Определение истины в интерпретации, которая использует функцию назначения переменной, не может работать с пустыми доменами, поскольку нет функций назначения переменной, диапазон которых пуст. (Аналогично, нельзя назначать интерпретации постоянным символам.) Это определение истины требует, чтобы нужно было выбрать функцию назначения переменной (μ выше) до того, как можно будет определить значения истины даже для атомарных формул. Затем значение истины предложения определяется как его значение истины при любом назначении переменной, и доказывается, что это значение истины не зависит от того, какое назначение выбрано. Этот метод не работает, если вообще нет функций назначения; его необходимо изменить, чтобы учесть пустые домены.

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

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

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

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

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

В общем, логическое следствие в логике первого порядка разрешимо лишь наполовину : если предложение 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 , так что формула после подстановки будет , что снова логически допустимо. ${\displaystyle \exists x(x=y)}$ ${\displaystyle \exists x(x=x+1)}$ ${\displaystyle \exists z(z=x+1)}$

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

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

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

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

Последовательное исчисление

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

${\displaystyle A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},}$

где A ₁ , ..., A _n , B ₁ , ..., B _k — формулы, а символ турникета используется как знак препинания для разделения двух половин. Интуитивно секвенция выражает идею, которая подразумевает . ${\displaystyle \vdash }$ ${\displaystyle (A_{1}\land \cdots \land A_{n})}$ ${\displaystyle (B_{1}\lor \cdots \lor B_{k})}$

Метод таблиц

Табличное доказательство для пропозициональной формулы ((a ∨ ¬b) ∧ b) → a

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

Разрешение

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

Метод резолюции работает только с формулами, которые являются дизъюнкциями атомарных формул; произвольные формулы должны быть сначала преобразованы в эту форму посредством скулемизации . Правило резолюции гласит, что из гипотез и можно получить заключение . ${\displaystyle A_{1}\lor \cdots \lor A_{k}\lor C}$ ${\displaystyle B_{1}\lor \cdots \lor B_{l}\lor \lnot C}$ ${\displaystyle A_{1}\lor \cdots \lor A_{k}\lor B_{1}\lor \cdots \lor B_{l}}$

Доказуемые идентичности

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

${\displaystyle \lnot \forall x\,P(x)\Leftrightarrow \exists x\,\lnot P(x)}$

${\displaystyle \lnot \exists x\,P(x)\Leftrightarrow \forall x\,\lnot P(x)}$

${\displaystyle \forall x\,\forall y\,P(x,y)\Leftrightarrow \forall y\,\forall x\,P(x,y)}$

${\displaystyle \exists x\,\exists y\,P(x,y)\Leftrightarrow \exists y\,\exists x\,P(x,y)}$

${\displaystyle \forall x\,P(x)\land \forall x\,Q(x)\Leftrightarrow \forall x\,(P(x)\land Q(x))}$

${\displaystyle \exists x\,P(x)\lor \exists x\,Q(x)\Leftrightarrow \exists x\,(P(x)\lor Q(x))}$

${\displaystyle P\land \exists x\,Q(x)\Leftrightarrow \exists x\,(P\land Q(x))}$(где не должно встречаться свободно в ) ${\displaystyle x}$ ${\displaystyle P}$

${\displaystyle P\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P\lor Q(x))}$(где не должно встречаться свободно в ) ${\displaystyle x}$ ${\displaystyle P}$

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

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

• Рефлексивность . Для каждой переменной x , x = x .
• Замена функций . Для всех переменных x и y и любого символа функции f ,

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

• Подстановка формул . Для любых переменных x и y и любой формулы φ( z ) со свободной переменной z, тогда:

  х = у → (φ(х) → φ(у)).

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

φ(z): f (..., x , ...) = f (..., z , ...)

Затем

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

Так как дано x = y , а f (..., x , ...) = f (..., x , ...) истинно по рефлексивности, то имеем f (..., x , ...) = f (..., y , ...)

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

• Симметрия . Если x = y , то y = x . ^[27]
• Транзитивность . Если x = y и y = z, то x = z . ^[28]

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

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

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

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

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

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

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

• В теории частичных порядков с одним символом отношения ≤ можно определить s = t как сокращение для s ≤ t t ≤ s . ${\displaystyle \wedge }$
• В теории множеств с одним отношением ∈ можно определить s = t как сокращение для ∀ x ( s ∈ x ↔ t ∈ x ) ∀ x ( x ∈ s ↔ x ∈ t ) ${\displaystyle \wedge }$ . Это определение равенства затем автоматически удовлетворяет аксиомам равенства. В этом случае следует заменить обычную аксиому экстенсиональности , которую можно сформулировать как , альтернативной формулировкой , которая гласит, что если множества x и y имеют одни и те же элементы, то они также принадлежат одним и тем же множествам. ${\displaystyle \forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow x=y]}$ ${\displaystyle \forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow \forall z(x\in z\Leftrightarrow y\in z)]}$

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

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

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

Теорема о полноте Гёделя , доказанная Куртом Гёделем в 1929 году, устанавливает, что существуют надежные, полные, эффективные дедуктивные системы для логики первого порядка, и, таким образом, отношение логического следствия первого порядка охватывается конечной доказуемостью. Наивно, утверждение, что формула φ логически подразумевает формулу ψ, зависит от каждой модели φ; эти модели, как правило, будут иметь произвольно большую мощность, и поэтому логическое следствие не может быть эффективно проверено проверкой каждой модели. Однако можно перечислить все конечные выводные данные и найти вывод ψ из φ. Если ψ логически подразумевается φ, такой вывод в конечном итоге будет найден. Таким образом, логическое следствие первого порядка полуразрешимо : можно сделать эффективное перечисление всех пар предложений (φ,ψ) таким образом, что ψ является логическим следствием φ.

В отличие от пропозициональной логики , логика первого порядка неразрешима (хотя и полуразрешима), при условии, что язык имеет хотя бы один предикат арности не менее 2 (кроме равенства). Это означает, что не существует процедуры принятия решения , которая определяет, являются ли произвольные формулы логически допустимыми. Этот результат был установлен независимо Алонзо Чёрчем и Аланом Тьюрингом в 1936 и 1937 годах соответственно, что дало отрицательный ответ на Entscheidungsproblem, поставленную Дэвидом Гильбертом и Вильгельмом Аккерманом в 1928 году. Их доказательства демонстрируют связь между неразрешимостью проблемы принятия решения для логики первого порядка и неразрешимостью проблемы остановки .

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

Теорема Лёвенгейма–Сколема

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

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

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

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

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

Существуют также более тонкие ограничения логики первого порядка, которые подразумеваются теоремой о компактности. Например, в информатике многие ситуации можно смоделировать как направленный граф состояний (узлов) и связей (направленных ребер). Проверка такой системы может потребовать показать, что ни одно «плохое» состояние не может быть достигнуто из любого «хорошего» состояния. Таким образом, мы стремимся определить, находятся ли хорошие и плохие состояния в разных связных компонентах графа. Однако теорему о компактности можно использовать, чтобы показать, что связные графы не являются элементарным классом в логике первого порядка, и нет формулы φ( x , y ) логики первого порядка, в логике графов , которая выражает идею о том, что существует путь от x до y . Связность может быть выражена в логике второго порядка , однако, но не только с помощью кванторов множества существования, поскольку также обладает компактностью. ${\displaystyle \Sigma _{1}^{1}}$

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

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

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

Ограничения

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

Например, логика первого порядка неразрешима, что означает, что надежный, полный и завершающий алгоритм принятия решения для доказуемости невозможен. Это привело к изучению интересных разрешимых фрагментов, таких как C ₂ : логика первого порядка с двумя переменными и подсчитывающими кванторами и . ^[30] ${\displaystyle \exists ^{\geq n}}$ ${\displaystyle \exists ^{\leq n}}$

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

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

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

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

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

Ограничения, расширения и вариации

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

Ограниченные языки

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

• Поскольку может быть выражено как , и может быть выражено как , любой из двух квантификаторов и может быть опущен. ${\displaystyle \exists x\varphi (x)}$ ${\displaystyle \neg \forall x\neg \varphi (x)}$ ${\displaystyle \forall x\varphi (x)}$ ${\displaystyle \neg \exists x\neg \varphi (x)}$ ${\displaystyle \exists }$ ${\displaystyle \forall }$
• Так как может быть выражено как и может быть выражено как , либо или можно опустить. Другими словами, достаточно иметь и , или и , как единственные логические связки. ${\displaystyle \varphi \lor \psi }$ ${\displaystyle \lnot (\lnot \varphi \land \lnot \psi )}$ ${\displaystyle \varphi \land \psi }$ ${\displaystyle \lnot (\lnot \varphi \lor \lnot \psi )}$ ${\displaystyle \vee }$ ${\displaystyle \wedge }$ ${\displaystyle \neg }$ ${\displaystyle \vee }$ ${\displaystyle \neg }$ ${\displaystyle \wedge }$
• Аналогично, достаточно иметь только и в качестве логических связок, или иметь только оператор штриха Шеффера (NAND) или стрелку Пирса (NOR). ${\displaystyle \neg }$ ${\displaystyle \rightarrow }$
• Можно полностью избежать функциональных символов и константных символов, переписав их через предикатные символы соответствующим образом. Например, вместо использования константного символа можно использовать предикат (интерпретируемый как ) и заменить каждый предикат, такой как на . Функция, такая как , будет аналогичным образом заменена предикатом, интерпретируемым как . Это изменение требует добавления дополнительных аксиом в имеющуюся теорию, так что интерпретации используемых предикатных символов имели правильную семантику. ^[32] ${\displaystyle \;0}$ ${\displaystyle \;0(x)}$ ${\displaystyle \;x=0}$ ${\displaystyle \;P(0,y)}$ ${\displaystyle \forall x\;(0(x)\rightarrow P(x,y))}$ ${\displaystyle f(x_{1},x_{2},...,x_{n})}$ ${\displaystyle F(x_{1},x_{2},...,x_{n},y)}$ ${\displaystyle y=f(x_{1},x_{2},...,x_{n})}$

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

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

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

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

Когда в теории имеется только конечное число сортов, многосортная логика первого порядка может быть сведена к односортной логике первого порядка. ^{[34] : 296–299} В односортную теорию вводится унарный предикатный символ для каждого сорта в многосортной теории и добавляется аксиома, гласящая, что эти унарные предикаты разделяют область дискурса. Например, если имеется два сорта, добавляются предикатные символы и и аксиома: ${\displaystyle P_{1}(x)}$ ${\displaystyle P_{2}(x)}$

${\displaystyle \forall x(P_{1}(x)\lor P_{2}(x))\land \lnot \exists x(P_{1}(x)\land P_{2}(x))}$.

Тогда элементы, удовлетворяющие , рассматриваются как элементы первого сорта, а элементы, удовлетворяющие , как элементы второго сорта. Можно провести квантификацию по каждому сорту, используя соответствующий предикатный символ для ограничения диапазона квантификации. Например, чтобы сказать, что существует элемент первого сорта, удовлетворяющий формуле , нужно написать: ${\displaystyle P_{1}}$ ${\displaystyle P_{2}}$ ${\displaystyle \varphi (x)}$

${\displaystyle \exists x(P_{1}(x)\land \varphi (x))}$.

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

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

• Иногда полезно сказать, что « P ( x ) справедливо ровно для одного x », что можно выразить как ∃! x P ( x ) . Эта нотация, называемая квантификацией уникальности , может быть использована для сокращения формулы, такой как ∃ x ( P ( x ) ∀ y ( P ( y ) → ( x = y ))) ${\displaystyle \wedge }$ .
• Логика первого порядка с дополнительными кванторами имеет новые кванторы Qx ,..., со значениями, такими как «существует много x таких, что ...». См. также кванторы ветвления и кванторы множественного числа Джорджа Булоса и других.
• Ограниченные квантификаторы часто используются при изучении теории множеств или арифметики.

Бесконечные логики

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

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

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

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

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

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

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

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

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

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

${\displaystyle \exists a({\text{Phil}}(a))}$

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

${\displaystyle \exists {\text{Phil}}({\text{Phil}}(a))}$

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

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

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

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

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

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

Некоторые верификаторы доказательств, такие как Metamath , настаивают на наличии полного вывода в качестве входных данных. Другие, такие как Mizar и Isabelle , берут хорошо отформатированный набросок доказательства (который все еще может быть очень длинным и подробным) и заполняют недостающие части, выполняя простой поиск доказательств или применяя известные процедуры принятия решений: полученный вывод затем проверяется небольшим основным «ядром». Многие такие системы в первую очередь предназначены для интерактивного использования математиками-людьми: они известны как помощники по доказательству . Они также могут использовать формальную логику, которая сильнее логики первого порядка, например, теорию типов. Поскольку полный вывод любого нетривиального результата в дедуктивной системе первого порядка будет чрезвычайно длинным для записи человеком, ^[39] результаты часто формализуются в виде серии лемм, для которых выводы могут быть построены отдельно.

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

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

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

• Философский портал

• ACL2 — вычислительная логика для аппликационного Common Lisp
• Аристотелевская логика
• Равносогласованность
• Игра Эренфойхта-Фресса
• Расширение по определениям
• Расширение (логика предикатов)
• Еебрендизация
• Список логических символов

• Ложбан
• Число Лёвенгейма
• Непервоупорядочиваемость
• Нормальная предварительная форма
• Предыдущая аналитика
• Пролог
• Реляционная алгебра
• Реляционная модель
• Сколемская нормальная форма
• Мир Тарского
• Таблица истинности
• Тип (теория модели)

Примечания

1. Ходжсон, доктор Дж. П. Э., «Логика первого порядка» (archive.org), Университет Святого Иосифа , Филадельфия , 1995.
2. Хьюз, GE и Крессвелл, MJ , Новое введение в модальную логику ( Лондон : Routledge , 1996), стр.161.
3. A. Tarski, Undecidable Theories (1953), стр. 77. Исследования по логике и основаниям математики, Северная Голландия
4. Мендельсон, Эллиотт (1964). Введение в математическую логику . Ван Ностранд Рейнхольд . стр. 56.
5. Эрик М. Хаммер: Семантика для экзистенциальных графов, Журнал философской логики , том 27, выпуск 5 (октябрь 1998 г.), стр. 489: «Развитие логики первого порядка независимо от Фреге, предвосхищая предваренные и сколемовские нормальные формы»
6. Х. Фридман, «Приключения в основах математики 1: Логическое рассуждение», Ross Program 2022, заметки лекций. Доступ 28 июля 2023 г.
7. Герцель, Б. , Гейсвайлер, Н., Коэльо, Л., Яничич, П. и Пенначин, К., Рассуждения в реальном мире: к масштабируемому, неопределенному пространственно-временному, контекстуальному и причинному выводу ( Амстердам и Париж : Atlantis Press , 2011), стр. 29–30.
8. WVO Куайн, Математическая логика (1981). Издательство Гарвардского университета, 0-674-55451-5.
9. Дэвис, Эрнест (1990). Представления здравого смысла знаний . Морган Кауфманн. С. 27–28. ISBN 978-1-4832-0770-4.
10. "Предикатная логика | Brilliant Math & Science Wiki". brilliant.org . Получено 20-08-2020 .
11. "Введение в символическую логику: Лекция 2". cstl-cla.semo.edu . Получено 04.01.2021 .
12. Ганс Гермес (1973). Введение в математическую логику . Hochschultext (Springer-Verlag). Лондон: Springer. ISBN 3540058192. ISSN  1431-4657.
13. Точнее, существует только один язык каждого варианта односортной логики первого порядка: с равенством или без него, с функциями или без них, с пропозициональными переменными или без них, ....
14. Слово « язык» иногда используется как синоним слова «подпись», но это может привести к путанице, поскольку «язык» может также относиться к набору формул.
15. Эберхард Бергманн и Хельга Нолл (1977). Математическая логика с информатикой . Heidelberger Taschenbücher, Sammlung Informatik (на немецком языке). Том. 187. Гейдельберг: Шпрингер. стр. 300–302.
16. Смаллиан, Р. М. , Логика первого порядка ( Нью-Йорк : Dover Publications , 1968), стр. 5.
17. Г. Такеути, «Теория доказательств» (1989, стр. 6)
18. Некоторые авторы, использующие термин «правильно построенная формула», используют «формулу» для обозначения любой строки символов из алфавита. Однако большинство авторов в математической логике используют «формулу» для обозначения «правильно построенной формулы» и не имеют термина для неправильно построенных формул. В любом контексте интерес представляют только правильно построенные формулы.
19. y встречается в соответствии с правилом 4, хотя он не появляется ни в одной атомарной подформуле
20. Кажется, этот символ был введен Клини, см. сноску 30 в переиздании Довером в 2002 году его книги «Математическая логика», издательство John Wiley and Sons, 1967. ${\displaystyle \vDash }$
21. FR Drake, Теория множеств: Введение в большие кардиналы (1974)
22. Роджерс, Р. Л., Математическая логика и формализованные теории: обзор основных концепций и результатов (Амстердам/Лондон: North-Holland Publishing Company , 1971), стр. 39.
23. Бринк, К. , Каль, В., и Шмидт, Г. , ред., Реляционные методы в информатике ( Берлин / Гейдельберг : Springer , 1997), стр. 32–33.
24. Anon., Mathematical Reviews ( Провиденс : Американское математическое общество , 2006), стр. 803.
25. Шанкар, Н. , Оуре, С., Рашби, Дж. М. и Стрингер-Калверт, Д. В. Дж., Руководство по испытанию образцов PVS 7.1 ( Менло-Парк : SRI International , август 2020 г.).
26. Фитинг, М. , Логика первого порядка и автоматическое доказательство теорем (Берлин/Гейдельберг: Springer, 1990), стр. 198–200.
27. Используйте подстановку формул, где φ(z) — z = x , тогда φ(x) — это x=x, что подразумевает φ(y): y=x, затем используйте рефлексивность.
28. Используйте подстановку формулы, где φ(a) — это a = z , чтобы получить y = x → ( y = z → x = z ), затем используйте симметрию и декарринг .
29. Ходель, Р. Э., Введение в математическую логику ( Mineola NY : Dover , 1995), стр. 199.
30. Хоррокс, Ян (2010). «Описательная логика: формальная основа для языков и инструментов» (PDF) . Слайд 22. Архивировано (PDF) из оригинала 2015-09-06.
31. Гамут 1991, стр. 75.
32. Левая тотальность может быть выражена аксиомой ; правая единственность — , при условии, что допускается символ равенства. Оба также применимы к постоянным заменам (для ). ${\displaystyle \forall x_{1},...,x_{n}.\exists y.F(x_{1},...,x_{n},y)}$ ${\displaystyle \forall x_{1},...,x_{n},y,y'.}$ ${\displaystyle F(x_{1},...,x_{n},y)\land F(x_{1},...,x_{n},y')\rightarrow y=y'}$ ${\displaystyle n=0}$
33. Uzquiano, Gabriel (17 октября 2018 г.). «Квантификаторы и квантификация». В Zalta, Edward N. (ред.). Stanford Encyclopedia of Philosophy (зимнее изд. 2018 г.).См., в частности, раздел 3.2, Многосортная квантификация.
34. Эндертон, Х. Математическое введение в логику , второе издание. Academic Press , 2001, стр. 296–299.
35. Некоторые авторы допускают только формулы с конечным числом свободных переменных в L _κω , а в более общем случае — только формулы с < λ свободными переменными в L _κλ .
36. Bosse, Uwe (1993). "Игра Эренфойхта–Фрайсса для логики с фиксированной точкой и стратифицированной логики с фиксированной точкой". В Börger, Egon (ред.). Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers . Lecture Notes in Computer Science. Vol. 702. Springer-Verlag . pp. 100–114. ISBN 3-540-56992-8. Збл  0808.03024.
37. Мелвин Фиттинг (6 декабря 2012 г.). Логика первого порядка и автоматическое доказательство теорем. Springer Science & Business Media. ISBN 978-1-4612-2360-3.
38. "15-815 Автоматическое доказательство теорем". www.cs.cmu.edu . Получено 2024-01-10 .
39. Авигад и др. (2007) обсуждают процесс формальной проверки доказательства теоремы о простых числах . Формализованное доказательство потребовало около 30 000 строк ввода для верификатора доказательств Isabelle.

Ссылки

• Раутенберг, Вольфганг (2010), Краткое введение в математическую логику (3-е изд.), Нью-Йорк, штат Нью-Йорк : Springer Science+Business Media , doi : 10.1007/978-1-4419-1221-3, ISBN 978-1-4419-1220-6
• Эндрюс, Питер Б. (2002); Введение в математическую логику и теорию типов: к истине через доказательство , 2-е изд., Берлин: Kluwer Academic Publishers. Доступно в Springer.
• Авигад, Джереми; Доннелли, Кевин; Грей, Дэвид; и Рафф, Пол (2007); «Формально проверенное доказательство теоремы о простых числах», ACM Transactions on Computational Logic , т. 9, № 1, doi :10.1145/1297658.1297660
• Barwise, Jon (1977). "Введение в логику первого порядка". В Barwise, Jon (ред.). Справочник по математической логике . Исследования по логике и основаниям математики. Амстердам, Нидерланды: Северная Голландия (опубликовано в 1982 году). ISBN 978-0-444-86388-1.
• Монк, Дж. Дональд (1976). Математическая логика. Нью-Йорк, Нью-Йорк: Springer New York. doi :10.1007/978-1-4684-9452-5. ISBN 978-1-4684-9454-9.
• Барвайз, Джон; и Этчеменди, Джон (2000); Языковое доказательство и логика , Стэнфорд, Калифорния: CSLI Publications (Распространяется издательством Чикагского университета)
• Бохенский, Юзеф Мария (2007); A Précis of Mathematical Logic , Дордрехт, Нидерланды: D. Reidel, перевод с французского и немецкого изданий Отто Берда
• Феррейрос, Хосе (2001); Дорога к современной логике — интерпретация, Бюллетень символической логики, том 7, выпуск 4, 2001, стр. 441–484, doi : 10.2307/2687794, JSTOR  2687794
• Гамут, LTF (1991), Логика, язык и значение, том 2: Интенсиональная логика и логическая грамматика , Чикаго, Иллинойс: Издательство Чикагского университета, ISBN 0-226-28088-8
• Гильберт, Дэвид ; и Акерманн, Вильгельм (1950); Принципы математической логики , Челси (английский перевод Grundzüge der theoretischen Logik , первое немецкое издание 1928 года)
• Ходжес, Уилфрид (2001); «Классическая логика I: логика первого порядка», в книге Гобла, Лу (ред.); «Путеводитель по философской логике» издательства Blackwell , Blackwell
• Эббингауз, Хайнц-Дитер ; Флум, Йорг; и Томас, Вольфганг (1994); Математическая логика, Тексты для студентов по математике , Берлин, Делавэр/Нью-Йорк, Нью-Йорк: Springer-Verlag , второе издание, ISBN 978-0-387-94258-2 
• Тарский, Альфред и Дживант, Стивен (1987); Формализация теории множеств без переменных . Том 41 публикаций коллоквиума Американского математического общества, Провиденс, Род-Айленд: Американское математическое общество, ISBN 978-0821810415 

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

• «Исчисление предикатов», Энциклопедия математики , EMS Press , 2001 [1994]
• Стэнфордская энциклопедия философии : Шапиро, Стюарт; «Классическая логика». Охватывает синтаксис, теорию моделей и метатеорию для логики первого порядка в стиле естественной дедукции.
• Магнус, ПД; forall x: введение в формальную логику . Охватывает формальную семантику и теорию доказательств для логики первого порядка.
• Metamath: текущий онлайн-проект по реконструкции математики как огромной теории первого порядка с использованием логики первого порядка и аксиоматической теории множеств ZFC . Модернизированная Principia Mathematica .
• Подниекс, Карл; Введение в математическую логику
• Заметки по Cambridge Mathematical Tripos (набранные Джоном Фремлином). Эти заметки охватывают часть прошлого курса Cambridge Mathematical Tripos, который преподавался студентам бакалавриата (обычно) на третьем курсе. Курс называется «Логика, вычисления и теория множеств» и охватывает порядковые и кардинальные числа, частично упорядоченные множества и лемму Цорна, пропозициональную логику, логику предикатов, теорию множеств и вопросы непротиворечивости, связанные с ZFC и другими теориями множеств.
• Генератор доказательств дерева может проверять или опровергать формулы логики первого порядка с помощью метода семантических таблиц .