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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

кванторов Символы $: \forall$ для количественной оценки универсальности и $\exists$ для количественной оценки существования.
Логические связки : $\land$ для конъюнкции , $\lor$ для дизъюнкции , $\to$ для импликации , $\leftrightarrow$ для двуусловия , $\neg$ для отрицания. Некоторые авторы ^[11]используйте C pq вместо $\to$ и E pq вместо $\leftrightarrow$ , особенно в контекстах, где → используется для других целей. Более того, подкова $\supset$ может заменить $\to$ ; ^[8]тройная черта $\equiv$ может заменить $\leftrightarrow$ ; тильда ( $~$ ), N p или F p может заменить $\neg$ ; двойной бар $\|$ , $+$ , ^[12]или A pq может заменить $\lor$ ; а амперсанд $&$ , K pq или средняя точка $\cdot$ могут заменить $\land$ , особенно если эти символы недоступны по техническим причинам. (Вышеупомянутые символы C pq , E pq , N p , A pq и K pq используются в польских обозначениях .)
Круглые скобки, квадратные скобки и другие знаки препинания. Выбор таких символов варьируется в зависимости от контекста.
Бесконечный набор переменных , часто обозначаемых строчными буквами в конце алфавита x , y , z ,.... Для различения переменных часто используются индексы: $x 0, x 1, x 2, ... .$
Символ равенства (иногда символ тождества ) $=$ (см. § Равенство и его аксиомы ниже).

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

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

Константы истинности: 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 . Символ а может обозначать Сократа. В арифметике это может означать 0. В теории множеств это может означать пустое множество .

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

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

БНФ- грамматика

<index>             ::= "" 
                      | <index> "'"
<variable>          ::= "x" <index>
<constant>          ::= "c" <index>
<unary function>    ::= "f1" <index>
<binary function>   ::= "f2" <index>
<ternary function>  ::= "f3" <index>
<unary predicate>   ::= "p1" <index>
<binary predicate>  ::= "p2" <index>
<ternary predicate> ::= "p3" <index>
<term>              ::= <variable> 
                      | <constant> 
                      | <unary function> "(" <term> ")" 
                      | <binary function> "(" <term> "," <term> ")" 
                      | <ternary function> "(" <term> "," <term> "," <term> ")"
<atomic formula>    ::= "TRUE" 
                      | "FALSE"
                      | <term> "=" <term>
                      | <unary predicate> "(" <term> ")" 
                      | <binary predicate> "(" <term> "," <term> ")" 
                      | <ternary predicate> "(" <term> "," <term> "," <term> ")"
<formula>           ::= <atomic formula> 
                      | "¬" <formula>
                      | <formula> "∧" <formula>
                      | <formula> "∨" <formula>
                      | <formula> "⇒" <formula>
                      | <formula> "⇔" <formula>
                      | "(" <formula> ")"
                      | "∀" <variable> <formula>
                      | "∃" <variable> <formula>

The above context-free grammar in Backus-Naur form defines the language of syntactically valid first-order formulas with function symbols and predicate symbols up to arity 3. For higher arities, it needs to be adapted accordingly.^[15]^{[citation needed]}

The example formula ∀x ∃x' (¬x=c) ⇒ f2(x,x')=c' describes multiplicative inverses when f2', c, and c' are interpreted as multiplication, zero, and one, respectively.

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

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

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

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

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

Formulas[editФормулы

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

Символы предикатов . Если P — n -арный символ-предикат и t ₁ , ..., t _n — термины, то P ( t ₁ ,..., t _n ) — формула.
Равенство . Если символ равенства считается частью логики, а t ₁ и t ₂ являются терминами, то t ₁ = t ₂ является формулой.
Отрицание . Если $\varphi$ это формула, то $\lnot \varphi$ это формула.
Бинарные связки . Если $\varphi$ и $\psi$ являются формулами, то ( $\varphi \rightarrow \psi$ ) — это формула. Аналогичные правила применимы и к другим двоичным логическим связкам.
Кванторы . Если $\varphi$ — формула, а x — переменная, то $\forall x\varphi$ (для всех х, $\varphi$ держится) и $\exists x\varphi$ (существует x такой, что $\varphi$ ) являются формулами.

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

Например:

\forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))

