First-order logic

"Predicate logic" redirects here. First-order logic_sentence_0

For logics admitting predicate or function variables, see Higher-order logic. First-order logic_sentence_1

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic_sentence_2

First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. First-order logic_sentence_3

This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic. First-order logic_sentence_4

A theory about a topic is usually a first-order logic together with a specified domain of discourse (over which the quantified variables range), finitely many functions from that domain to itself, finitely many predicates defined on that domain, and a set of axioms believed to hold about them. First-order logic_sentence_5

Sometimes, "theory" is understood in a more formal sense, which is just a set of sentences in first-order logic. First-order logic_sentence_6

The adjective "first-order" distinguishes first-order logic from higher-order logic, in which there are predicates having predicates or functions as arguments, or in which one or both of predicate quantifiers or function quantifiers are permitted. First-order logic_sentence_7

In first-order theories, predicates are often associated with sets. First-order logic_sentence_8

In interpreted higher-order theories, predicates may be interpreted as sets of sets. First-order logic_sentence_9

There are many deductive systems for first-order logic which are both sound (i.e., all provable statements are true in all models) and complete (i.e. all statements which are true in all models are provable). First-order logic_sentence_10

Although the logical consequence relation is only semidecidable, much progress has been made in automated theorem proving in first-order logic. First-order logic_sentence_11

First-order logic also satisfies several metalogical theorems that make it amenable to analysis in proof theory, such as the Löwenheim–Skolem theorem and the compactness theorem. First-order logic_sentence_12

First-order logic is the standard for the formalization of mathematics into axioms, and is studied in the foundations of mathematics. First-order logic_sentence_13

Peano arithmetic and Zermelo–Fraenkel set theory are axiomatizations of number theory and set theory, respectively, into first-order logic. First-order logic_sentence_14

No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the natural numbers or the real line. First-order logic_sentence_15

Axiom systems that do fully describe these two structures (that is, categorical axiom systems) can be obtained in stronger logics such as second-order logic. First-order logic_sentence_16

The foundations of first-order logic were developed independently by Gottlob Frege and Charles Sanders Peirce. First-order logic_sentence_17

For a history of first-order logic and how it came to dominate formal logic, see José Ferreirós (2001). First-order logic_sentence_18

Introduction First-order logic_section_0

While propositional logic deals with simple declarative propositions, first-order logic additionally covers predicates and quantification. First-order logic_sentence_19

A predicate takes an entity or entities in the domain of discourse as input while outputs are either True or False. First-order logic_sentence_20

Consider the two sentences "Socrates is a philosopher" and "Plato is a philosopher". First-order logic_sentence_21

In propositional logic, these sentences are viewed as being unrelated, and might be denoted, for example, by variables such as p and q. First-order logic_sentence_22

The predicate "is a philosopher" occurs in both sentences, which have a common structure of "a is a philosopher". First-order logic_sentence_23

The variable a is instantiated as "Socrates" in the first sentence, and is instantiated as "Plato" in the second sentence. First-order logic_sentence_24

While first-order logic allows for the use of predicates, such as "is a philosopher" in this example, propositional logic does not. First-order logic_sentence_25

Relationships between predicates can be stated using logical connectives. First-order logic_sentence_26

Consider, for example, the first-order formula "if a is a philosopher, then a is a scholar". First-order logic_sentence_27

This formula is a conditional statement with "a is a philosopher" as its hypothesis, and "a is a scholar" as its conclusion. First-order logic_sentence_28

The truth of this formula depends on which object is denoted by a, and on the interpretations of the predicates "is a philosopher" and "is a scholar". First-order logic_sentence_29

Quantifiers can be applied to variables in a formula. First-order logic_sentence_30

The variable a in the previous formula can be universally quantified, for instance, with the first-order sentence "For every a, if a is a philosopher, then a is a scholar". First-order logic_sentence_31

The universal quantifier "for every" in this sentence expresses the idea that the claim "if a is a philosopher, then a is a scholar" holds for all choices of a. First-order logic_sentence_32

The negation of the sentence "For every a, if a is a philosopher, then a is a scholar" is logically equivalent to the sentence "There exists a such that a is a philosopher and a is not a scholar". First-order logic_sentence_33

The existential quantifier "there exists" expresses the idea that the claim "a is a philosopher and a is not a scholar" holds for some choice of a. First-order logic_sentence_34

The predicates "is a philosopher" and "is a scholar" each take a single variable. First-order logic_sentence_35

In general, predicates can take several variables. First-order logic_sentence_36

In the first-order sentence "Socrates is the teacher of Plato", the predicate "is the teacher of" takes two variables. First-order logic_sentence_37

An interpretation (or model) of a first-order formula specifies what each predicate means, and the entities that can instantiate the variables. First-order logic_sentence_38

These entities form the domain of discourse or universe, which is usually required to be a nonempty set. First-order logic_sentence_39

For example, in an interpretation with the domain of discourse consisting of all human beings and the predicate "is a philosopher" understood as "was the author of the Republic", the sentence "There exists a such that a is a philosopher" is seen as being true, as witnessed by Plato. First-order logic_sentence_40

Syntax First-order logic_section_1

There are two key parts of first-order logic. First-order logic_sentence_41

The syntax determines which finite sequences of symbols are well-formed expressions in first-order logic, while the semantics determines the meanings behind these expressions. First-order logic_sentence_42

Alphabet First-order logic_section_2

Unlike natural languages, such as English, the language of first-order logic is completely formal, so that it can be mechanically determined whether a given expression is well formed. First-order logic_sentence_44

There are two key types of well-formed expressions: terms, which intuitively represent objects, and formulas, which intuitively express predicates that can be true or false. First-order logic_sentence_45

The terms and formulas of first-order logic are strings of symbols, where all the symbols together form the alphabet of the language. First-order logic_sentence_46

As with all formal languages, the nature of the symbols themselves is outside the scope of formal logic; they are often regarded simply as letters and punctuation symbols. First-order logic_sentence_47

Logical symbols First-order logic_section_3

There are several logical symbols in the alphabet, which vary by author but usually include: First-order logic_sentence_48

First-order logic_unordered_list_0

