First-order logic, also calledpredicate logic,predicate calculus, orquantificational logic, is a collection offormal systems used inmathematics,philosophy,linguistics, andcomputer science. First-order logic usesquantified variables over non-logical objects, and allows the use of sentences that contain variables. Rather than propositions such as "all men are mortal", in first-order logic one can have expressions in the form "for allx, ifx is a man, thenx is mortal"; where "for allx" is a quantifier,x is a variable, and "...is a man" and "...is mortal" are predicates.[1] This distinguishes it frompropositional logic, which does not use quantifiers orrelations;[2]: 161 in this sense, propositional logic is the foundation of first-order logic.
A theory about a topic, such asset theory, a theory for groups,[3] or a formal theory ofarithmetic, is usually a first-order logic together with a specifieddomain of discourse (over which the quantified variables range), finitely many functions from that domain to itself, finitely manypredicates defined on that domain, and a set of axioms believed to hold about them. "Theory" is sometimes understood in a more formal sense as just a set of sentences in first-order logic.
The term "first-order" distinguishes first-order logic fromhigher-order logic, in which there are predicates having predicates or functions as arguments, or in which quantification over predicates, functions, or both, are permitted.[4]: 56 In first-order theories, predicates are often associated with sets. In interpreted higher-order theories, predicates may be interpreted as sets of sets.
There are manydeductive systems for first-order logic which are bothsound, i.e. all provable statements are true in all models; andcomplete, i.e. all statements which are true in all models are provable. Although thelogical consequence relation is onlysemidecidable, much progress has been made inautomated theorem proving in first-order logic. First-order logic also satisfies severalmetalogical theorems that make it amenable to analysis inproof theory, such as theLöwenheim–Skolem theorem and thecompactness theorem.
First-order logic is the standard for the formalization of mathematics intoaxioms, and is studied in thefoundations of mathematics.Peano arithmetic andZermelo–Fraenkel set theory are axiomatizations ofnumber theory and set theory, respectively, into first-order logic. No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as thenatural numbers or thereal line. Axiom systems that do fully describe these two structures, i.e.categorical axiom systems, can be obtained in stronger logics such assecond-order logic.
The foundations of first-order logic were developed independently byGottlob Frege andCharles Sanders Peirce.[5] For a history of first-order logic and how it came to dominate formal logic, see José Ferreirós (2001).
| Logical connectives | ||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| ||||||||||||||||||||||||||
| Related concepts | ||||||||||||||||||||||||||
| Applications | ||||||||||||||||||||||||||
 Category | ||||||||||||||||||||||||||