является формулой, если f — унарный символ функции, P — унарный символ предиката, а Q — троичный символ предиката. Однако, $\forall x\,x\rightarrow$ не является формулой, хотя представляет собой строку символов алфавита.

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

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

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

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

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

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

\lnot \forall xP(x)\to \exists x\lnot P(x)

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

(\lnot [\forall xP(x)])\to \exists x[\lnot P(x)].

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

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

\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 находится в пределах области действия хотя бы одного из $\exists x$ или $\forall x$ . Наконец, x связан в φ, если все вхождения x в φ связаны. ^[8]^{стр.142--143}

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

Атомные формулы: Если φ — атомарная формула, то x свободно встречается в φ тогда и только тогда, когда x встречается в φ . Более того, ни в одной атомарной формуле нет связанных переменных.
Отрицание: x встречается свободным в ¬ φ тогда и только тогда, когда x встречается свободным в φ . x встречается связанным в ¬ φ тогда и только тогда, когда x встречается связанным в φ
Бинарные связки: x встречается свободным в ( φ → ψ ) тогда и только тогда, когда x встречается свободным либо в φ , либо в ψ . x встречается связанным в ( φ → ψ ) тогда и только тогда, когда x встречается связанным либо в φ , либо в ψ . То же правило применяется к любой другой бинарной связке вместо →.
Кванторы: x встречается свободно в $\forall y φ$ тогда и только тогда, когда x встречается свободно в φ и x является символом, отличным от y . Кроме того, x встречается связанным в $\forall y φ$ тогда и только тогда, когда x есть y или x встречается связанным в φ . То же правило справедливо и для $\exists$ вместо $\forall$ .

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

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

Формула в логике первого порядка, в которой отсутствуют свободные переменные, называется первого порядка предложением . Это формулы, которые будут иметь четко определенные значения истинности при интерпретации. Например, истинность такой формулы, как Phil( x ), должна зависеть от того, что представляет собой x . Но предложение $\exists 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 .
Выражение $(\forall x\forall y\,[\mathop {\leq } (\mathop {+} (x,y),z)\to \forall x\,\forall y\,\mathop {+} (x,y)=0)]$ это формула , которую обычно записывают как $\forall x\forall y(x+y\leq z)\to \forall x\forall y(x+y=0).$ В этой формуле есть одна свободная переменная z .

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

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

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

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

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

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

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

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

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

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

Оценка истинностных значений [ править ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Чтобы понять, почему необходимо ограничение на связанные переменные, рассмотрим логически допустимую формулу φ, заданную формулой $\exists x(x=y)$ , в сигнатуре (0,1,+,×,=) арифметики. Если t является термином «x + 1», формула φ[ t / y ] имеет вид $\exists x(x=x+1)$ , что будет ложным во многих интерпретациях. Проблема в том, что свободная переменная x в t во время замены стала связанной. Предполагаемую замену можно получить, переименовав связанную переменную x функции φ во что-нибудь другое, скажем, z , так что формула после замены будет иметь вид $\exists z(z=x+1)$ , что опять-таки логически верно.

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

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

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

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

Расчеты следуют [ править ]

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

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

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

Табличный метод [ править ]

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

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

Разрешение [ править ]

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

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

Доказуемые личности [ править ]

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

\lnot \forall x\,P(x)\Leftrightarrow \exists x\,\lnot P(x)

\lnot \exists x\,P(x)\Leftrightarrow \forall x\,\lnot P(x)

\forall x\,\forall y\,P(x,y)\Leftrightarrow \forall y\,\forall x\,P(x,y)

\exists x\,\exists y\,P(x,y)\Leftrightarrow \exists y\,\exists x\,P(x,y)

\forall x\,P(x)\land \forall x\,Q(x)\Leftrightarrow \forall x\,(P(x)\land Q(x))

\exists x\,P(x)\lor \exists x\,Q(x)\Leftrightarrow \exists x\,(P(x)\lor Q(x))

P\land \exists x\,Q(x)\Leftrightarrow \exists x\,(P\land Q(x))

(где

x

не должно происходить свободно в

P

)

P\lor \forall x\,Q(x)\Leftrightarrow \forall x\,(P\lor Q(x))

(где

x

не должно происходить свободно в

P

)

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

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

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

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

Икс знак равно у → ( ж (..., Икс , ...) знак равно z → ж (..., у , ...) знак равно z ).

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

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

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

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

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

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

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

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

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

В теории частичных порядков с одним символом отношения ≤ можно определить s = t как аббревиатуру для s ≤ t ∧ t ≤ s .
В теории множеств с одним отношением ∈ можно определить s = t как аббревиатуру для $\forall x (s \in x \leftrightarrow t \in x) \land \forall x (x \in s \leftrightarrow x \in t)$ . Тогда это определение равенства автоматически удовлетворяет аксиомам равенства. В этом случае следует заменить обычную аксиому экстенсиональности , которую можно сформулировать как $\forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow x=y]$ , с альтернативной формулировкой $\forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow \forall z(x\in z\Leftrightarrow y\in z)]$ , который говорит, что если множества x и y состоят из одних и тех же элементов, то они также принадлежат одним и тем же множествам.