• The quantifier symbols: for universal quantification, and for existential quantificationFirst-order logic_item_0_0
• The logical connectives: ∧ for conjunction, ∨ for disjunction, → for implication, ↔ for biconditional, ¬ for negation. Occasionally other logical connective symbols are included. Some authors use Cpq, instead of →, and Epq, instead of ↔, especially in contexts where → is used for other purposes. Moreover, the horseshoe ⊃ may replace →; the triple-bar ≡ may replace ↔; a tilde (~), Np, or Fp, may replace ¬; a double bar ||, + or Apq may replace ∨; and ampersand &, Kpq, or the middle dot, ⋅, may replace ∧, especially if these symbols are not available for technical reasons. (The aforementioned symbols Cpq, Epq, Np, Apq, and Kpq are used in Polish notation.)First-order logic_item_0_1
• Parentheses, brackets, and other punctuation symbols. The choice of such symbols varies depending on context.First-order logic_item_0_2
• An infinite set of variables, often denoted by lowercase letters at the end of the alphabet x, y, z, ... . Subscripts are often used to distinguish variables: x0, x1, x2, ... .First-order logic_item_0_3
• An equality symbol (sometimes, identity symbol) =; see the section on equality below.First-order logic_item_0_4

Not all of these symbols are required–only one of the quantifiers, negation and conjunction, variables, brackets and equality suffice. First-order logic_sentence_49

There are numerous minor variations that may define additional logical symbols: First-order logic_sentence_50

First-order logic_unordered_list_1

• In some occasions, the truth constants T, Vpq, or ⊤, for "true" and F, Opq, or ⊥, for "false" are included. Without any such logical operators of valence 0, these two constants can only be expressed using quantifiers.First-order logic_item_1_5
• In other occasions, additional logical connectives are included, such as the Sheffer stroke, Dpq (NAND), and exclusive or, Jpq.First-order logic_item_1_6

Non-logical symbols First-order logic_section_4

The non-logical symbols represent predicates (relations), functions and constants on the domain of discourse. First-order logic_sentence_51

It used to be standard practice to use a fixed, infinite set of non-logical symbols for all purposes. First-order logic_sentence_52

A more recent practice is to use different non-logical symbols according to the application one has in mind. First-order logic_sentence_53

Therefore, it has become necessary to name the set of all non-logical symbols used in a particular application. First-order logic_sentence_54

This choice is made via a signature. First-order logic_sentence_55

The traditional approach is to have only one, infinite, set of non-logical symbols (one signature) for all applications. First-order logic_sentence_56

Consequently, under the traditional approach there is only one language of first-order logic. First-order logic_sentence_57

This approach is still common, especially in philosophically oriented books. First-order logic_sentence_58

First-order logic_ordered_list_2

1. For every integer n ≥ 0, there is a collection of n-ary, or n-place, predicate symbols. Because they represent relations between n elements, they are also called relation symbols. For each arity n, we have an infinite supply of them:First-order logic_item_2_7
• P0, P1, P2, P3, ...First-order logic_item_2_8
2. For every integer n ≥ 0, there are infinitely many n-ary function symbols:First-order logic_item_2_9
• f0, f1, f2, f3, ...First-order logic_item_2_10

In contemporary mathematical logic, the signature varies by application. First-order logic_sentence_59

Typical signatures in mathematics are {1, ×} or just {×} for groups, or {0, 1, +, ×, <} for ordered fields. First-order logic_sentence_60

There are no restrictions on the number of non-logical symbols. First-order logic_sentence_61

The signature can be empty, finite, or infinite, even uncountable. First-order logic_sentence_62

Uncountable signatures occur for example in modern proofs of the Löwenheim–Skolem theorem. First-order logic_sentence_63

In this approach, every non-logical symbol is of one of the following types. First-order logic_sentence_64

First-order logic_ordered_list_3

1. A predicate symbol (or relation symbol) with some valence (or arity, number of arguments) greater than or equal to 0. These are often denoted by uppercase letters such as P, Q and R.First-order logic_item_3_11
• Relations of valence 0 can be identified with propositional variables. For example, P, which can stand for any statement.First-order logic_item_3_12
• For example, P(x) is a predicate variable of valence 1. One possible interpretation is "x is a man".First-order logic_item_3_13
• Q(x,y) is a predicate variable of valence 2. Possible interpretations include "x is greater than y" and "x is the father of y".First-order logic_item_3_14
2. A function symbol, with some valence greater than or equal to 0. These are often denoted by lowercase roman letters such as f, g and h.First-order logic_item_3_15
• Examples: f(x) may be interpreted as for "the father of x". In arithmetic, it may stand for "-x". In set theory, it may stand for "the power set of x". In arithmetic, g(x,y) may stand for "x+y". In set theory, it may stand for "the union of x and y".First-order logic_item_3_16
• Function symbols of valence 0 are called constant symbols, and are often denoted by lowercase letters at the beginning of the alphabet such as a, b and c. The symbol a may stand for Socrates. In arithmetic, it may stand for 0. In set theory, such a constant may stand for the empty set.First-order logic_item_3_17

The traditional approach can be recovered in the modern approach, by simply specifying the "custom" signature to consist of the traditional sequences of non-logical symbols. First-order logic_sentence_65

Formation rules First-order logic_section_5

First-order logic_table_general_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>First-order logic_cell_0_1_0
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.First-order logic_cell_0_2_0
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.First-order logic_cell_0_3_0

The formation rules define the terms and formulas of first-order logic. First-order logic_sentence_66

When terms and formulas are represented as strings of symbols, these rules can be used to write a formal grammar for terms and formulas. First-order logic_sentence_67

These rules are generally context-free (each production has a single symbol on the left side), except that the set of symbols may be allowed to be infinite and there may be many start symbols, for example the variables in the case of terms. First-order logic_sentence_68

Terms First-order logic_section_6

The set of terms is inductively defined by the following rules: First-order logic_sentence_69

First-order logic_ordered_list_4

1. Variables. Any variable is a term.First-order logic_item_4_18
2. Functions. Any expression f(t1,...,tn) of n arguments (where each argument ti is a term and f is a function symbol of valence n) is a term. In particular, symbols denoting individual constants are nullary function symbols, and thus are terms.First-order logic_item_4_19

Only expressions which can be obtained by finitely many applications of rules 1 and 2 are terms. First-order logic_sentence_70

For example, no expression involving a predicate symbol is a term. First-order logic_sentence_71

Formulas First-order logic_section_7

The set of formulas (also called well-formed formulas or WFFs) is inductively defined by the following rules: First-order logic_sentence_72

Only expressions which can be obtained by finitely many applications of rules 1–5 are formulas. First-order logic_sentence_73

The formulas obtained from the first two rules are said to be atomic formulas. First-order logic_sentence_74

For example, First-order logic_sentence_75

The role of the parentheses in the definition is to ensure that any formula can only be obtained in one way—by following the inductive definition (i.e., there is a unique parse tree for each formula). First-order logic_sentence_76

This property is known as unique readability of formulas. First-order logic_sentence_77

There are many conventions for where parentheses are used in formulas. First-order logic_sentence_78