Whilepropositional logic deals with simple declarative propositions, first-order logic additionally coverspredicates andquantification. A predicate evaluates totrue orfalse for an entity or entities in thedomain of discourse.
Consider the two sentences "Socrates is a philosopher" and "Plato is a philosopher". Inpropositional logic, these sentences themselves are viewed as the individuals of study, and might be denoted, for example, by variables such asp andq. They are not viewed as an application of a predicate, such as, to any particular objects in the domain of discourse, instead viewing them as purely an utterance which is either true or false.[6] However, in first-order logic, these two sentences may be framed as statements that a certain individual or non-logical object has a property. In this example, both sentences happen to have the common form for some individual, in the first sentence the value of the variablex is "Socrates", and in the second sentence it is "Plato". Due to the ability to speak about non-logical individuals along with the original logical connectives, first-order logic includes propositional logic.[7]: 29–30
The truth of a formula such as "x is a philosopher" depends on which object is denoted byx and on the interpretation of the predicate "is a philosopher". Consequently, "x is a philosopher" alone does not have a definite truth value of true or false, and is akin to a sentence fragment.[8] Relationships between predicates can be stated usinglogical connectives. For example, the first-order formula "ifx is a philosopher, thenx is a scholar", is aconditional statement with "x is a philosopher" as its hypothesis, and "x is a scholar" as its conclusion, which again needs specification ofx in order to have a definite truth value.
Quantifiers can be applied to variables in a formula. The variablex in the previous formula can be universally quantified, for instance, with the first-order sentence "For everyx, ifx is a philosopher, thenx is a scholar". Theuniversal quantifier "for every" in this sentence expresses the idea that the claim "ifx is a philosopher, thenx is a scholar" holds forall choices ofx.
Thenegation of the sentence "For everyx, ifx is a philosopher, thenx is a scholar" is logically equivalent to the sentence "There existsx such thatx is a philosopher andx is not a scholar". Theexistential quantifier "there exists" expresses the idea that the claim "x is a philosopher andx is not a scholar" holds forsome choice ofx.
The predicates "is a philosopher" and "is a scholar" each take a single variable. In general, predicates can take several variables. In the first-order sentence "Socrates is the teacher of Plato", the predicate "is the teacher of" takes two variables.
An interpretation (or model) of a first-order formula specifies what each predicate means, and the entities that can instantiate the variables. These entities form thedomain of discourse or universe, which is usually required to be a nonempty set. For example, consider the sentence "There existsx such thatx is a philosopher." This sentence is seen as being true in an interpretation such that the domain of discourse consists of all human beings, and that the predicate "is a philosopher" is understood as "was the author of theRepublic." It is true, as witnessed by Plato in that text.[clarification needed]
There are two key parts of first-order logic. Thesyntax determines which finite sequences of symbols are well-formed expressions in first-order logic, while thesemantics determines the meanings behind these expressions.
| Part ofa series on |
| Formal languages |
|---|
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 iswell formed. There are two key types of well-formed expressions:terms, which intuitively represent objects, andformulas, which intuitively express statements that can be true or false. The terms and formulas of first-order logic are strings ofsymbols, where all the symbols together form thealphabet of the language.
As with allformal languages, the nature of the symbols themselves is outside the scope of formal logic; they are often regarded simply as letters and punctuation symbols.
It is common to divide the symbols of the alphabet intological symbols, which always have the same meaning, andnon-logical symbols, whose meaning varies by interpretation.[9] For example, the logical symbol always represents "and"; it is never interpreted as "or", which is represented by the logical symbol. However, a non-logical predicate symbol such as Phil(x) could be interpreted to mean "x is a philosopher", "x is a man named Philip", or any other unary predicate depending on the interpretation at hand.
Logical symbols are a set of characters that vary by author, but usually include the following:[10]
Not all of these symbols are required in first-order logic. Either one of the quantifiers along with negation, conjunction (or disjunction), variables, brackets, and equality suffices.
Other logical symbols include the following:
Non-logical symbols represent predicates (relations), functions and constants. It used to be standard practice to use a fixed, infinite set of non-logical symbols for all purposes:
When the arity of a predicate symbol or function symbol is clear from context, the superscriptn is often omitted.
In this traditional approach, there is only one language of first-order logic.[13] This approach is still common, especially in philosophically oriented books.
A more recent practice is to use different non-logical symbols according to the application one has in mind. Therefore, it has become necessary to name the set of all non-logical symbols used in a particular application. This choice is made via asignature.[14]
Typical signatures in mathematics are {1, ×} or just {×} forgroups,[3] or {0, 1, +, ×, <} forordered fields. There are no restrictions on the number of non-logical symbols. The signature can beempty, finite, or infinite, evenuncountable. Uncountable signatures occur for example in modern proofs of theLöwenheim–Skolem theorem.
Though signatures might in some cases imply how non-logical symbols are to be interpreted,interpretation of the non-logical symbols in the signature is separate (and not necessarily fixed). Signatures concern syntax rather than semantics.
In this approach, every non-logical symbol is of one of the following types:
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.
| BNF grammar |
|---|
<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 abovecontext-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 whenf2',c, andc' are interpreted as multiplication, zero, and one, respectively. |
Theformation rules define the terms and formulas of first-order logic.[16] When terms and formulas are represented as strings of symbols, these rules can be used to write aformal grammar for terms and formulas. These rules are generallycontext-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 ofterms.
The set ofterms isinductively defined by the following rules:[17]
Only expressions which can be obtained by finitely many applications of rules 1 and 2 are terms. For example, no expression involving a predicate symbol is a term.
The set offormulas (also calledwell-formed formulas[18] orWFFs) is inductively defined by the following rules:
Only expressions which can be obtained by finitely many applications of rules 1–5 are formulas. The formulas obtained from the first two rules are said to beatomic formulas.
For example:
is a formula, iff is a unary function symbol,P a unary predicate symbol, and Q a ternary predicate symbol. However, is not a formula, although it is a string of symbols from the alphabet.
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 uniqueparse tree for each formula). This property is known asunique readability of formulas. There are many conventions for where parentheses are used in formulas. For example, some authors use colons or full stops instead of parentheses, or change the places in which parentheses are inserted. Each author's particular definition must be accompanied by a proof of unique readability.
For convenience, conventions have been developed about the precedence of the logical operators, to avoid the need to write parentheses in some cases. These rules are similar to theorder of operations in arithmetic. A common convention is:
Moreover, extra punctuation not required by the definition may be inserted—to make formulas easier to read. Thus the formula:
might be written as:
In some fields, it is common to use infix notation for binary relations and functions, instead of the prefix notation defined above. For example, in arithmetic, one typically writes "2 + 2 = 4" instead of "=(+(2,2),4)". It is common to regard formulas in infix notation as abbreviations for the corresponding formulas in prefix notation, cf. alsoterm structure vs. representation.
The definitions above use infix notation for binary connectives such as. A less common convention isPolish notation, in which one writes, and so on in front of their arguments rather than between them. This convention is advantageous in that it allows all punctuation symbols to be discarded. As such, Polish notation is compact and elegant, but rarely used in practice because it is hard for humans to read. In Polish notation, the formula:
becomes"∀x∀y→Pfx¬→ PxQfyxz".
In a formula, a variable may occurfree orbound (or both). One formalization of this notion is due to Quine, first the concept of a variable occurrence is defined, then whether a variable occurrence is free or bound, then whether a variable symbol overall is free or bound. In order to distinguish different occurrences of the identical symbolx, each occurrence of a variable symbolx in a formula φ is identified with the initial substring of φ up to the point at which said instance of the symbolx appears.[8]p.297 Then, an occurrence ofx is said to be bound if that occurrence ofx lies within the scope of at least one of either or. Finally,x is bound in φ if all occurrences ofx in φ are bound.[8]pp.142--143
Intuitively, a variable symbol is free in a formula if at no point is it quantified:[8]pp.142--143 in∀yP(x,y), the sole occurrence of variablex is free while that ofy is bound. The free and bound variable occurrences in a formula are defined inductively as follows.
For example, in∀x ∀y (P(x) →Q(x,f(x),z)),x andy occur only bound,[19]z occurs only free, andw is neither because it does not occur in the formula.
Free and bound variables of a formula need not be disjoint sets: in the formulaP(x) → ∀xQ(x), the first occurrence ofx, as argument ofP, is free while the second one, as argument ofQ, is bound.
A formula in first-order logic with no free variable occurrences is called afirst-ordersentence. These are the formulas that will have well-definedtruth values under an interpretation. For example, whether a formula such as Phil(x) is true must depend on whatx represents. But the sentence∃x Phil(x) will be either true or false in a given interpretation.
In mathematics, the language of orderedabelian groups has one constant symbol 0, one unary function symbol −, one binary function symbol +, and one binary relation symbol ≤. Then:
The axioms for ordered abelian groups can be expressed as a set of sentences in the language. For example, the axiom stating that the group is commutative is usually written
Aninterpretation of a first-order language assigns a denotation to each non-logical symbol (predicate symbol, function symbol, or constant symbol) in that language. It also determines adomain of discourse that specifies the range of the quantifiers. 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. In this way, an interpretation provides semantic meaning to the terms, predicates, and formulas of the language. The study of the interpretations of formal languages is calledformal semantics. What follows is a description of the standard orTarskian semantics for first-order logic. (It is also possible to definegame semantics for first-order logic, but aside from requiring theaxiom of choice, game semantics agree with Tarskian semantics for first-order logic, so game semantics will not be elaborated herein.)
The most common way of specifying an interpretation (especially in mathematics) is to specify astructure (also called amodel; see below). The structure consists of a domain of discourseD and an interpretation functionI mapping non-logical symbols to predicates, functions, and constants.
The domain of discourseD is a nonempty set of "objects" of some kind. Intuitively, given an interpretation, a first-order formula becomes a statement about these objects; for example, states the existence of some object inD for which the predicateP is true (or, more precisely, for which the predicate assigned to the predicate symbolP by the interpretation is true). For example, one can takeD to be the set ofintegers.
Non-logical symbols are interpreted as follows:
 | This sectiondoes notcite anysources. Please helpimprove this section byadding citations to reliable sources. Unsourced material may be challenged andremoved.(July 2023) (Learn how and when to remove this message) |