Металогические свойства [ править ]

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

Полнота и неразрешимость [ править ]

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

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

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

Левенхайма Скулема Теорема –

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Тип	Пример	Комментарий
Количественная оценка по свойствам	Если Джон самодоволен, то есть, по крайней мере, что-то общее, что у него есть с Петром.	В примере требуется квантификатор для предикатов, который не может быть реализован в логике первого порядка с одинарной сортировкой: Zj → ∃X(Xj∧Xp) .
Количественная оценка по свойствам	Дед Мороз обладает всеми атрибутами садиста.	В примере требуются кванторы над предикатами, которые не могут быть реализованы в логике первого порядка с одинарной сортировкой: ∀X(∀x(Sx → Xx) → Xs) .
Предикат наречие	Джон идет быстро.	Пример не может быть проанализирован как Wj ∧ Qj ; Наречия предикатов — это не то же самое, что предикаты второго порядка, такие как цвет.
Относительное прилагательное	Джамбо – маленький слон.	Пример не может быть проанализирован как Sj ∧ Нет ; Прилагательные-сказуемые — это не то же самое, что предикаты второго порядка, такие как цвет.
Деепричастный модификатор сказуемого	Джон идет очень быстро.	—
Модификатор относительного прилагательного	Джамбо ужасно маленький.	Такое выражение, как «ужасно», при применении к относительному прилагательному, например «маленький», приводит к новому составному относительному прилагательному «ужасно маленький».
Предлоги	Мэри сидит рядом с Джоном.	Предлог «рядом с» при применении к «Джону» приводит к образованию предиката-наречия «рядом с Джоном».

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

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

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

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

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

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

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

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

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

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

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

.

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

\exists x(P_{1}(x)\land \varphi (x))

.

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

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

Иногда полезно сказать, что « $P (x)$ выполняется ровно для одного x », что можно выразить как $\exists! Икс П (Икс)$ . Это обозначение, называемое количественной оценкой уникальности , может быть использовано для сокращения такой формулы, как $\exists x (P (x) \land \forall y (P (y) \to (x = y)))$ .
Логика первого порядка с дополнительными кванторами имеет новые кванторы Qx ,... со значениями типа «есть много x таких, что ...». См. также кванторы ветвления и кванторы множественного числа Джорджа Булоса и других.
Ограниченные кванторы часто используются при изучении теории множеств или арифметики.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