For example, some authors use colons or full stops instead of parentheses, or change the places in which parentheses are inserted. First-order logic_sentence_79

Each author's particular definition must be accompanied by a proof of unique readability. First-order logic_sentence_80

This definition of a formula does not support defining an if-then-else function ite(c, a, b), where "c" is a condition expressed as a formula, that would return "a" if c is true, and "b" if it is false. First-order logic_sentence_81

This is because both predicates and functions can only accept terms as parameters, but the first parameter is a formula. First-order logic_sentence_82

Some languages built on first-order logic, such as SMT-LIB 2.0, add this. First-order logic_sentence_83

Notational conventions First-order logic_section_8

For convenience, conventions have been developed about the precedence of the logical operators, to avoid the need to write parentheses in some cases. First-order logic_sentence_84

These rules are similar to the order of operations in arithmetic. First-order logic_sentence_85

A common convention is: First-order logic_sentence_86

Moreover, extra punctuation not required by the definition may be inserted—to make formulas easier to read. First-order logic_sentence_87

Thus the formula First-order logic_sentence_88

might be written as First-order logic_sentence_89

In some fields, it is common to use infix notation for binary relations and functions, instead of the prefix notation defined above. First-order logic_sentence_90

For example, in arithmetic, one typically writes "2 + 2 = 4" instead of "=(+(2,2),4)". First-order logic_sentence_91

It is common to regard formulas in infix notation as abbreviations for the corresponding formulas in prefix notation, cf. First-order logic_sentence_92

also term structure vs. representation. First-order logic_sentence_93

becomes "∀x∀y→Pfx¬→ PxQfyxz". First-order logic_sentence_94

Free and bound variables First-order logic_section_9

Main article: Free variables and bound variables First-order logic_sentence_95

In a formula, a variable may occur free or bound (or both). First-order logic_sentence_96

Intuitively, a variable occurrence is free in a formula if it is not quantified: in ∀y P(x, y), the sole occurrence of variable x is free while that of y is bound. First-order logic_sentence_97

The free and bound variable occurrences in a formula are defined inductively as follows. First-order logic_sentence_98

First-order logic_ordered_list_5

1. Atomic formulas. If φ is an atomic formula, then x occurs free in φ if and only if x occurs in φ. Moreover, there are no bound variables in any atomic formula.First-order logic_item_5_20
2. Negation. x occurs free in ¬φ if and only if x occurs free in φ. x occurs bound in ¬φ if and only if x occurs bound in φ.First-order logic_item_5_21
3. Binary connectives. x occurs free in (φ → ψ) if and only if x occurs free in either φ or ψ. x occurs bound in (φ → ψ) if and only if x occurs bound in either φ or ψ. The same rule applies to any other binary connective in place of →.First-order logic_item_5_22
4. Quantifiers. x occurs free in ∀y φ, if and only if x occurs free in φ and x is a different symbol from y. Also, x occurs bound in ∀y φ, if and only if x is y or x occurs bound in φ. The same rule holds with ∃ in place of ∀.First-order logic_item_5_23

For example, in ∀x ∀y (P(x) → Q(x,f(x),z)), x and y occur only bound, z occurs only free, and w is neither because it does not occur in the formula. First-order logic_sentence_99

Free and bound variables of a formula need not be disjoint sets: in the formula P(x) → ∀x Q(x), the first occurrence of x, as argument of P, is free while the second one, as argument of Q, is bound. First-order logic_sentence_100

A formula in first-order logic with no free variable occurrences is called a first-order sentence. First-order logic_sentence_101

These are the formulas that will have well-defined truth values under an interpretation. First-order logic_sentence_102

For example, whether a formula such as Phil(x) is true must depend on what x represents. First-order logic_sentence_103

But the sentence ∃x Phil(x) will be either true or false in a given interpretation. First-order logic_sentence_104

Example: ordered abelian groups First-order logic_section_10

In mathematics, the language of ordered abelian groups has one constant symbol 0, one unary function symbol −, one binary function symbol +, and one binary relation symbol ≤. First-order logic_sentence_105

Then: First-order logic_sentence_106

Semantics First-order logic_section_11

An interpretation of a first-order language assigns a denotation to each non-logical symbol in that language. First-order logic_sentence_107

It also determines a domain of discourse that specifies the range of the quantifiers. First-order logic_sentence_108

The result is that each term is assigned an object that it represents, each predicate is assigned a property of objects, and each sentence is assigned a truth value. First-order logic_sentence_109

In this way, an interpretation provides semantic meaning to the terms, the predicates, and formulas of the language. First-order logic_sentence_110

The study of the interpretations of formal languages is called formal semantics. First-order logic_sentence_111

What follows is a description of the standard or Tarskian semantics for first-order logic. First-order logic_sentence_112

(It is also possible to define game semantics for first-order logic, but aside from requiring the axiom of choice, game semantics agree with Tarskian semantics for first-order logic, so game semantics will not be elaborated herein.) First-order logic_sentence_113

The interpretation of a function symbol is a function. First-order logic_sentence_114

For example, if the domain of discourse consists of integers, a function symbol f of arity 2 can be interpreted as the function that gives the sum of its arguments. First-order logic_sentence_115

In other words, the symbol f is associated with the function I(f) which, in this interpretation, is addition. First-order logic_sentence_116

The interpretation of an n-ary predicate symbol is a set of n-tuples of elements of the domain of discourse. First-order logic_sentence_117

This means that, given an interpretation, a predicate symbol, and n elements of the domain of discourse, one can tell whether the predicate is true of those elements according to the given interpretation. First-order logic_sentence_118

For example, an interpretation I(P) of a binary predicate symbol P may be the set of pairs of integers such that the first one is less than the second. First-order logic_sentence_119

According to this interpretation, the predicate P would be true if its first argument is less than the second. First-order logic_sentence_120

First-order structures First-order logic_section_12

Main article: Structure (mathematical logic) First-order logic_sentence_121

The most common way of specifying an interpretation (especially in mathematics) is to specify a structure (also called a model; see below). First-order logic_sentence_122

The structure consists of a nonempty set D that forms the domain of discourse and an interpretation I of the non-logical terms of the signature. First-order logic_sentence_123

This interpretation is itself a function: First-order logic_sentence_124

Evaluation of truth values First-order logic_section_13

First, the variable assignment μ can be extended to all terms of the language, with the result that each term maps to a single element of the domain of discourse. First-order logic_sentence_125

The following rules are used to make this assignment: First-order logic_sentence_126

Next, each formula is assigned a truth value. First-order logic_sentence_127

The inductive definition used to make this assignment is called the T-schema. First-order logic_sentence_128

There is a second common approach to defining truth values that does not rely on variable assignment functions. First-order logic_sentence_129

