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

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

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

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

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

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

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

Введение [ править ]

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

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

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

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

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

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

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

Синтаксис [ править ]

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

Алфавит [ править ]

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

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

Логические символы [ править ]

В алфавите есть несколько логических символов, которые различаются в зависимости от автора, но обычно включают: ^{[6] [7]}

• В кванторных символах: ∀ для универсальной квантификации и ∃ для экзистенциальной квантификации
• В логические связки : ∧ для связи , ∨ для дизъюнкции , → для импликации , ↔ для biconditional , ¬ для отрицания. Иногда используются другие логические соединительные символы. Некоторые авторы ^[8] используют 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 ₀ , x ₁ , x ₂ , ....
• Символ равенства (иногда, символ идентичности ) =; см. раздел о равенстве ниже .

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

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

Нелогические символы [ править ]

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

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

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

   P ⁿ ₀ , P ⁿ ₁ , P ⁿ ₂ , P ⁿ ₃ , ...

2. Для любого целого n  ≥ 0 существует бесконечное число n -арных функциональных символов :

   f ⁿ ₀ , f ⁿ ₁ , f ⁿ ₂ , f ⁿ ₃ , ...

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

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

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

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

Правила формирования [ править ]

< индекс >  :: = "" | < индекс > "'" < переменная >  :: = "x" < индекс > < константа >  :: = "c" < индекс > < унарная функция >  :: = "f1" < индекс > < бинарная функция >  :: = "f2" < индекс > < тернарная функция >  :: = "f3" < индекс > <унарный предикат >  :: ="p1" < индекс > < двоичный предикат >  :: = "p2" < индекс > < тройной предикат >  :: = "p3" < индекс > < термин >  :: =  < переменная > | < константа > | < унарная функция > "(" < термин > ")" | < бинарная функция > "(" < термин > "," < термин > ")" | < тернарная функция > "(" < термин > "," < термин > "," < термин > ")" < атомарная формула >  :: = "ИСТИНА" | "ЛОЖНЫЙ" | < термин > "=" < термин > | < унарный предикат > "(" < термин > ")" | < бинарный предикат > "(" < термин > "," < термин > ")" | < тернарный предикат > "(" < термин > "," < термин > "," < термин > ")" < формула >  :: =  < атомарная формула > | "¬" < формула > | < формула > «∧» < формула > | < формула > "∨" <формула > |< формула > "⇒" < формула > | < формула > «⇔» < формула > | "(" < формула > ")" | «∀» < переменная >  < формула > | «∃» < переменная >  < формула >

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

Условия [ править ]

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

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

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

Формулы [ править ]

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

1. Предикатные символы. Если P - n -арный предикатный символ и t ₁ , ..., t _n - термы, то P ( t ₁ , ..., t _n ) - формула.
2. Равенство . Если символ равенства считается частью логики, а t ₁ и t ₂ являются членами, то t ₁ = t ₂ является формулой.
3. Отрицание. Если φ формула, то φ формула.${\ Displaystyle \ lnot}$
4. Бинарные связки. Если φ и ψ формулы, то (φ ψ) формула. Подобные правила применяются к другим двоичным логическим связкам.${\displaystyle \rightarrow }$
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 }$

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

Это определение формулы не поддерживает определение функции if-then-else ite (c, a, b) , где «c» - это условие, выраженное в виде формулы, которая вернет «a», если c истинно, и « б "если это ложь. Это связано с тем, что и предикаты, и функции могут принимать только термины в качестве параметров, но первый параметр - это формула. Некоторые языки, построенные на логике первого порядка, такие как SMT-LIB 2.0, добавляют это. ^[15]

Условные обозначения [ править ]

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

• ${\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)». Принято рассматривать формулы в инфиксной записи как сокращения для соответствующих формул в префиксной записи, ср. также временная структура против представления .