^ Ходжсон, доктор JPE, «Логика первого порядка» ( archive.org ), Университет Святого Иосифа , Филадельфия , 1995.
^ Хьюз, GE , и Крессвелл, MJ , Новое введение в модальную логику ( Лондон : Routledge , 1996), стр.161 .
^ Перейти обратно: ^а ^б А. Тарский, Неразрешимые теории (1953), с.77. Исследования в области логики и основы математики, Северная Голландия
^ Мендельсон, Эллиотт (1964). Введение в математическую логику . Ван Ностранд Рейнхольд . п. 56 .
^ Эрик М. Хаммер: Семантика экзистенциальных графов, Журнал философской логики , том 27, выпуск 5 (октябрь 1998 г.), стр. 489: «Развитие логики первого порядка независимо от Фреге, предвосхищая пренекс и скулемские нормальные формы»
^ Х. Фридман, « Приключения в основах математики 1: Логические рассуждения », Программа Росса 2022, конспекты лекций. По состоянию на 28 июля 2023 г.
^ Герцель Б. , Гейсвайлер Н., Коэльо Л., Яничич П. и Пенначин К., Рассуждения в реальном мире: к масштабируемым, неопределенным пространственно-временным, контекстуальным и причинным выводам ( Амстердам и Париж : Atlantis Press , 2011), стр. 29--30 .
^ Перейти обратно: ^а ^б ^с ^д ^Это У.В.О. Куайн, Математическая логика (1981). Издательство Гарвардского университета, 0-674-55451-5.
^ Дэвис, Эрнест (1990). Репрезентации здравого знания . Морган Кауфман. стр. 27–28. ISBN 978-1-4832-0770-4 .
^ «Логика предикатов | Блестящая математическая и научная вики» . блестящий.орг . Проверено 20 августа 2020 г.
^ «Введение в символическую логику: Лекция 2» . cstl-cla.semo.edu . Проверено 4 января 2021 г.
^ Ганс Гермес (1973). Введение в математическую логику . Hochschultext (Springer-Verlag). Лондон: Спрингер. ISBN 3540058192 . ISSN 1431-4657 .
^ Точнее, существует только один язык каждого варианта односортной логики первого порядка: с равенством или без него, с функциями или без них, с пропозициональными переменными или без них, ....
^ Слово «язык» иногда используется как синоним подписи, но это может сбивать с толку, поскольку «язык» также может относиться к набору формул.
^ Эберхард Бергманн и Хельга Нолл (1977). Математическая логика с приложениями в области информатики . Гейдельбергские книги в мягкой обложке, сборник информатики (на немецком языке). Том 187. Гейдельберг: Springer. стр. 300–302 .
^ Смуллян, Р.М. , Логика первого порядка ( Нью-Йорк : Dover Publications , 1968), стр. 5 .
^ Г. Такеути, «Теория доказательств» (1989, стр.6)
^ Некоторые авторы, использующие термин «правильная формула», используют «формулу» для обозначения любой строки символов из алфавита. Однако большинство авторов по математической логике используют слово «формула» для обозначения «правильно составленной формулы» и не имеют термина для обозначения неправильно составленных формул. В любом контексте интерес представляют только правильно составленные формулы.
^ Кларк Барретт; Аарон Стамп; Чезаре Тинелли. «Стандарт SMT-LIB: Версия 2.0» . СМТ-ЛИБ . Проверено 15 июня 2019 г.
^ y встречается в соответствии с правилом 4, хотя он не появляется ни в одной атомарной подформуле.
^ Кажется, этот символ $\vDash$ был введен Клини, см. сноску 30 в переиздании Довером его книги «Математическая логика» в 2002 году, John Wiley and Sons, 1967.
^ Ф. Р. Дрейк, Теория множеств: введение в большие кардиналы (1974)
^ Роджерс, Р.Л., Математическая логика и формализованные теории: обзор основных концепций и результатов (Амстердам/Лондон: издательство North-Holland Publishing Company , 1971), стр. 39 .
^ Бринк, К. , Каль, В., и Шмидт, Г. , ред., Реляционные методы в информатике ( Берлин / Гейдельберг : Springer , 1997), стр. 32–33 .
^ Anon., Mathematical Reviews ( Провиденс : Американское математическое общество , 2006), стр. 803.
^ Шанкар, Н. , Оуре, С., Рашби, Дж. М. и Стрингер-Калверт, DWJ, Руководство по проверке PVS 7.1 ( Менло-Парк : SRI International , август 2020 г.).
^ Фиттинг, М. , Логика первого порядка и автоматическое доказательство теорем (Берлин/Гейдельберг: Springer, 1990), стр. 198–200 .
^ Используйте замену формулы, где φ равно x = x и φ' равно y = x , затем используйте рефлексивность.
^ Используйте замену формулы, где φ равно y = z , а φ' равно x = z , чтобы получить y = x → ( y = z → x = z ), затем используйте симметрию и некаррирование .
^ Ходел, Р.Э., Введение в математическую логику ( Минеола, штат Нью-Йорк : Дувр , 1995), стр. 199 .
^ Хоррокс, Ян (2010). «Логика описания: формальная основа языков и инструментов» (PDF) . Слайд 22. Архивировано (PDF) из оригинала 6 сентября 2015 г.
^ Гамут 1991 , с. 75.
^ Левая тотальность может быть выражена аксиомой $\forall x_{1},...,x_{n}.\exists y.F(x_{1},...,x_{n},y)$ ; праву единственность по $\forall x_{1},...,x_{n},y,y'.$ $F(x_{1},...,x_{n},y)\land F(x_{1},...,x_{n},y')\rightarrow y=y'$ , при условии, что допускается символ равенства. Оба также применимы к постоянным заменам (для $n=0$ ).
^ Ускиано, Габриэль (17 октября 2018 г.). «Кванторы и квантификация» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии (изд. Зима 2018 г.). См., в частности, раздел 3.2 «Многосортированная количественная оценка».
^ Эндертон, Х. Математическое введение в логику , второе издание. Академик Пресс , 2001, стр. 296–299 .
^ Некоторые авторы допускают только формулы с конечным числом свободных переменных в L _κω и, в более общем плане, только формулы с < λ свободными переменными в L _κλ .
^ Боссе, Уве (1993). «Игра Эренфойхта – Фрэссе для логики с фиксированной точкой и стратифицированной логики с фиксированной точкой». В Бёргере, Эгон (ред.). Логика информатики: 6-й семинар, CSL'92, Сан-Миниато, Италия, 28 сентября - 2 октября 1992 г. Избранные статьи . Конспекты лекций по информатике. Том. 702. Шпрингер-Верлаг . стр. 100–114. ISBN 3-540-56992-8 . Збл 0808.03024 .
^ Мелвин Фиттинг (6 декабря 2012 г.). Логика первого порядка и автоматическое доказательство теорем . Springer Science & Business Media. ISBN 978-1-4612-2360-3 .
^ «15-815 Автоматическое доказательство теорем» . www.cs.cmu.edu . Проверено 10 января 2024 г.
^ Авигад и др. (2007) обсуждают процесс формальной проверки доказательства теоремы о простых числах . Формализованное доказательство потребовало около 30 000 строк ввода в верификатор доказательства Изабель.

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