A formula evaluates to true or false given an interpretation and avariable assignment μ that associates an element of the domain of discourse with each variable. The reason that a variable assignment is required is to give meanings to formulas with free variables, such as. The truth value of this formula changes depending on the values thatx andy denote.
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. The following rules are used to make this assignment:
Next, each formula is assigned a truth value. The inductive definition used to make this assignment is called theT-schema.
If a formula does not contain free variables, and so is a sentence, then the initial variable assignment does not affect its truth value. In other words, a sentence is true according toM and if and only if it is true according toM and every other variable assignment.
There is a second common approach to defining truth values that does not rely on variable assignment functions. Instead, given an interpretationM, one first adds to the signature a collection of constant symbols, one for each element of the domain of discourse inM; say that for eachd in the domain the constant symbolcd is fixed. The interpretation is extended so that each new constant symbol is assigned to its corresponding element of the domain. One now defines truth for quantified formulas syntactically, as follows:
This alternate approach gives exactly the same truth values to all sentences as the approach via variable assignments.
If a sentence φ evaluates totrue under a given interpretationM, one says thatMsatisfies φ; this is denoted[20]. A sentence issatisfiable if there is some interpretation under which it is true. This is a bit different from the symbol from model theory, where denotes satisfiability in a model, i.e. "there is a suitable assignment of values in's domain to variable symbols of".[21]
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. 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, ...,. This has the same effect as saying that a formula φ is satisfied if and only if itsuniversal closure is satisfied.
A formula islogically valid (or simplyvalid) if it is true in every interpretation.[22] These formulas play a role similar totautologies in propositional logic.
A formula φ is alogical consequence of a formula ψ if every interpretation that makes ψ true also makes φ true. In this case one says that φ is logically implied by ψ.
An alternate approach to the semantics of first-order logic proceeds viaabstract algebra. This approach generalizes theLindenbaum–Tarski algebras of propositional logic. There are three ways of eliminating quantified variables from first-order logic that do not involve replacing quantifiers with other variable binding term operators:
Thesealgebras are alllattices that properly extend thetwo-element Boolean algebra.
Tarski and Givant (1987) showed that the fragment of first-order logic that has noatomic sentence lying in the scope of more than three quantifiers has the same expressive power asrelation algebra.[23]: 32–33 This fragment is of great interest because it suffices forPeano arithmetic and mostaxiomatic set theory, including the canonicalZermelo–Fraenkel set theory (ZFC). They also prove that first-order logic with a primitiveordered pair is equivalent to a relation algebra with two ordered pairprojection functions.[24]: 803
Afirst-order theory of a particular signature is a set ofaxioms, which are sentences consisting of symbols from that signature. The set of axioms is often finite orrecursively enumerable, in which case the theory is calledeffective. Some authors require theories to also include all logical consequences of the axioms. The axioms are considered to hold within the theory and from them other sentences that hold within the theory can be derived.
A first-order structure that satisfies all sentences in a given theory is said to be amodel of the theory. Anelementary class is the set of all structures satisfying a particular theory. These classes are a main subject of study inmodel theory.
Many theories have anintended interpretation, a certain model that is kept in mind when studying the theory. For example, the intended interpretation ofPeano arithmetic consists of the usualnatural numbers with their usual operations. However, the Löwenheim–Skolem theorem shows that most first-order theories will also have other,nonstandard models.
A theory isconsistent if it is not possible to prove a contradiction from the axioms of the theory. A theory iscomplete if, for every formula in its signature, either that formula or its negation is a logical consequence of the axioms of the theory.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.
The definition above requires that the domain of discourse of any interpretation must be nonempty. There are settings, such asinclusive logic, where empty domains are permitted. Moreover, if a class of algebraic structures includes an empty structure (for example, there is an emptyposet), 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.
There are several difficulties with empty domains, however:
Thus, when the empty domain is permitted, it must often be treated as a special case. Most authors, however, simply exclude the empty domain by definition.
Adeductive system is used to demonstrate, on a purely syntactic basis, that one formula is a logical consequence of another formula. There are many such systems for first-order logic, includingHilbert-style deductive systems,natural deduction, thesequent calculus, thetableaux method, andresolution. 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. These finite deductions themselves are often calledderivations in proof theory. They are also often calledproofs but are completely formalized unlike natural-languagemathematical proofs.
A deductive system issound if any formula that can be derived in the system is logically valid. Conversely, a deductive system iscomplete if every logically valid formula is derivable. All of the systems discussed in this article are both sound and complete. 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 calledeffective.
A key property of deductive systems is that they are purely syntactic, so that derivations can be verified without considering any interpretation. Thus, a sound argument is correct in every possible interpretation of the language, regardless of whether that interpretation is about mathematics, economics, or some other area.
In general, logical consequence in first-order logic is onlysemidecidable: 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). However, if A does not logically imply B, this does not mean that A logically implies the negation of B. There is no effective procedure that, given formulas A and B, always correctly decides whether A logically implies B.
Arule 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. 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.
For example, one common rule of inference is therule of substitution. Ift is a term and φ is a formula possibly containing the variablex, then φ[t/x] is the result of replacing all free instances ofx byt in φ. The substitution rule states that for any φ and any termt, one can conclude φ[t/x] from φ provided that no free variable oft becomes bound during the substitution process. (If some free variable oft becomes bound, then to substitutet forx it is first necessary to change the bound variables of φ to differ from the free variables oft.)
To see why the restriction on bound variables is necessary, consider the logically valid formula φ given by, in the signature of (0,1,+,×,=) of arithmetic. Ift is the term "x + 1", the formula φ[t/y] is, which will be false in many interpretations. The problem is that the free variablex oft became bound during the substitution. The intended replacement can be obtained by renaming the bound variablex of φ to something else, sayz, so that the formula after substitution is, which is again logically valid.
The substitution rule demonstrates several common aspects of rules of inference. It is entirely syntactical; one can tell whether it was correctly applied without appeal to any interpretation. It has (syntactically defined) limitations on when it can be applied, which must be respected to preserve the correctness of derivations. 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.
A deduction in a Hilbert-style deductive system is a list of formulas, each of which is alogical axiom, a hypothesis that has been assumed for the derivation at hand or follows from previous formulas via a rule of inference. The logical axioms consist of severalaxiom schemas of logically valid formulas; these encompass a significant amount of propositional logic. The rules of inference enable the manipulation of quantifiers. Typical Hilbert-style systems have a small number of rules of inference, along with several infinite schemas of logical axioms. It is common to have onlymodus ponens anduniversal generalization as rules of inference.
Natural deduction systems resemble Hilbert-style systems in that a deduction is a finite list of formulas. 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.
The sequent calculus was developed to study the properties of natural deduction systems.[25] Instead of working with one formula at a time, it usessequents, which are expressions of the form:
where A1, ..., An, B1, ..., Bk are formulas and the turnstile symbol is used as punctuation to separate the two halves. Intuitively, a sequent expresses the idea that implies.
Unlike the methods just described the derivations in the tableaux method are not lists of formulas. Instead, a derivation is a tree of formulas. To show that a formula A is provable, the tableaux method attempts to demonstrate that the negation of A is unsatisfiable. The tree of the derivation has at its root; the tree branches in a way that reflects the structure of the formula. For example, to show that is unsatisfiable requires showing that C and D are each unsatisfiable; this corresponds to a branching point in the tree with parent and children C and D.
Theresolution rule is a single rule of inference that, together withunification, is sound and complete for first-order logic. As with the tableaux method, a formula is proved by showing that the negation of the formula is unsatisfiable. Resolution is commonly used in automated theorem proving.
The resolution method works only with formulas that are disjunctions of atomic formulas; arbitrary formulas must first be converted to this form throughSkolemization. The resolution rule states that from the hypotheses and, the conclusion can be obtained.
Many identities can be proved, which establish equivalences between particular formulas. These identities allow for rearranging formulas by moving quantifiers across other connectives and are useful for putting formulas inprenex normal form. Some provable identities include:
There are several different conventions for using equality (or identity) in first-order logic. The most common convention, known asfirst-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. This approach also adds certain axioms about equality to the deductive system employed. These equality axioms are:[26]: 198–200
These areaxiom schemas, each of which specifies an infinite set of axioms. The third schema is known asLeibniz's law, "the principle of substitutivity", "the indiscernibility of identicals", or "the replacement property". The second schema, involving the function symbolf, is (equivalent to) a special case of the third schema, using the formula:
Then
Sincex =y is given, andf(...,x, ...) =f(...,x, ...) true by reflexivity, we havef(...,x, ...) =f(...,y, ...)
Many other properties of equality are consequences of the axioms above, for example:
An alternate approach considers the equality relation to be a non-logical symbol. This convention is known asfirst-order logic without equality. 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. 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). That is, the equality relation may now be interpreted by an arbitraryequivalence relation on the domain of discourse that iscongruent with respect to the functions and relations of the interpretation.
When this second convention is followed, the termnormal model is used to refer to an interpretation where no distinct individualsa andb satisfya =b. 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. When first-order logic without equality is studied, it is necessary to amend the statements of results such as theLöwenheim–Skolem theorem so that only normal models are considered.
First-order logic without equality is often employed in the context ofsecond-order arithmetic and other higher-order theories of arithmetic, where the equality relation between sets of natural numbers is usually omitted.
If a theory has a binary formulaA(x,y) which satisfies reflexivity and Leibniz's law, the theory is said to have equality, or to be a theory with equality. The theory may not have all instances of the above schemas as axioms, but rather as derivable theorems. For example, in theories with no function symbols and a finite number of relations, it is possible todefine equality in terms of the relations, by defining the two termss andt to be equal if any relation is unchanged by changings tot in any argument.
Some theories allow otherad hoc definitions of equality:
One motivation for the use of first-order logic, rather thanhigher-order logic, is that first-order logic has manymetalogical properties that stronger logics do not have. These results concern general properties of first-order logic itself, rather than properties of individual theories. They provide fundamental tools for the construction of models of first-order theories.
Gödel's completeness theorem, proved byKurt 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. 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. However, it is possible to enumerate all finite derivations and search for a derivation of ψ from φ. If ψ is logically implied by φ, such a derivation will eventually be found. Thus first-order logical consequence issemidecidable: it is possible to make an effective enumeration of all pairs of sentences (φ,ψ) such that ψ is a logical consequence of φ.
Unlikepropositional logic, first-order logic isundecidable (although semidecidable), provided that the language has at least one predicate of arity at least 2 (other than equality). This means that there is nodecision procedure that determines whether arbitrary formulas are logically valid. This result was established independently byAlonzo Church andAlan Turing in 1936 and 1937, respectively, giving a negative answer to theEntscheidungsproblem posed byDavid Hilbert andWilhelm Ackermann in 1928. Their proofs demonstrate a connection between the unsolvability of the decision problem for first-order logic and the unsolvability of thehalting problem.
There are systems weaker than full first-order logic for which the logical consequence relation is decidable. These include propositional logic andmonadic predicate logic, which is first-order logic restricted to unary predicate symbols and no function symbols. Other logics with no function symbols which are decidable are theguarded fragment of first-order logic, as well astwo-variable logic. TheBernays–Schönfinkel class of first-order formulas is also decidable. Decidable subsets of first-order logic are also studied in the framework ofdescription logics.
TheLöwenheim–Skolem theorem shows that if a first-order theory ofcardinality λ has an infinite model, then it has models of every infinite cardinality greater than or equal to λ. One of the earliest results inmodel theory, it implies that it is not possible to characterizecountability or uncountability in a first-order language with a countable signature. 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).
The Löwenheim–Skolem theorem implies that infinite structures cannot becategorically axiomatized in first-order logic. 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. Since the real line is infinite, any theory satisfied by the real line is also satisfied by somenonstandard models. When the Löwenheim–Skolem theorem is applied to first-order set theories, the nonintuitive consequences are known asSkolem's paradox.
Thecompactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model.[29] 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. 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. It is a central tool in model theory, providing a fundamental method for constructing models.
The compactness theorem has a limiting effect on which collections of first-order structures are elementary classes. For example, the compactness theorem implies that any theory that has arbitrarily large finite models has an infinite model. Thus, the class of all finitegraphs is not an elementary class (the same holds for many other algebraic structures).
There are also more subtle limitations of first-order logic that are implied by the compactness theorem. For example, in computer science, many situations can be modeled as adirected graph of states (nodes) and connections (directed edges). Validating such a system may require showing that no "bad" state can be reached from any "good" state. Thus, one seeks to determine if the good and bad states are in differentconnected components of the graph. However, the compactness theorem can be used to show that connected graphs are not an elementary class in first-order logic, and there is no formula φ(x,y) of first-order logic, in thelogic of graphs, that expresses the idea that there is a path fromx toy. Connectedness can be expressed insecond-order logic, however, but not with only existential set quantifiers, as also enjoys compactness.
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). Lindström defined a class of abstract logical systems, and a rigorous definition of the relative strength of a member of this class. He established two theorems for systems of this type:
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. These include limitations on its expressiveness and limitations of the fragments of natural languages that it can describe.
For instance, first-order logic is undecidable, meaning a sound, complete and terminating decision algorithm for provability is impossible. This has led to the study of interesting decidable fragments, such as C2: first-order logic with two variables and thecounting quantifiers and.[30]
TheLöwenheim–Skolem theorem shows that if a first-order theory has any infinite model, then it has infinite models of every cardinality. In particular, no first-order theory with an infinite model can becategorical. 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. 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[clarification needed]. This expressiveness comes at a metalogical cost, however: byLindströ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 is able to formalize many simple quantifier constructions in natural language, such as "every person who lives in Perth lives in Australia". Hence, first-order logic is used as a basis forknowledge representation languages, such asFO(.).
Still, there are complicated features of natural language that cannot be expressed in first-order logic. "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".[31]
| Type | Example | Comment |
|---|---|---|
| Quantification over properties | If John is self-satisfied, then there is at least one thing he has in common with Peter. | Example requires a quantifier over predicates, which cannot be implemented in single-sorted first-order logic:Zj → ∃X(Xj∧Xp). |
| Quantification over properties | Santa Claus has all the attributes of a sadist. | Example requires quantifiers over predicates, which cannot be implemented in single-sorted first-order logic:∀X(∀x(Sx → Xx) → Xs). |
| Predicate adverbial | John is walking quickly. | Example cannot be analysed asWj ∧ Qj; predicate adverbials are not the same kind of thing as second-order predicates such as colour. |
| Relative adjective | Jumbo is a small elephant. | Example cannot be analysed asSj ∧ Ej; predicate adjectives are not the same kind of thing as second-order predicates such as colour. |
| Predicate adverbial modifier | John is walking very quickly. | — |
| Relative adjective modifier | Jumbo is terribly small. | An expression such as "terribly", when applied to a relative adjective such as "small", results in a new composite relative adjective "terribly small". |
| Prepositions | Mary is sitting next to John. | The preposition "next to" when applied to "John" results in the predicate adverbial "next to John". |
There are many variations of first-order logic. Some of these are inessential in the sense that they merely change notation without affecting the semantics. Others change the expressive power more significantly, by extending the semantics through additional quantifiers or other new logical symbols. For example, infinitary logics permit formulas of infinite size, and modal logics add symbols for possibility and necessity.
First-order logic can be studied in languages with fewer logical symbols than were described above:
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. 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. Similarly, derivations in the limited systems may be longer than derivations in systems that include additional connectives. 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.
It is also possible to restrict the arities of function symbols and predicate symbols, in sufficiently expressive theories. One can in principle dispense entirely with functions of arity greater than 2 and predicates of arity greater than 1 in theories that include apairing function. This is a function of arity 2 that takes pairs of elements of the domain and returns anordered pair containing them. It is also sufficient to have two predicate symbols of arity 2 that define projection functions from an ordered pair to its components. In either case it is necessary that the natural axioms for a pairing function and its projections are satisfied.
Ordinary first-order interpretations have a single domain of discourse over which all quantifiers range.Many-sorted first-order logic allows variables to have differentsorts, which have different domains. This is also calledtyped first-order logic, and the sorts calledtypes (as indata type), but it is not the same as first-ordertype theory. Many-sorted first-order logic is often used in the study ofsecond-order arithmetic.[33]
When there are only finitely many sorts in a theory, many-sorted first-order logic can be reduced to single-sorted first-order logic.[34]: 296–299 One introduces into the single-sorted theory a unary predicate symbol for each sort in the many-sorted theory and adds an axiom saying that these unary predicates partition the domain of discourse. For example, if there are two sorts, one adds predicate symbols and and the axiom:
Then the elements satisfying are thought of as elements of the first sort, and elements satisfying as elements of the second sort. One can quantify over each sort by using the corresponding predicate symbol to limit the range of quantification. For example, to say there is an element of the first sort satisfying formula, one writes:
Additional quantifiers can be added to first-order logic.
Infinitary logic allows infinitely long sentences. For example, one may allow a conjunction or disjunction of infinitely many formulas, or quantification over infinitely many variables. Infinitely long sentences arise in areas of mathematics includingtopology andmodel theory.
Infinitary logic generalizes first-order logic to allow formulas of infinite length. The most common way in which formulas can become infinite is through infinite conjunctions and disjunctions. 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. 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. Thus, formulas are, essentially, identified with their parse trees, rather than with the strings being parsed.
The most commonly studied infinitary logics are denotedLαβ, where α and β are each eithercardinal numbers or the symbol ∞. In this notation, ordinary first-order logic isLωω.In the logicL∞ω, arbitrary conjunctions or disjunctions are allowed when building formulas, and there is an unlimited supply of variables. More generally, the logic that permits conjunctions or disjunctions with less than κ constituents is known asLκω. For example,Lω1ω permitscountable conjunctions and disjunctions.
The set of free variables in a formula ofLκω 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.[35] In other infinitary logics, a subformula may be in the scope of infinitely many quantifiers. For example, inLκ∞, a single universal or existential quantifier may bind arbitrarily many variables simultaneously. Similarly, the logicLκλ permits simultaneous quantification over fewer than λ variables, as well as conjunctions and disjunctions of size less than κ.
Fixpoint logic extends first-order logic by adding the closure under the least fixed points of positive operators.[36]
The characteristic feature of first-order logic is that individuals can be quantified, but not predicates. Thus
is a legal first-order formula, but
is not, in most formalizations of first-order logic.Second-order logic extends first-order logic by adding the latter type of quantification. Otherhigher-order logics allow quantification over even highertypes than second-order logic permits. These higher types include relations between relations, functions from relations to relations between relations, and other higher-type objects. Thus the "first" in first-order logic describes the type of objects that can be quantified.
Unlike first-order logic, for which only one semantics is studied, there are several possible semantics for second-order logic. The most commonly employed semantics for second-order and higher-order logic is known asfull semantics. The combination of additional quantifiers and the full semantics for these quantifiers makes higher-order logic stronger than first-order logic. 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.
Second-order logic with full semantics is more expressive than first-order logic. For example, it is possible to create axiom systems in second-order logic that uniquely characterize the natural numbers and the real line. The cost of this expressiveness is that second-order and higher-order logics have fewer attractive metalogical properties than first-order logic. 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.
Automated theorem proving refers to the development of computer programs that search and find derivations (formal proofs) of mathematical theorems.[37] Finding derivations is a difficult task because thesearch space can be very large; an exhaustive search of every possible derivation is theoretically possible butcomputationally infeasible for many systems of interest in mathematics. Thus complicatedheuristic functions are developed to attempt to find a derivation in less time than a blind search.[38]
The related area of automatedproof verification uses computer programs to check that human-created proofs are correct. 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. This validation of the proof verifier is needed to give confidence that any derivation labeled as "correct" is actually correct.
Some proof verifiers, such asMetamath, insist on having a complete derivation as input. Others, such asMizar andIsabelle, 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". Many such systems are primarily intended for interactive use by human mathematicians: these are known asproof assistants. They may also use formal logics that are stronger than first-order logic, such as type theory. Because a full derivation of any nontrivial result in a first-order deductive system will be extremely long for a human to write,[39] results are often formalized as a series of lemmas, for which derivations can be constructed separately.
Automated theorem provers are also used to implementformal verification in computer science. In this setting, theorem provers are used to verify the correctness of programs and of hardware such asprocessors with respect to aformal specification. 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.
For the problem ofmodel checking, efficientalgorithms are known todecide whether an input finite structure satisfies a first-order formula, in addition tocomputational complexity bounds: seeModel checking § First-order logic.
| General | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Theorems (list) and paradoxes | |||||||||
| Logics |
| ||||||||
| Set theory |
| ||||||||
| Formal systems (list), language and syntax |
| ||||||||
| Proof theory | |||||||||
| Model theory | |||||||||
| Computability theory | |||||||||
| Related | |||||||||