Instead, given an interpretation M, one first adds to the signature a collection of constant symbols, one for each element of the domain of discourse in M; say that for each d in the domain the constant symbol cd is fixed. First-order logic_sentence_130

The interpretation is extended so that each new constant symbol is assigned to its corresponding element of the domain. First-order logic_sentence_131

One now defines truth for quantified formulas syntactically, as follows: First-order logic_sentence_132

This alternate approach gives exactly the same truth values to all sentences as the approach via variable assignments. First-order logic_sentence_133

Validity, satisfiability, and logical consequence First-order logic_section_14

Satisfiability of formulas with free variables is more complicated, because an interpretation on its own does not determine the truth value of such a formula. First-order logic_sentence_135

The most common convention is that a formula with free variables is said to be satisfied by an interpretation if the formula remains true regardless which individuals from the domain of discourse are assigned to its free variables. First-order logic_sentence_136

This has the same effect as saying that a formula is satisfied if and only if its universal closure is satisfied. First-order logic_sentence_137

A formula is logically valid (or simply valid) if it is true in every interpretation. First-order logic_sentence_138

These formulas play a role similar to tautologies in propositional logic. First-order logic_sentence_139

A formula φ is a logical consequence of a formula ψ if every interpretation that makes ψ true also makes φ true. First-order logic_sentence_140

In this case one says that φ is logically implied by ψ. First-order logic_sentence_141

Algebraizations First-order logic_section_15

An alternate approach to the semantics of first-order logic proceeds via abstract algebra. First-order logic_sentence_142

This approach generalizes the Lindenbaum–Tarski algebras of propositional logic. First-order logic_sentence_143

There are three ways of eliminating quantified variables from first-order logic that do not involve replacing quantifiers with other variable binding term operators: First-order logic_sentence_144

First-order logic_unordered_list_6

These algebras are all lattices that properly extend the two-element Boolean algebra. First-order logic_sentence_145

Tarski and Givant (1987) showed that the fragment of first-order logic that has no atomic sentence lying in the scope of more than three quantifiers has the same expressive power as relation algebra. First-order logic_sentence_146

This fragment is of great interest because it suffices for Peano arithmetic and most axiomatic set theory, including the canonical ZFC. First-order logic_sentence_147

They also prove that first-order logic with a primitive ordered pair is equivalent to a relation algebra with two ordered pair projection functions. First-order logic_sentence_148

First-order theories, models, and elementary classes First-order logic_section_16

A first-order theory of a particular signature is a set of axioms, which are sentences consisting of symbols from that signature. First-order logic_sentence_149

The set of axioms is often finite or recursively enumerable, in which case the theory is called effective. First-order logic_sentence_150

Some authors require theories to also include all logical consequences of the axioms. First-order logic_sentence_151

The axioms are considered to hold within the theory and from them other sentences that hold within the theory can be derived. First-order logic_sentence_152

A first-order structure that satisfies all sentences in a given theory is said to be a model of the theory. First-order logic_sentence_153

An elementary class is the set of all structures satisfying a particular theory. First-order logic_sentence_154

These classes are a main subject of study in model theory. First-order logic_sentence_155

Many theories have an intended interpretation, a certain model that is kept in mind when studying the theory. First-order logic_sentence_156

For example, the intended interpretation of Peano arithmetic consists of the usual natural numbers with their usual operations. First-order logic_sentence_157

However, the Löwenheim–Skolem theorem shows that most first-order theories will also have other, nonstandard models. First-order logic_sentence_158

A theory is consistent if it is not possible to prove a contradiction from the axioms of the theory. First-order logic_sentence_159

A theory is complete if, for every formula in its signature, either that formula or its negation is a logical consequence of the axioms of the theory. First-order logic_sentence_160

Gödel's incompleteness theorem shows that effective first-order theories that include a sufficient portion of the theory of the natural numbers can never be both consistent and complete. First-order logic_sentence_161

For more information on this subject see List of first-order theories and Theory (mathematical logic) First-order logic_sentence_162

Empty domains First-order logic_section_17

Main article: Empty domain First-order logic_sentence_163

The definition above requires that the domain of discourse of any interpretation must be nonempty. First-order logic_sentence_164

There are settings, such as inclusive logic, where empty domains are permitted. First-order logic_sentence_165

Moreover, if a class of algebraic structures includes an empty structure (for example, there is an empty poset), that class can only be an elementary class in first-order logic if empty domains are permitted or the empty structure is removed from the class. First-order logic_sentence_166

There are several difficulties with empty domains, however: First-order logic_sentence_167

Thus, when the empty domain is permitted, it must often be treated as a special case. First-order logic_sentence_168

Most authors, however, simply exclude the empty domain by definition. First-order logic_sentence_169

Deductive systems First-order logic_section_18

A deductive system is used to demonstrate, on a purely syntactic basis, that one formula is a logical consequence of another formula. First-order logic_sentence_170

There are many such systems for first-order logic, including Hilbert-style deductive systems, natural deduction, the sequent calculus, the tableaux method, and resolution. First-order logic_sentence_171

These share the common property that a deduction is a finite syntactic object; the format of this object, and the way it is constructed, vary widely. First-order logic_sentence_172

These finite deductions themselves are often called derivations in proof theory. First-order logic_sentence_173

They are also often called proofs, but are completely formalized unlike natural-language mathematical proofs. First-order logic_sentence_174

A deductive system is sound if any formula that can be derived in the system is logically valid. First-order logic_sentence_175

Conversely, a deductive system is complete if every logically valid formula is derivable. First-order logic_sentence_176

All of the systems discussed in this article are both sound and complete. First-order logic_sentence_177

They also share the property that it is possible to effectively verify that a purportedly valid deduction is actually a deduction; such deduction systems are called effective. First-order logic_sentence_178

A key property of deductive systems is that they are purely syntactic, so that derivations can be verified without considering any interpretation. First-order logic_sentence_179

Thus a sound argument is correct in every possible interpretation of the language, regardless whether that interpretation is about mathematics, economics, or some other area. First-order logic_sentence_180

In general, logical consequence in first-order logic is only semidecidable: if a sentence A logically implies a sentence B then this can be discovered (for example, by searching for a proof until one is found, using some effective, sound, complete proof system). First-order logic_sentence_181

However, if A does not logically imply B, this does not mean that A logically implies the negation of B. First-order logic_sentence_182

There is no effective procedure that, given formulas A and B, always correctly decides whether A logically implies B. First-order logic_sentence_183

Rules of inference First-order logic_section_19

Further information: List of rules of inference First-order logic_sentence_184