Раутенберг, Вольфганг (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 .
Монк, Дж. Дональд (1976). Математическая логика . Нью-Йорк, штат Нью-Йорк: Springer New York. дои : 10.1007/978-1-4684-9452-5 . ISBN 978-1-4684-9454-9 .
Барвайз, Джон; и Этчеменди, Джон (2000); Языковое доказательство и логика , Стэнфорд, Калифорния: Публикации CSLI (распространяются издательством Чикагского университета)
Боченский, Юзеф Мария (2007); Краткое изложение математической логики , Дордрехт, Нидерланды: Д. Рейдель, перевод с французского и немецкого изданий Отто Берда.
Феррейрос, Хосе (2001); Дорога к современной логике — интерпретация , Бюллетень символической логики, том 7, выпуск 4, 2001, стр. 441–484, дои : 10.2307/2687794 , JSTOR 2687794
Гамут, LTF (1991), Логика, язык и значение, Том 2: Интенсиональная логика и логическая грамматика , Чикаго, Иллинойс: University of Chicago Press, ISBN 0-226-28088-8
Гильберт, Дэвид ; и Акерманн, Вильгельм (1950); Принципы математической логики , Челси (английский перевод « Основ теоретической логики» , первое издание на немецком языке, 1928 г.)
Ходжес, Уилфрид (2001); «Классическая логика I: логика первого порядка», Гобл, Лу (ред.); Руководство Блэквелла по философской логике , Блэквелл
Эббингауз, Хайнц-Дитер ; Флум, Йорг; и Томас, Вольфганг (1994); Математическая логика , Тексты для студентов по математике , Берлин, Делавэр/Нью-Йорк, Нью-Йорк: Springer-Verlag , Второе издание, ISBN 978-0-387-94258-2
Тарский, Альфред и Гивант, Стивен (1987); Формализация теории множеств без переменных . Том 41 публикаций коллоквиума Американского математического общества, Провиденс, Род-Айленд: Американское математическое общество, ISBN 978-0821810415

Внешние ссылки [ править ]

«Исчисление предикатов» , Математическая энциклопедия , EMS Press , 2001 [1994]
Стэнфордская энциклопедия философии : Шапиро, Стюарт; « Классическая логика ». Охватывает синтаксис, теорию моделей и метатеорию логики первого порядка в стиле естественной дедукции.
Magnus, P. D.; forall x: an introduction to formal logic. Covers formal semantics and proof theory for first-order logic.
Metamath: an ongoing online project to reconstruct mathematics as a huge first-order theory, using first-order logic and the axiomatic set theory ZFC. Principia Mathematica modernized.
Podnieks, Karl; Introduction to mathematical logic
Cambridge Mathematical Tripos notes (typeset by John Fremlin). These notes cover part of a past Cambridge Mathematical Tripos course taught to undergraduate students (usually) within their third year. The course is entitled "Logic, Computation and Set Theory" and covers Ordinals and cardinals, Posets and Zorn's Lemma, Propositional logic, Predicate logic, Set theory and Consistency issues related to ZFC and other set theories.
Tree Proof Generator can validate or invalidate formulas of first-order logic through the semantic tableaux method.

[1] Ходжсон, доктор JPE, «Логика первого порядка» ( archive.org ), Университет Святого Иосифа , Филадельфия , 1995.

[2] Хьюз, GE , и Крессвелл, MJ , Новое введение в модальную логику ( Лондон : Routledge , 1996), стр.161 .

[Tarski53-3] Перейти обратно: ^а ^б А. Тарский, Неразрешимые теории (1953), с.77. Исследования в области логики и основы математики, Северная Голландия

[4] Мендельсон, Эллиотт (1964). Введение в математическую логику . Ван Ностранд Рейнхольд . п. 56 .

[5] Эрик М. Хаммер: Семантика экзистенциальных графов, Журнал философской логики , том 27, выпуск 5 (октябрь 1998 г.), стр. 489: «Развитие логики первого порядка независимо от Фреге, предвосхищая пренекс и скулемские нормальные формы»

[6] Х. Фридман, « Приключения в основах математики 1: Логические рассуждения », Программа Росса 2022, конспекты лекций. По состоянию на 28 июля 2023 г.

[7] Герцель Б. , Гейсвайлер Н., Коэльо Л., Яничич П. и Пенначин К., Рассуждения в реальном мире: к масштабируемым, неопределенным пространственно-временным, контекстуальным и причинным выводам ( Амстердам и Париж : Atlantis Press , 2011), стр. 29--30 .

[Quine81-8] Перейти обратно: ^а ^б ^с ^д ^Это У.В.О. Куайн, Математическая логика (1981). Издательство Гарвардского университета, 0-674-55451-5.

[9] Дэвис, Эрнест (1990). Репрезентации здравого знания . Морган Кауфман. стр. 27–28. ISBN 978-1-4832-0770-4 .

[10] «Логика предикатов | Блестящая математическая и научная вики» . блестящий.орг . Проверено 20 августа 2020 г.

[11] «Введение в символическую логику: Лекция 2» . cstl-cla.semo.edu . Проверено 4 января 2021 г.

[12] Ганс Гермес (1973). Введение в математическую логику . Hochschultext (Springer-Verlag). Лондон: Спрингер. ISBN 3540058192 . ISSN 1431-4657 .

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

[14] Слово «язык» иногда используется как синоним подписи, но это может сбивать с толку, поскольку «язык» также может относиться к набору формул.

[15] Эберхард Бергманн и Хельга Нолл (1977). Математическая логика с приложениями в области информатики . Гейдельбергские книги в мягкой обложке, сборник информатики (на немецком языке). Том 187. Гейдельберг: Springer. стр. 300–302 .

[16] Смуллян, Р.М. , Логика первого порядка ( Нью-Йорк : Dover Publications , 1968), стр. 5 .

[17] Г. Такеути, «Теория доказательств» (1989, стр.6)

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

[19] Кларк Барретт; Аарон Стамп; Чезаре Тинелли. «Стандарт SMT-LIB: Версия 2.0» . СМТ-ЛИБ . Проверено 15 июня 2019 г.

[20] y встречается в соответствии с правилом 4, хотя он не появляется ни в одной атомарной подформуле.

[21] Кажется, этот символ $\vDash$ был введен Клини, см. сноску 30 в переиздании Довером его книги «Математическая логика» в 2002 году, John Wiley and Sons, 1967.

[22] Ф. Р. Дрейк, Теория множеств: введение в большие кардиналы (1974)

[23] Роджерс, Р.Л., Математическая логика и формализованные теории: обзор основных концепций и результатов (Амстердам/Лондон: издательство North-Holland Publishing Company , 1971), стр. 39 .

[24] Бринк, К. , Каль, В., и Шмидт, Г. , ред., Реляционные методы в информатике ( Берлин / Гейдельберг : Springer , 1997), стр. 32–33 .

[25] Anon., Mathematical Reviews ( Провиденс : Американское математическое общество , 2006), стр. 803.

[26] Шанкар, Н. , Оуре, С., Рашби, Дж. М. и Стрингер-Калверт, DWJ, Руководство по проверке PVS 7.1 ( Менло-Парк : SRI International , август 2020 г.).

[27] Фиттинг, М. , Логика первого порядка и автоматическое доказательство теорем (Берлин/Гейдельберг: Springer, 1990), стр. 198–200 .

[28] Используйте замену формулы, где φ равно x = x и φ' равно y = x , затем используйте рефлексивность.

[29] Используйте замену формулы, где φ равно y = z , а φ' равно x = z , чтобы получить y = x → ( y = z → x = z ), затем используйте симметрию и некаррирование .

[30] Ходел, Р.Э., Введение в математическую логику ( Минеола, штат Нью-Йорк : Дувр , 1995), стр. 199 .

[31] Хоррокс, Ян (2010). «Логика описания: формальная основа языков и инструментов» (PDF) . Слайд 22. Архивировано (PDF) из оригинала 6 сентября 2015 г.

[FOOTNOTEGamut199175-32] Гамут 1991 , с. 75.

[33] Левая тотальность может быть выражена аксиомой $\forall x_{1},...,x_{n}.\exists y.F(x_{1},...,x_{n},y)$ ; праву единственность по $\forall x_{1},...,x_{n},y,y'.$ $F(x_{1},...,x_{n},y)\land F(x_{1},...,x_{n},y')\rightarrow y=y'$ , при условии, что допускается символ равенства. Оба также применимы к постоянным заменам (для $n=0$ ).