В приведенных выше определениях используется инфиксная нотация для двоичных связок, таких как . Менее общее соглашение является польская запись , в которой один пишет , и так далее перед своими аргументами , а не между ними. Это соглашение выгодно тем, что позволяет отбросить все символы пунктуации. Таким образом, польские обозначения компактны и элегантны, но редко используются на практике, потому что их трудно читать людям. В польских обозначениях формула${\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».

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

В формуле переменная может быть свободной или связанной (или и тем, и другим). Интуитивно понятно, что переменная может быть в формуле свободна, если она не определена количественно: ^[16] в y P ( x , y ) единственное вхождение переменной x является свободным, в то время как y является связанным. Вхождения свободных и связанных переменных в формулу индуктивно определяются следующим образом.

1. Атомарные формулы. Если φ является атомарной формулой, то x появляется в φ свободно тогда и только тогда, когда x входит в φ. Более того, ни в одной атомарной формуле нет связанных переменных.
2. Отрицание. x появляется свободным в ¬φ тогда и только тогда, когда x встречается свободным в φ. x встречается связанным в ¬φ тогда и только тогда, когда x встречается связанным в φ.
3. Бинарные связки. x появляется свободным в (φ → ψ) тогда и только тогда, когда x встречается свободно в φ или ψ. x встречается связанной в (φ → ψ) тогда и только тогда, когда x встречается связанной либо в φ, либо в ψ. То же правило применяется к любой другой двоичной связке вместо →.
4. Квантификаторы. x появляется свободным в y φ, тогда и только тогда, когда x встречается свободно в φ и x является отличным от y символом . Кроме того, x встречается связанным в ∀ y φ, если и только если x равно y или x встречается связанным в φ. То же правило выполняется с ∃ вместо ∀.

Например, в ∀ x ∀ y ( P ( x ) → Q ( x , f ( x ), z )) x и y встречаются только связанными, ^[17] 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 - это непустое множество «объектов» определенного вида. Интуитивно формула первого порядка - это утверждение об этих объектах; например, заявляет о существовании такого объекта x , что предикат P истинен там, где он упоминается. Область дискурса - это совокупность рассматриваемых объектов. Например, можно принять набор целых чисел.${\displaystyle \exists xP(x)}$${\displaystyle D}$

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

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

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

Структуры первого порядка [ править ]

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

• Каждому функциональному символу f арности n присваивается функция I (f) от до . В частности, каждому постоянному символу подписи присваивается индивидуум в предметной области.${\displaystyle D^{n}}$${\displaystyle D}$
• Каждому предикатному символу P арности n присваивается отношение I (P) над или, что то же самое, функция от до . Таким образом , каждый предикат символ интерпретируется булевозначной функцией на D .${\displaystyle D^{n}}$${\displaystyle D^{n}}$${\displaystyle \{\mathrm {true,false} \}}$

Оценка истинности [ править ]

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

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

1. Переменные. Каждая переменная x оценивается как μ ( x )
2. Функции. Учитывая термины , которые были оценены как элементы предметной области, и 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. Атомарные формулы (1). С формулой связано значение истина или ложь в зависимости от того , где, где находятся оценка терминов и интерпретация , которая по предположению является подмножеством .${\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. Атомарные формулы (2). Формула присваивается верно , если и оценить тот же объект домена дискурса (см раздел равенства ниже).${\displaystyle t_{1}=t_{2}}$${\displaystyle t_{1}}$${\displaystyle t_{2}}$
3. Логические связки. Формула в форме , и т. Д. Оценивается в соответствии с таблицей истинности для рассматриваемой связки, как в логике высказываний.${\displaystyle \neg \phi }$${\displaystyle \phi \rightarrow \psi }$
4. Экзистенциальные кванторы. Формула истинна согласно M и если существует оценка переменных, которая отличается только от оценки x и такая, что φ истинно согласно интерпретации M и присвоению переменной . Это формальное определение отражает идею, которая истинна тогда и только тогда, когда есть способ выбрать значение для x, такое, что φ ( x ) удовлетворяется.${\displaystyle \exists x\phi (x)}$${\displaystyle \mu }$${\displaystyle \mu '}$${\displaystyle \mu }$${\displaystyle \mu '}$${\displaystyle \exists x\phi (x)}$
5. Универсальные кванторы. Формула истинна согласно M, и если φ ( x ) истинно для каждой пары, составленной посредством интерпретации M и некоторого присвоения переменной, которое отличается только от значения x . Это отражает идею, которая верна, если каждый возможный выбор значения для x заставляет φ ( x ) быть истинным.${\displaystyle \forall x\phi (x)}$${\displaystyle \mu }$${\displaystyle \mu '}$${\displaystyle \mu }$${\displaystyle \forall x\phi (x)}$

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

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

1. Экзистенциальные кванторы (альтернативные). Формула истинна согласно M, если в области дискурса существует такое d , которое выполняется. Вот результат замены c _d на каждое свободное вхождение x в φ.${\displaystyle \exists x\phi (x)}$${\displaystyle \phi (c_{d})}$${\displaystyle \phi (c_{d})}$
2. Универсальные кванторы (альтернативные). Формула верна в соответствии с М , если для каждого г в области речи, правда , по любому из M .${\displaystyle \forall x\phi (x)}$${\displaystyle \phi (c_{d})}$

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

Действительность, выполнимость и логическое следствие [ править ]

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

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

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

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

Алгебраизации [ править ]

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

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

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

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

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

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

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

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

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

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

Пустые домены [ править ]

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

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

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

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

Дедуктивные системы [ править ]

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

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

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

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

Правила вывода [ править ]

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

Например, одним из общих правил вывода является правило подстановки . Если t - терм, а φ - формула, которая, возможно, содержит переменную x , то φ [ t / x ] - это результат замены всех свободных экземпляров x на t в φ. Правило подстановки гласит, что для любого φ и любого члена t можно вывести φ [ t / x ] из φ при условии, что никакая свободная переменная t не становится связанной в процессе замены. (Если некоторые свободные переменная т становится связанным, затем заменитель т по йсначала необходимо изменить связанные переменные функции φ, чтобы они отличались от свободных переменных функции 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 и универсальное обобщение .

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

Последовательное исчисление [ править ]

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

${\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})}$

Tableaux метод [ править ]

В отличие от только что описанных методов, производные в методе таблиц не являются списками формул. Вместо этого вывод - это дерево формул. Чтобы показать, что формула 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}$

Равенство и его аксиомы [ править ]

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

1. Рефлексивность . Для каждой переменной х , х = х .
2. Подмена функций. Для всех переменных х и у , и любого символа функции F ,

   x = y → f (..., 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 . ^[23]
2. Транзитивность. Если x = y и y = z, то x = z . ^[24]

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

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

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

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

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

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

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

• В теории частичных порядков с одним символом отношения ≤ можно определить s = t как сокращение для s ≤ t ∧ t ≤ s .
• В теории множеств с одним отношением ∈ можно определить s = t как сокращение для ∀ x ( s ∈ x ↔ t ∈ x ) ∧ ∀ x ( x ∈ s ↔ x ∈ t ). Тогда это определение равенства автоматически удовлетворяет аксиомам равенства. В этом случае следует заменить обычную аксиому экстенсиональности , которую можно сформулировать как , альтернативной формулировкой , в которой говорится, что если множества 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 годах, соответственно, дав отрицательный ответ на проблему Entscheidungs, поставленную Дэвидом Гильбертом и Вильгельмом Аккерманом.в 1928 году. Их доказательства демонстрируют связь между неразрешимостью проблемы решения для логики первого порядка и неразрешимостью проблемы остановки .

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

Теорема Левенхайма – Сколема [ править ]

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

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

Теорема компактности [ править ]

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

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

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

Теорема Линдстрема [ править ]

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

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

Ограничения [ править ]

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

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

Выразительность [ править ]

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

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

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

Ограничения, расширения и варианты [ править ]

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

Запрещенные языки [ править ]

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

• Потому что может быть выражено как , а может быть выражено как любой из двух квантификаторов и может быть опущено.${\displaystyle \exists x\phi (x)}$${\displaystyle \neg \forall x\neg \phi (x)}$${\displaystyle \forall x\phi (x)}$${\displaystyle \neg \exists x\neg \phi (x)}$${\displaystyle \exists }$${\displaystyle \forall }$
• Поскольку может быть выражено как и может быть выражено как , либо, либо можно опустить. Другими словами, достаточно иметь и , или и , как единственные логические связки.${\displaystyle \phi \lor \psi }$${\displaystyle \lnot (\lnot \phi \land \lnot \psi )}$${\displaystyle \phi \land \psi }$${\displaystyle \lnot (\lnot \phi \lor \lnot \psi )}$${\displaystyle \vee }$${\displaystyle \wedge }$${\displaystyle \neg }$${\displaystyle \vee }$${\displaystyle \neg }$${\displaystyle \wedge }$
• Аналогичным образом , достаточно иметь только и как логические связки, или иметь только штрих Шеффера (NAND) или Пирс стрелок оператора (НИ).${\displaystyle \neg }$${\displaystyle \rightarrow }$
• Можно полностью избежать функциональных символов и константных символов, переписав их соответствующим образом с помощью предикатных символов. Например, вместо использования постоянного символа один может использовать предикат (интерпретируется как ), и заменить каждый предикат , такой как с . Функция, такая как, будет заменена предикатом, интерпретируемым как . Это изменение требует добавления дополнительных аксиом к рассматриваемой теории, чтобы интерпретации используемых предикатных символов имели правильную семантику. ^[28]${\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, которые определяют функции проекции упорядоченной пары на ее компоненты. В любом случае необходимо, чтобы выполнялись естественные аксиомы для функции спаривания и ее проекций.

Многосортная логика [ править ]

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

Когда в теории есть только конечное число сортов, многосортированная логика первого порядка может быть сведена к односортированной логике первого порядка. ^{[30] : 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))}$.

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

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

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

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

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

Бесконечная логика [ править ]

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

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

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

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

Неклассическая и модальная логика [ править ]

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

Логика фиксированной точки [ править ]

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

Логика высшего порядка [ править ]

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

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

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

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

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

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

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

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

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

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

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

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

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

См. Также [ править ]

• ACL2 - вычислительная логика для аппликативного Common Lisp.
• Равносогласованность
• Расширение по определениям
• Расширение (логика предиката)
• Гербирование
• Логика высшего порядка
• Список логических символов
• Число Левенхайма
• Неупорядоченность
• Prenex нормальная форма
• Реляционная алгебра
• Реляционная модель
• Логика второго порядка
• Сколем нормальная форма
• Мир Тарского
• Таблица истинности
• Тип (теория модели)
• Пролог

Примечания [ править ]

Ссылки [ править ]

• Раутенберг, Вольфганг (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 , vol. 9 нет. 1 дой : 10.1145 / 1297658.1297660
• Барвайз, Джон (1977). «Введение в логику первого порядка» . В Барвайз, Джон (ред.). Справочник по математической логике . Исследования по логике и основам математики. Амстердам, Нидерланды: Северная Голландия (опубликовано в 1982 г.). ISBN 978-0-444-86388-1.
• Барвайз, Джон; и Этчменди, Джон (2000); Language Proof and Logic , Stanford, CA: CSLI Publications (Распространяется издательством Чикагского университета)
• Бохенский, Юзеф Мария (2007); A Précis of Mathematical Logic , Dordrecht, NL: D. Reidel, перевод с французского и немецкого изданий Отто Берда
• Феррейрос, Хосе (2001); Путь к современной логике - интерпретация ., Бюллетень символической логики, том 7, выпуск 4, 2001, стр 441-484, DOI : 10,2307 / 2687794 , JSTOR  2687794
• Gamut, LTF (1991), Логика, язык и значение, Том 2: Интенсивная логика и логическая грамматика , Чикаго, Иллинойс: University of Chicago Press, ISBN 0-226-28088-8
• Гильберт, Дэвид ; и Аккерман, Вильгельм (1950); Принципы математической логики , Chelsea (английский перевод Grundzüge der Theoretischen Logik , 1928, немецкое первое издание)
• Ходжес, Уилфрид (2001); «Классическая логика I: логика первого порядка», в Гобле, Лу (ред.); Руководство Блэквелла по философской логике , Блэквелл
• Эббингаус, Хайнц-Дитер ; Флум, Йорг; и Томас, Вольфганг (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, который преподается студентам бакалавриата (обычно) на третьем курсе. Курс называется «Логика, вычисление и теория множеств» и охватывает ординалы и кардиналы, Posets и лемму Цорна, логику высказываний, логику предикатов, теорию множеств и вопросы согласованности, связанные с ZFC и другими теориями множеств.
• Tree Proof Generator может проверять или аннулировать формулы логики первого порядка с помощью метода семантических таблиц .