A rule of inference states that, given a particular formula (or set of formulas) with a certain property as a hypothesis, another specific formula (or set of formulas) can be derived as a conclusion. First-order logic_sentence_185

The rule is sound (or truth-preserving) if it preserves validity in the sense that whenever any interpretation satisfies the hypothesis, that interpretation also satisfies the conclusion. First-order logic_sentence_186

For example, one common rule of inference is the rule of substitution. First-order logic_sentence_187

If t is a term and φ is a formula possibly containing the variable x, then φ[t/x] is the result of replacing all free instances of x by t in φ. First-order logic_sentence_188

The substitution rule states that for any φ and any term t, one can conclude φ[t/x] from φ provided that no free variable of t becomes bound during the substitution process. First-order logic_sentence_189

(If some free variable of t becomes bound, then to substitute t for x it is first necessary to change the bound variables of φ to differ from the free variables of t.) First-order logic_sentence_190

The substitution rule demonstrates several common aspects of rules of inference. First-order logic_sentence_191

It is entirely syntactical; one can tell whether it was correctly applied without appeal to any interpretation. First-order logic_sentence_192

It has (syntactically defined) limitations on when it can be applied, which must be respected to preserve the correctness of derivations. First-order logic_sentence_193

Moreover, as is often the case, these limitations are necessary because of interactions between free and bound variables that occur during syntactic manipulations of the formulas involved in the inference rule. First-order logic_sentence_194

Hilbert-style systems and natural deduction First-order logic_section_20

A deduction in a Hilbert-style deductive system is a list of formulas, each of which is a logical axiom, a hypothesis that has been assumed for the derivation at hand, or follows from previous formulas via a rule of inference. First-order logic_sentence_195

The logical axioms consist of several axiom schemas of logically valid formulas; these encompass a significant amount of propositional logic. First-order logic_sentence_196

The rules of inference enable the manipulation of quantifiers. First-order logic_sentence_197

Typical Hilbert-style systems have a small number of rules of inference, along with several infinite schemas of logical axioms. First-order logic_sentence_198

It is common to have only modus ponens and universal generalization as rules of inference. First-order logic_sentence_199

Natural deduction systems resemble Hilbert-style systems in that a deduction is a finite list of formulas. First-order logic_sentence_200

However, natural deduction systems have no logical axioms; they compensate by adding additional rules of inference that can be used to manipulate the logical connectives in formulas in the proof. First-order logic_sentence_201

Sequent calculus First-order logic_section_21

Further information: Sequent calculus First-order logic_sentence_202

The sequent calculus was developed to study the properties of natural deduction systems. First-order logic_sentence_203

Instead of working with one formula at a time, it uses sequents, which are expressions of the form First-order logic_sentence_204

Tableaux method First-order logic_section_22

Further information: Method of analytic tableaux First-order logic_sentence_205

Resolution First-order logic_section_23

The resolution rule is a single rule of inference that, together with unification, is sound and complete for first-order logic. First-order logic_sentence_206

As with the tableaux method, a formula is proved by showing that the negation of the formula is unsatisfiable. First-order logic_sentence_207

Resolution is commonly used in automated theorem proving. First-order logic_sentence_208

Provable identities First-order logic_section_24

Many identities can be proved, which establish equivalences between particular formulas. First-order logic_sentence_209

These identities allow for rearranging formulas by moving quantifiers across other connectives, and are useful for putting formulas in prenex normal form. First-order logic_sentence_210

Some provable identities include: First-order logic_sentence_211

Equality and its axioms First-order logic_section_25

There are several different conventions for using equality (or identity) in first-order logic. First-order logic_sentence_212

The most common convention, known as first-order logic with equality, includes the equality symbol as a primitive logical symbol which is always interpreted as the real equality relation between members of the domain of discourse, such that the "two" given members are the same member. First-order logic_sentence_213

This approach also adds certain axioms about equality to the deductive system employed. First-order logic_sentence_214

These equality axioms are: First-order logic_sentence_215

First-order logic_ordered_list_7