[34] Ускиано, Габриэль (17 октября 2018 г.). «Кванторы и квантификация» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии (изд. Зима 2018 г.). См., в частности, раздел 3.2 «Многосортированная количественная оценка».

[35] Эндертон, Х. Математическое введение в логику , второе издание. Академик Пресс , 2001, стр. 296–299 .

[36] Некоторые авторы допускают только формулы с конечным числом свободных переменных в L _κω и, в более общем плане, только формулы с < λ свободными переменными в L _κλ .

[37] Боссе, Уве (1993). «Игра Эренфойхта – Фрэссе для логики с фиксированной точкой и стратифицированной логики с фиксированной точкой». В Бёргере, Эгон (ред.). Логика информатики: 6-й семинар, CSL'92, Сан-Миниато, Италия, 28 сентября - 2 октября 1992 г. Избранные статьи . Конспекты лекций по информатике. Том. 702. Шпрингер-Верлаг . стр. 100–114. ISBN 3-540-56992-8 . Збл 0808.03024 .

[Fitting2012-38] Мелвин Фиттинг (6 декабря 2012 г.). Логика первого порядка и автоматическое доказательство теорем . Springer Science & Business Media. ISBN 978-1-4612-2360-3 .

[39] «15-815 Автоматическое доказательство теорем» . www.cs.cmu.edu . Проверено 10 января 2024 г.

[40] Авигад и др. (2007) обсуждают процесс формальной проверки доказательства теоремы о простых числах . Формализованное доказательство потребовало около 30 000 строк ввода в верификатор доказательства Изабель.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

[37]

[38]

[39]

[40]