1. Reflexivity. For each variable x, x = x.First-order logic_item_7_27
2. Substitution for functions. For all variables x and y, and any function symbol f,First-order logic_item_7_28
• x = y → f(...,x,...) = f(...,y,...).First-order logic_item_7_29
3. Substitution for formulas. For any variables x and y and any formula φ(x), if φ' is obtained by replacing any number of free occurrences of x in φ with y, such that these remain free occurrences of y, thenFirst-order logic_item_7_30
• x = y → (φ → φ').First-order logic_item_7_31

These are axiom schemas, each of which specifies an infinite set of axioms. First-order logic_sentence_216

The third schema is known as Leibniz's law, "the principle of substitutivity", "the indiscernibility of identicals", or "the replacement property". First-order logic_sentence_217

The second schema, involving the function symbol f, is (equivalent to) a special case of the third schema, using the formula First-order logic_sentence_218

First-order logic_description_list_8

• x = y → (f(...,x,...) = z → f(...,y,...) = z).First-order logic_item_8_32

Many other properties of equality are consequences of the axioms above, for example: First-order logic_sentence_219

First-order logic_ordered_list_9

1. Symmetry. If x = y then y = x.First-order logic_item_9_33
2. Transitivity. If x = y and y = z then x = z.First-order logic_item_9_34

First-order logic without equality First-order logic_section_26

An alternate approach considers the equality relation to be a non-logical symbol. First-order logic_sentence_220

This convention is known as first-order logic without equality. First-order logic_sentence_221

If an equality relation is included in the signature, the axioms of equality must now be added to the theories under consideration, if desired, instead of being considered rules of logic. First-order logic_sentence_222

The main difference between this method and first-order logic with equality is that an interpretation may now interpret two distinct individuals as "equal" (although, by Leibniz's law, these will satisfy exactly the same formulas under any interpretation). First-order logic_sentence_223

That is, the equality relation may now be interpreted by an arbitrary equivalence relation on the domain of discourse that is congruent with respect to the functions and relations of the interpretation. First-order logic_sentence_224

When this second convention is followed, the term normal model is used to refer to an interpretation where no distinct individuals a and b satisfy a = b. First-order logic_sentence_225

In first-order logic with equality, only normal models are considered, and so there is no term for a model other than a normal model. First-order logic_sentence_226

When first-order logic without equality is studied, it is necessary to amend the statements of results such as the Löwenheim–Skolem theorem so that only normal models are considered. First-order logic_sentence_227

First-order logic without equality is often employed in the context of second-order arithmetic and other higher-order theories of arithmetic, where the equality relation between sets of natural numbers is usually omitted. First-order logic_sentence_228

Defining equality within a theory First-order logic_section_27

If a theory has a binary formula A(x,y) which satisfies reflexivity and Leibniz's law, the theory is said to have equality, or to be a theory with equality. First-order logic_sentence_229

The theory may not have all instances of the above schemas as axioms, but rather as derivable theorems. First-order logic_sentence_230

For example, in theories with no function symbols and a finite number of relations, it is possible to define equality in terms of the relations, by defining the two terms s and t to be equal if any relation is unchanged by changing s to t in any argument. First-order logic_sentence_231

Some theories allow other ad hoc definitions of equality: First-order logic_sentence_232

Metalogical properties First-order logic_section_28

One motivation for the use of first-order logic, rather than higher-order logic, is that first-order logic has many metalogical properties that stronger logics do not have. First-order logic_sentence_233

These results concern general properties of first-order logic itself, rather than properties of individual theories. First-order logic_sentence_234

They provide fundamental tools for the construction of models of first-order theories. First-order logic_sentence_235

Completeness and undecidability First-order logic_section_29

Gödel's completeness theorem, proved by Kurt Gödel in 1929, establishes that there are sound, complete, effective deductive systems for first-order logic, and thus the first-order logical consequence relation is captured by finite provability. First-order logic_sentence_236

Naively, the statement that a formula φ logically implies a formula ψ depends on every model of φ; these models will in general be of arbitrarily large cardinality, and so logical consequence cannot be effectively verified by checking every model. First-order logic_sentence_237

However, it is possible to enumerate all finite derivations and search for a derivation of ψ from φ. First-order logic_sentence_238

If ψ is logically implied by φ, such a derivation will eventually be found. First-order logic_sentence_239

Thus first-order logical consequence is semidecidable: it is possible to make an effective enumeration of all pairs of sentences (φ,ψ) such that ψ is a logical consequence of φ. First-order logic_sentence_240

Unlike propositional logic, first-order logic is undecidable (although semidecidable), provided that the language has at least one predicate of arity at least 2 (other than equality). First-order logic_sentence_241

This means that there is no decision procedure that determines whether arbitrary formulas are logically valid. First-order logic_sentence_242

This result was established independently by Alonzo Church and Alan Turing in 1936 and 1937, respectively, giving a negative answer to the Entscheidungsproblem posed by David Hilbert and Wilhelm Ackermann in 1928. First-order logic_sentence_243

Their proofs demonstrate a connection between the unsolvability of the decision problem for first-order logic and the unsolvability of the halting problem. First-order logic_sentence_244

There are systems weaker than full first-order logic for which the logical consequence relation is decidable. First-order logic_sentence_245

These include propositional logic and monadic predicate logic, which is first-order logic restricted to unary predicate symbols and no function symbols. First-order logic_sentence_246

Other logics with no function symbols which are decidable are the guarded fragment of first-order logic, as well as two-variable logic. First-order logic_sentence_247

The Bernays–Schönfinkel class of first-order formulas is also decidable. First-order logic_sentence_248

Decidable subsets of first-order logic are also studied in the framework of description logics. First-order logic_sentence_249

The Löwenheim–Skolem theorem First-order logic_section_30

The Löwenheim–Skolem theorem shows that if a first-order theory of cardinality λ has an infinite model, then it has models of every infinite cardinality greater than or equal to λ. First-order logic_sentence_250

One of the earliest results in model theory, it implies that it is not possible to characterize countability or uncountability in a first-order language with a countable signature. First-order logic_sentence_251

That is, there is no first-order formula φ(x) such that an arbitrary structure M satisfies φ if and only if the domain of discourse of M is countable (or, in the second case, uncountable). First-order logic_sentence_252

The Löwenheim–Skolem theorem implies that infinite structures cannot be categorically axiomatized in first-order logic. First-order logic_sentence_253

For example, there is no first-order theory whose only model is the real line: any first-order theory with an infinite model also has a model of cardinality larger than the continuum. First-order logic_sentence_254

Since the real line is infinite, any theory satisfied by the real line is also satisfied by some nonstandard models. First-order logic_sentence_255

When the Löwenheim–Skolem theorem is applied to first-order set theories, the nonintuitive consequences are known as Skolem's paradox. First-order logic_sentence_256

The compactness theorem First-order logic_section_31

The compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model. First-order logic_sentence_257

This implies that if a formula is a logical consequence of an infinite set of first-order axioms, then it is a logical consequence of some finite number of those axioms. First-order logic_sentence_258

This theorem was proved first by Kurt Gödel as a consequence of the completeness theorem, but many additional proofs have been obtained over time. First-order logic_sentence_259

It is a central tool in model theory, providing a fundamental method for constructing models. First-order logic_sentence_260

The compactness theorem has a limiting effect on which collections of first-order structures are elementary classes. First-order logic_sentence_261

For example, the compactness theorem implies that any theory that has arbitrarily large finite models has an infinite model. First-order logic_sentence_262

Thus the class of all finite graphs is not an elementary class (the same holds for many other algebraic structures). First-order logic_sentence_263

Lindström's theorem First-order logic_section_32

Main article: Lindström's theorem First-order logic_sentence_264

Per Lindström showed that the metalogical properties just discussed actually characterize first-order logic in the sense that no stronger logic can also have those properties (Ebbinghaus and Flum 1994, Chapter XIII). First-order logic_sentence_265

Lindström defined a class of abstract logical systems, and a rigorous definition of the relative strength of a member of this class. First-order logic_sentence_266

He established two theorems for systems of this type: First-order logic_sentence_267

First-order logic_unordered_list_10

• A logical system satisfying Lindström's definition that contains first-order logic and satisfies both the Löwenheim–Skolem theorem and the compactness theorem must be equivalent to first-order logic.First-order logic_item_10_35
• A logical system satisfying Lindström's definition that has a semidecidable logical consequence relation and satisfies the Löwenheim–Skolem theorem must be equivalent to first-order logic.First-order logic_item_10_36

Limitations First-order logic_section_33

Although first-order logic is sufficient for formalizing much of mathematics, and is commonly used in computer science and other fields, it has certain limitations. First-order logic_sentence_268

These include limitations on its expressiveness and limitations of the fragments of natural languages that it can describe. First-order logic_sentence_269

Expressiveness First-order logic_section_34

The Löwenheim–Skolem theorem shows that if a first-order theory has any infinite model, then it has infinite models of every cardinality. First-order logic_sentence_270

In particular, no first-order theory with an infinite model can be categorical. First-order logic_sentence_271

Thus there is no first-order theory whose only model has the set of natural numbers as its domain, or whose only model has the set of real numbers as its domain. First-order logic_sentence_272

Many extensions of first-order logic, including infinitary logics and higher-order logics, are more expressive in the sense that they do permit categorical axiomatizations of the natural numbers or real numbers. First-order logic_sentence_273

This expressiveness comes at a metalogical cost, however: by Lindström's theorem, the compactness theorem and the downward Löwenheim–Skolem theorem cannot hold in any logic stronger than first-order. First-order logic_sentence_274

Formalizing natural languages First-order logic_section_35

First-order logic is able to formalize many simple quantifier constructions in natural language, such as "every person who lives in Perth lives in Australia". First-order logic_sentence_275

But there are many more complicated features of natural language that cannot be expressed in (single-sorted) first-order logic. First-order logic_sentence_276

"Any logical system which is appropriate as an instrument for the analysis of natural language needs a much richer structure than first-order predicate logic". First-order logic_sentence_277

First-order logic_table_general_1

Quantification over propertiesFirst-order logic_cell_1_1_0 If John is self-satisfied, then there is at least one thing he has in common with Peter.First-order logic_cell_1_1_1 Example requires a quantifier over predicates, which cannot be implemented in single-sorted first-order logic: Zj→ ∃X(Xj∧Xp).First-order logic_cell_1_1_2
Quantification over propertiesFirst-order logic_cell_1_2_0 Santa Claus has all the attributes of a sadist.First-order logic_cell_1_2_1 Example requires quantifiers over predicates, which cannot be implemented in single-sorted first-order logic: ∀X(∀x(Sx → Xx)→Xs).First-order logic_cell_1_2_2
Predicate adverbialFirst-order logic_cell_1_3_0 John is walking quickly.First-order logic_cell_1_3_1 Example cannot be analysed as Wj ∧ Qj; predicate adverbials are not the same kind of thing as second-order predicates such as colour.First-order logic_cell_1_3_2
Relative adjectiveFirst-order logic_cell_1_4_0 Jumbo is a small elephant.First-order logic_cell_1_4_1 Example cannot be analysed as Sj ∧ Ej; predicate adjectives are not the same kind of thing as second-order predicates such as colour.First-order logic_cell_1_4_2
Predicate adverbial modifierFirst-order logic_cell_1_5_0 John is walking very quickly.First-order logic_cell_1_5_1 -First-order logic_cell_1_5_2
Relative adjective modifierFirst-order logic_cell_1_6_0 Jumbo is terribly small.First-order logic_cell_1_6_1 An expression such as "terribly", when applied to a relative adjective such as "small", results in a new composite relative adjective "terribly small".First-order logic_cell_1_6_2
PrepositionsFirst-order logic_cell_1_7_0 Mary is sitting next to John.First-order logic_cell_1_7_1 The preposition "next to" when applied to "John" results in the predicate adverbial "next to John".First-order logic_cell_1_7_2

Restrictions, extensions, and variations First-order logic_section_36

There are many variations of first-order logic. First-order logic_sentence_278

Some of these are inessential in the sense that they merely change notation without affecting the semantics. First-order logic_sentence_279

Others change the expressive power more significantly, by extending the semantics through additional quantifiers or other new logical symbols. First-order logic_sentence_280

For example, infinitary logics permit formulas of infinite size, and modal logics add symbols for possibility and necessity. First-order logic_sentence_281

Restricted languages First-order logic_section_37

First-order logic can be studied in languages with fewer logical symbols than were described above. First-order logic_sentence_282

Restrictions such as these are useful as a technique to reduce the number of inference rules or axiom schemas in deductive systems, which leads to shorter proofs of metalogical results. First-order logic_sentence_283

The cost of the restrictions is that it becomes more difficult to express natural-language statements in the formal system at hand, because the logical connectives used in the natural language statements must be replaced by their (longer) definitions in terms of the restricted collection of logical connectives. First-order logic_sentence_284

Similarly, derivations in the limited systems may be longer than derivations in systems that include additional connectives. First-order logic_sentence_285

There is thus a trade-off between the ease of working within the formal system and the ease of proving results about the formal system. First-order logic_sentence_286

It is also possible to restrict the arities of function symbols and predicate symbols, in sufficiently expressive theories. First-order logic_sentence_287

One can in principle dispense entirely with functions of arity greater than 2 and predicates of arity greater than 1 in theories that include a pairing function. First-order logic_sentence_288

This is a function of arity 2 that takes pairs of elements of the domain and returns an ordered pair containing them. First-order logic_sentence_289

It is also sufficient to have two predicate symbols of arity 2 that define projection functions from an ordered pair to its components. First-order logic_sentence_290

In either case it is necessary that the natural axioms for a pairing function and its projections are satisfied. First-order logic_sentence_291

Many-sorted logic First-order logic_section_38

Main article: Many-sorted logic First-order logic_sentence_292

Ordinary first-order interpretations have a single domain of discourse over which all quantifiers range. First-order logic_sentence_293

Many-sorted first-order logic allows variables to have different sorts, which have different domains. First-order logic_sentence_294

This is also called typed first-order logic, and the sorts called types (as in data type), but it is not the same as first-order type theory. First-order logic_sentence_295

Many-sorted first-order logic is often used in the study of second-order arithmetic. First-order logic_sentence_296

First-order logic_unordered_list_11

• Sometimes it is useful to say that "P(x) holds for exactly one x", which can be expressed as ∃!x P(x). This notation, called uniqueness quantification, may be taken to abbreviate a formula such as ∃x (P(x) ∧∀y (P(y) → (x = y))).First-order logic_item_11_37
• First-order logic with extra quantifiers has new quantifiers Qx,..., with meanings such as "there are many x such that ...". Also see branching quantifiers and the plural quantifiers of George Boolos and others.First-order logic_item_11_38
• Bounded quantifiers are often used in the study of set theory or arithmetic.First-order logic_item_11_39

Infinitary logics First-order logic_section_40

Main article: Infinitary logic First-order logic_sentence_298

Infinitary logic allows infinitely long sentences. First-order logic_sentence_299

For example, one may allow a conjunction or disjunction of infinitely many formulas, or quantification over infinitely many variables. First-order logic_sentence_300

Infinitely long sentences arise in areas of mathematics including topology and model theory. First-order logic_sentence_301

Infinitary logic generalizes first-order logic to allow formulas of infinite length. First-order logic_sentence_302

The most common way in which formulas can become infinite is through infinite conjunctions and disjunctions. First-order logic_sentence_303

However, it is also possible to admit generalized signatures in which function and relation symbols are allowed to have infinite arities, or in which quantifiers can bind infinitely many variables. First-order logic_sentence_304

Because an infinite formula cannot be represented by a finite string, it is necessary to choose some other representation of formulas; the usual representation in this context is a tree. First-order logic_sentence_305

Thus formulas are, essentially, identified with their parse trees, rather than with the strings being parsed. First-order logic_sentence_306

The most commonly studied infinitary logics are denoted Lαβ, where α and β are each either cardinal numbers or the symbol ∞. First-order logic_sentence_307

In this notation, ordinary first-order logic is Lωω. First-order logic_sentence_308

In the logic L∞ω, arbitrary conjunctions or disjunctions are allowed when building formulas, and there is an unlimited supply of variables. First-order logic_sentence_309

More generally, the logic that permits conjunctions or disjunctions with less than κ constituents is known as Lκω. First-order logic_sentence_310

For example, Lω1ω permits countable conjunctions and disjunctions. First-order logic_sentence_311

The set of free variables in a formula of Lκω can have any cardinality strictly less than κ, yet only finitely many of them can be in the scope of any quantifier when a formula appears as a subformula of another. First-order logic_sentence_312

In other infinitary logics, a subformula may be in the scope of infinitely many quantifiers. First-order logic_sentence_313

For example, in Lκ∞, a single universal or existential quantifier may bind arbitrarily many variables simultaneously. First-order logic_sentence_314

Similarly, the logic Lκλ permits simultaneous quantification over fewer than λ variables, as well as conjunctions and disjunctions of size less than κ. First-order logic_sentence_315

Non-classical and modal logics First-order logic_section_41

First-order logic_unordered_list_12

• Intuitionistic first-order logic uses intuitionistic rather than classical propositional calculus; for example, ¬¬φ need not be equivalent to φ.First-order logic_item_12_40
• First-order modal logic allows one to describe other possible worlds as well as this contingently true world which we inhabit. In some versions, the set of possible worlds varies depending on which possible world one inhabits. Modal logic has extra modal operators with meanings which can be characterized informally as, for example "it is necessary that φ" (true in all possible worlds) and "it is possible that φ" (true in some possible world). With standard first-order logic we have a single domain and each predicate is assigned one extension. With first-order modal logic we have a domain function that assigns each possible world its own domain, so that each predicate gets an extension only relative to these possible worlds. This allows us to model cases where, for example, Alex is a Philosopher, but might have been a Mathematician, and might not have existed at all. In the first possible world P(a) is true, in the second P(a) is false, and in the third possible world there is no a in the domain at all.First-order logic_item_12_41
• First-order fuzzy logics are first-order extensions of propositional fuzzy logics rather than classical propositional calculus.First-order logic_item_12_42

Fixpoint logic First-order logic_section_42

Fixpoint logic extends first-order logic by adding the closure under the least fixed points of positive operators. First-order logic_sentence_316

Higher-order logics First-order logic_section_43

Main article: Higher-order logic First-order logic_sentence_317

The characteristic feature of first-order logic is that individuals can be quantified, but not predicates. First-order logic_sentence_318

Thus First-order logic_sentence_319

is a legal first-order formula, but First-order logic_sentence_320

is not, in most formalizations of first-order logic. First-order logic_sentence_321

Second-order logic extends first-order logic by adding the latter type of quantification. First-order logic_sentence_322

Other higher-order logics allow quantification over even higher types than second-order logic permits. First-order logic_sentence_323

These higher types include relations between relations, functions from relations to relations between relations, and other higher-type objects. First-order logic_sentence_324

Thus the "first" in first-order logic describes the type of objects that can be quantified. First-order logic_sentence_325

Unlike first-order logic, for which only one semantics is studied, there are several possible semantics for second-order logic. First-order logic_sentence_326

The most commonly employed semantics for second-order and higher-order logic is known as full semantics. First-order logic_sentence_327

The combination of additional quantifiers and the full semantics for these quantifiers makes higher-order logic stronger than first-order logic. First-order logic_sentence_328

In particular, the (semantic) logical consequence relation for second-order and higher-order logic is not semidecidable; there is no effective deduction system for second-order logic that is sound and complete under full semantics. First-order logic_sentence_329

Second-order logic with full semantics is more expressive than first-order logic. First-order logic_sentence_330

For example, it is possible to create axiom systems in second-order logic that uniquely characterize the natural numbers and the real line. First-order logic_sentence_331

The cost of this expressiveness is that second-order and higher-order logics have fewer attractive metalogical properties than first-order logic. First-order logic_sentence_332

For example, the Löwenheim–Skolem theorem and compactness theorem of first-order logic become false when generalized to higher-order logics with full semantics. First-order logic_sentence_333

Automated theorem proving and formal methods First-order logic_section_44

Further information: Automated theorem proving § First-order theorem proving First-order logic_sentence_334

Automated theorem proving refers to the development of computer programs that search and find derivations (formal proofs) of mathematical theorems. First-order logic_sentence_335

Finding derivations is a difficult task because the search space can be very large; an exhaustive search of every possible derivation is theoretically possible but computationally infeasible for many systems of interest in mathematics. First-order logic_sentence_336

Thus complicated heuristic functions are developed to attempt to find a derivation in less time than a blind search. First-order logic_sentence_337

The related area of automated proof verification uses computer programs to check that human-created proofs are correct. First-order logic_sentence_338

Unlike complicated automated theorem provers, verification systems may be small enough that their correctness can be checked both by hand and through automated software verification. First-order logic_sentence_339

This validation of the proof verifier is needed to give confidence that any derivation labeled as "correct" is actually correct. First-order logic_sentence_340

Some proof verifiers, such as Metamath, insist on having a complete derivation as input. First-order logic_sentence_341

Others, such as Mizar and Isabelle, take a well-formatted proof sketch (which may still be very long and detailed) and fill in the missing pieces by doing simple proof searches or applying known decision procedures: the resulting derivation is then verified by a small, core "kernel". First-order logic_sentence_342

Many such systems are primarily intended for interactive use by human mathematicians: these are known as proof assistants. First-order logic_sentence_343

They may also use formal logics that are stronger than first-order logic, such as type theory. First-order logic_sentence_344

Because a full derivation of any nontrivial result in a first-order deductive system will be extremely long for a human to write, results are often formalized as a series of lemmas, for which derivations can be constructed separately. First-order logic_sentence_345

Automated theorem provers are also used to implement formal verification in computer science. First-order logic_sentence_346

In this setting, theorem provers are used to verify the correctness of programs and of hardware such as processors with respect to a formal specification. First-order logic_sentence_347

Because such analysis is time-consuming and thus expensive, it is usually reserved for projects in which a malfunction would have grave human or financial consequences. First-order logic_sentence_348

For the problem of model checking, efficient algorithms are known to decide whether an input finite structure satisfies a first-order formula, in addition to computational complexity bounds: see Model checking#First-order logic. First-order logic_sentence_349