HOME

TheInfoList



OR:

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of
formal system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A fo ...
s used in
mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
,
philosophy Philosophy (from , ) is the systematized study of general and fundamental questions, such as those about existence, reason, knowledge, values, mind, and language. Such questions are often posed as problems to be studied or resolved. ...
,
linguistics Linguistics is the scientific study of human language. It is called a scientific study because it entails a comprehensive, systematic, objective, and precise analysis of all aspects of language, particularly its nature and structure. Ling ...
, and
computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
. 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. This distinguishes it from
propositional logic Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic. A theory about a topic is usually a first-order logic together with a specified
domain of discourse In the formal sciences, the domain of discourse, also called the universe of discourse, universal set, or simply universe, is the set of entities over which certain variables of interest in some formal treatment may range. Overview The doma ...
(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. Sometimes, "theory" is understood in a more formal sense as just a set of sentences in first-order logic. The adjective "first-order" distinguishes first-order logic from
higher-order logic mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
, in which there are predicates having predicates or functions as arguments, or in which quantification over predicates or functions, or both, are permitted. 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 many
deductive system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A for ...
s for first-order logic which are both
sound In physics, sound is a vibration that propagates as an acoustic wave, through a transmission medium such as a gas, liquid or solid. In human physiology and psychology, sound is the ''reception'' of such waves and their ''perception'' by ...
(i.e., all provable statements are true in all models) and
complete Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies t ...
(i.e. all statements which are true in all models are provable). Although the
logical consequence Logical consequence (also entailment) is a fundamental concept in logic, which describes the relationship between statements that hold true when one statement logically ''follows from'' one or more statements. A valid logical argument is on ...
relation is only
semidecidable In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer. Zeroth-order logic (propositional logic) is decidable, whereas first-order and higher-order logic are not. Logical systems a ...
, much progress has been made in
automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ...
in first-order logic. First-order logic also satisfies several
metalogic Metalogic is the study of the metatheory of logic. Whereas ''logic'' studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems.Harry GenslerIntroduction to Logic Routledge, ...
al theorems that make it amenable to analysis in
proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding part ...
, such as the
Löwenheim–Skolem theorem In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem. The precise formulation is given below. It implies that if a countable first-ord ...
and the
compactness theorem In mathematical logic, 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. This theorem is an important tool in model theory, as it provides a useful (but generally ...
. First-order logic is the standard for the formalization of mathematics into axioms, and is studied in the
foundations of mathematics Foundations of mathematics is the study of the philosophical and logical and/or algorithmic basis of mathematics, or, in a broader sense, the mathematical investigation of what underlies the philosophical theories concerning the nature of mathe ...
.
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearl ...
and
Zermelo–Fraenkel set theory In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such ...
are axiomatizations of
number theory Number theory (or arithmetic or higher arithmetic in older usage) is a branch of pure mathematics devoted primarily to the study of the integers and integer-valued functions. German mathematician Carl Friedrich Gauss (1777–1855) said, "Ma ...
and
set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly concern ...
, respectively, into first-order logic. No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the
natural number In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country"). Numbers used for counting are called '' cardinal ...
s or the
real line In elementary mathematics, a number line is a picture of a graduated straight line that serves as visual representation of the real numbers. Every point of a number line is assumed to correspond to a real number, and every real number to a po ...
. 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 In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies on ...
. The foundations of first-order logic were developed independently by
Gottlob Frege Friedrich Ludwig Gottlob Frege (; ; 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic p ...
and
Charles Sanders Peirce Charles Sanders Peirce ( ; September 10, 1839 – April 19, 1914) was an American philosopher, logician, mathematician and scientist who is sometimes known as "the father of pragmatism". Educated as a chemist and employed as a scientist for ...
. For a history of first-order logic and how it came to dominate formal logic, see José Ferreirós (2001).


Introduction

While
propositional logic Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
deals with simple declarative propositions, first-order logic additionally covers
predicate Predicate or predication may refer to: * Predicate (grammar), in linguistics * Predication (philosophy) * several closely related uses in mathematics and formal logic: **Predicate (mathematical logic) **Propositional function **Finitary relation, o ...
s and quantification. A predicate takes an entity or entities in the
domain of discourse In the formal sciences, the domain of discourse, also called the universe of discourse, universal set, or simply universe, is the set of entities over which certain variables of interest in some formal treatment may range. Overview The doma ...
and evaluates to
true True most commonly refers to truth, the state of being in congruence with fact or reality. True may also refer to: Places * True, West Virginia, an unincorporated community in the United States * True, Wisconsin, a town in the United States * ...
or false. Consider the two sentences "Socrates is a philosopher" and "Plato is a philosopher". In
propositional logic Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
, these sentences are viewed as being unrelated, and might be denoted, for example, by variables such as ''p'' and ''q''. The predicate "is a philosopher" occurs in both sentences, which have a common structure of "''a'' is a philosopher". The variable ''a'' is instantiated as "Socrates" in the first sentence, and is instantiated as "Plato" in the second sentence. While first-order logic allows for the use of predicates, such as "is a philosopher" in this example, propositional logic does not. Relationships between predicates can be stated using
logical connective In logic, a logical connective (also called a logical operator, sentential connective, or sentential operator) is a logical constant. They can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary ...
s. Consider, for example, the first-order formula "if ''a'' is a philosopher, then ''a'' is a scholar". This formula is a
conditional Conditional (if then) may refer to: *Causal conditional, if X then Y, where X is a cause of Y *Conditional probability, the probability of an event A given that another event B has occurred *Conditional proof, in logic: a proof that asserts a co ...
statement with "''a'' is a philosopher" as its hypothesis, and "''a'' is a scholar" as its conclusion. 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". Quantifiers can be applied to variables in a formula. 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". The
universal quantifier In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other ...
"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''. The ''
negation In logic, negation, also called the logical complement, is an operation that takes a proposition P to another proposition "not P", written \neg P, \mathord P or \overline. It is interpreted intuitively as being true when P is false, and false ...
'' 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". The
existential quantifier In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, w ...
"there exists" expresses the idea that the claim "''a'' is a philosopher and ''a'' is not a scholar" holds for ''some'' choice of ''a''. 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 the
domain of discourse In the formal sciences, the domain of discourse, also called the universe of discourse, universal set, or simply universe, is the set of entities over which certain variables of interest in some formal treatment may range. Overview The doma ...
or universe, which is usually required to be a nonempty set. 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 A republic () is a " state in which power rests with the people or their representatives; specifically a state without a monarchy" and also a "government, or system of government, of such a state." Previously, especially in the 17th and 18th ...
''", the sentence "There exists ''a'' such that ''a'' is a philosopher" is seen as being true, as witnessed by Plato. There are two key parts of first-order logic. The
syntax In linguistics, syntax () is the study of how words and morphemes combine to form larger units such as phrases and sentences. Central concerns of syntax include word order, grammatical relations, hierarchical sentence structure ( constituenc ...
determines which finite sequences of symbols are well-formed expressions in first-order logic, while the
semantics Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and comput ...
determines the meanings behind these expressions.


Syntax


Alphabet

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. There are two key types of well-formed expressions: ''terms'', which intuitively represent objects, and ''formulas'', which intuitively express statements that can be true or false. The terms and formulas of first-order logic are strings of ''symbols'', where all the symbols together form the ''alphabet'' of the language. As with all
formal language In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules. The alphabet of a formal language consists of sym ...
s, 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 into ''logical symbols'', which always have the same meaning, and ''non-logical symbols'', whose meaning varies by interpretation. For example, the logical symbol \land always represents "and"; it is never interpreted as "or", which is represented by the logical symbol \lor. 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

Logical symbols are a set of characters that vary by author, but usually include the following: * Quantifier symbols: for universal quantification, and for existential quantification *
Logical connective In logic, a logical connective (also called a logical operator, sentential connective, or sentential operator) is a logical constant. They can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary ...
s: for
conjunction Conjunction may refer to: * Conjunction (grammar), a part of speech * Logical conjunction, a mathematical operator ** Conjunction introduction, a rule of inference of propositional logic * Conjunction (astronomy), in which two astronomical bodies ...
, for
disjunction In logic, disjunction is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is raining or it is snowing" can be represented in logic using the disjunctive formula R \lor ...
, for implication, for biconditional, for negation. Some authors use C''pq'' instead of and E''pq'' instead of , especially in contexts where → is used for other purposes. Moreover, the horseshoe may replace ; the triple-bar may replace ; a tilde (), N''p'', or F''p'' may replace ; a double bar \, , +, or A''pq'' may replace ; and an ampersand , K''pq'', or the middle dot may replace , especially if these symbols are not available for technical reasons. (The aforementioned symbols C''pq'', E''pq'', N''p'', A''pq'', and K''pq'' are used in
Polish notation Polish notation (PN), also known as normal Polish notation (NPN), Łukasiewicz notation, Warsaw notation, Polish prefix notation or simply prefix notation, is a mathematical notation in which operators ''precede'' their operands, in contrast ...
.) * Parentheses, brackets, and other punctuation symbols. The choice of such symbols varies depending on context. * 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: * An ''equality symbol'' (sometimes, ''identity symbol'') (see below). 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: * Truth constants: T, V, or for "true" and F, O, or for "false" (V and O are from Polish notation). Without any such logical operators of valence 0, these two constants can only be expressed using quantifiers. * Additional logical connectives such as the Sheffer stroke, D''pq'' (NAND), and
exclusive or Exclusive or or exclusive disjunction is a logical operation that is true if and only if its arguments differ (one is true, the other is false). It is symbolized by the prefix operator J and by the infix operators XOR ( or ), EOR, EXOR, , ...
, J''pq''.


Non-logical symbols

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: * 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'', there is an infinite supply of them: *:''P''''n''0, ''P''''n''1, ''P''''n''2, ''P''''n''3, ... * For every integer ''n'' ≥ 0, there are infinitely many ''n''-ary ''function symbols'': *:''f n''0, ''f n''1, ''f n''2, ''f n''3, ... When the arity of a predicate symbol or function symbol is clear from context, the superscript ''n'' is often omitted. In this traditional approach, there is only one language of first-order logic. 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 a ''
signature A signature (; from la, signare, "to sign") is a Handwriting, handwritten (and often Stylization, stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and ...
''. Typical signatures in mathematics are or just for
group A group is a number of persons or things that are located, gathered, or classed together. Groups of people * Cultural group, a group whose members share the same cultural identity * Ethnic group, a group whose members share the same ethnic ide ...
s, or for
ordered field In mathematics, an ordered field is a field together with a total ordering of its elements that is compatible with the field operations. The basic example of an ordered field is the field of real numbers, and every Dedekind-complete ordered fiel ...
s. There are no restrictions on the number of non-logical symbols. The signature can be
empty Empty may refer to: ‍ Music Albums * ''Empty'' (God Lives Underwater album) or the title song, 1995 * ''Empty'' (Nils Frahm album), 2020 * ''Empty'' (Tait album) or the title song, 2001 Songs * "Empty" (The Click Five song), 2007 * ...
, finite, or infinite, even
uncountable In mathematics, an uncountable set (or uncountably infinite set) is an infinite set that contains too many elements to be countable. The uncountability of a set is closely related to its cardinal number: a set is uncountable if its cardinal num ...
. Uncountable signatures occur for example in modern proofs of the
Löwenheim–Skolem theorem In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem. The precise formulation is given below. It implies that if a countable first-ord ...
. Though signatures might in some cases imply how non-logical symbols are to be interpreted,
interpretation Interpretation may refer to: Culture * Aesthetic interpretation, an explanation of the meaning of a work of art * Allegorical interpretation, an approach that assumes a text should not be interpreted literally * Dramatic Interpretation, an event ...
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: * 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''. Examples: ** In ''P''(''x''), ''P'' is a predicate symbol of valence 1. One possible interpretation is "''x'' is a man". ** In ''Q''(''x'',''y''), ''Q'' is a predicate symbol of valence 2. Possible interpretations include "''x'' is greater than ''y''" and "''x'' is the father of ''y''". ** Relations of valence 0 can be identified with propositional variables, which can stand for any statement. One possible interpretation of ''R'' is "Socrates is a man". * 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''. Examples: ** ''f''(''x'') may be interpreted as "the father of ''x''". In
arithmetic Arithmetic () is an elementary part of mathematics that consists of the study of the properties of the traditional operations on numbers— addition, subtraction, multiplication, division, exponentiation, and extraction of roots. In the 19th ...
, it may stand for "-x". In
set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly concern ...
, it may stand for "the
power set In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is post ...
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''". ** 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, it may stand for the
empty set In mathematics, the empty set is the unique set having no elements; its size or cardinality (count of elements in a set) is zero. Some axiomatic set theories ensure that the empty set exists by including an axiom of empty set, while in othe ...
. 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.


Formation rules

The
formation rule In mathematical logic, formation rules are rules for describing which strings of symbols formed from the alphabet of a formal language are syntactically valid within the language. These rules only address the location and manipulation of the str ...
s define the terms and formulas of first-order logic. When terms and formulas are represented as strings of symbols, these rules can be used to write a
formal grammar In formal language theory, a grammar (when the context is not given, often called a formal grammar for clarity) describes how to form strings from a language's alphabet that are valid according to the language's syntax. A grammar does not describe ...
for terms and formulas. 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.


Terms

The set of '' terms'' is inductively defined by the following rules: * ''Variables''. Any variable symbol is a term. * ''Functions''. If ''f'' is an ''n''-ary function symbol, and ''t''1, ..., ''t''''n'' are terms, then ''f''(''t''1,...,''t''''n'') is a term. In particular, symbols denoting individual constants are nullary function symbols, and thus are terms. 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.


Formulas

The set of '' formulas'' (also called ''
well-formed formulas In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language. A formal language c ...
'' or ''WFFs'') is inductively defined by the following rules: * ''Predicate symbols''. If ''P'' is an ''n''-ary predicate symbol and ''t''1, ..., ''t''''n'' are terms then ''P''(''t''1,...,''t''''n'') is a formula. * '' Equality''. If the equality symbol is considered part of logic, and ''t''1 and ''t''2 are terms, then ''t''1 = ''t''2 is a formula. * ''Negation''. If \varphi is a formula, then \lnot\varphi is a formula. * ''Binary connectives''. If and are formulas, then (\varphi\rightarrow\psi) is a formula. Similar rules apply to other binary logical connectives. * ''Quantifiers''. If \varphi is a formula and ''x'' is a variable, then \forall x \varphi (for all x, \varphi holds) and \exists x \varphi (there exists x such that \varphi) are formulas. 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 be ''
atomic formula In mathematical logic, an atomic formula (also known as an atom or a prime formula) is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformu ...
s''. For example, :\forall x \forall y (P(f(x)) \rightarrow\neg (P(x) \rightarrow Q(f(y),x,z))) is a formula, if ''f'' is a unary function symbol, ''P'' a unary predicate symbol, and Q a ternary predicate symbol. However, \forall x\, x \rightarrow 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 unique
parse tree A parse tree or parsing tree or derivation tree or concrete syntax tree is an ordered, rooted tree that represents the syntactic structure of a string according to some context-free grammar. The term ''parse tree'' itself is used primarily in co ...
for each formula). This property is known as ''unique 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. 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. This is because both predicates and functions can only accept terms as parameters, but the first parameter is a formula. Some languages built on first-order logic, such as SMT-LIB 2.0, add this.


Notational conventions

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 the
order of operations In mathematics and computer programming, the order of operations (or operator precedence) is a collection of rules that reflect conventions about which procedures to perform first in order to evaluate a given mathematical expression. For examp ...
in arithmetic. A common convention is: * \lnot is evaluated first * \land and \lor are evaluated next * Quantifiers are evaluated next * \to is evaluated last. Moreover, extra punctuation not required by the definition may be inserted—to make formulas easier to read. Thus the formula :\lnot \forall x P(x) \to \exists x \lnot P(x) might be written as :(\lnot forall x P(x) \to \exists x lnot P(x) 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. also term structure vs. representation. The definitions above use infix notation for binary connectives such as \to. A less common convention is
Polish notation Polish notation (PN), also known as normal Polish notation (NPN), Łukasiewicz notation, Warsaw notation, Polish prefix notation or simply prefix notation, is a mathematical notation in which operators ''precede'' their operands, in contrast ...
, in which one writes \rightarrow, \wedge 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 :\forall x \forall y (P(f(x)) \rightarrow\neg (P(x) \rightarrow Q(f(y),x,z))) becomes


Free and bound variables

In a formula, a variable may occur ''free'' or ''bound'' (or both). Intuitively, a variable occurrence is free in a formula if it is not quantified: in , the sole occurrence of variable ''x'' is free while that of ''y'' is bound. The free and bound variable occurrences in a formula are defined inductively as follows. ; 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. ; 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 ''φ'' ; 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 →. ; Quantifiers : ''x'' occurs free in , if and only if x occurs free in ''φ'' and ''x'' is a different symbol from ''y''. Also, ''x'' occurs bound in , if and only if ''x'' is ''y'' or ''x'' occurs bound in ''φ''. The same rule holds with in place of . For example, in , ''x'' and ''y'' occur only bound, ''z'' occurs only free, and ''w'' is neither because it does not occur in the formula. Free and bound variables of a formula need not be disjoint sets: in the formula , the first occurrence of ''x'', as argument of ''P'', is free while the second one, as argument of ''Q'', is bound. A formula in first-order logic with no free variable occurrences is called a ''first-order sentence''. These are the formulas that will have well-defined
truth value In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth, which in classical logic has only two possible values ('' true'' or '' false''). Computing In some pro ...
s under an interpretation. For example, whether a formula such as Phil(''x'') is true must depend on what ''x'' represents. But the sentence will be either true or false in a given interpretation.


Example: ordered abelian groups

In mathematics, the language of ordered
abelian groups In mathematics, an abelian group, also called a commutative group, is a group in which the result of applying the group operation to two group elements does not depend on the order in which they are written. That is, the group operation is commut ...
has one constant symbol 0, one unary function symbol −, one binary function symbol +, and one binary relation symbol ≤. Then: *The expressions +(''x'', ''y'') and +(''x'', +(''y'', −(''z''))) are ''terms''. These are usually written as ''x'' + ''y'' and ''x'' + ''y'' − ''z''. *The expressions +(''x'', ''y'') = 0 and ≤(+(''x'', +(''y'', −(''z''))), +(''x'', ''y'')) are ''atomic formulas''. These are usually written as ''x'' + ''y'' = 0 and ''x'' + ''y'' − ''z''  ≤  ''x'' + ''y''. *The expression (\forall x \forall y \, mathop(\mathop(x, y), z) \to \forall x\, \forall y\, \mathop(x, y) = 0)/math> is a ''formula'', which is usually written as \forall x \forall y ( x + y \leq z) \to \forall x \forall y (x+y = 0). This formula has one free variable, ''z''. 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 (\forall x)(\forall y) + y = y + x


Semantics

An
interpretation Interpretation may refer to: Culture * Aesthetic interpretation, an explanation of the meaning of a work of art * Allegorical interpretation, an approach that assumes a text should not be interpreted literally * Dramatic Interpretation, an event ...
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 a
domain of discourse In the formal sciences, the domain of discourse, also called the universe of discourse, universal set, or simply universe, is the set of entities over which certain variables of interest in some formal treatment may range. Overview The doma ...
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 called formal semantics. What follows is a description of the standard or Tarskian semantics for first-order logic. (It is also possible to define game semantics for first-order logic, but aside from requiring the
axiom of choice In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
, game semantics agree with Tarskian semantics for first-order logic, so game semantics will not be elaborated herein.)


First-order structures

The most common way of specifying an interpretation (especially in mathematics) is to specify a ''structure'' (also called a ''model''; see below). The structure consists of a domain of discourse ''D'' and an interpretation function mapping non-logical symbols to predicates, functions, and constants. The domain of discourse ''D'' 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, \exists x P(x) states the existence of some object in ''D'' for which the predicate ''P'' is true (or, more precisely, for which the predicate assigned to the predicate symbol ''P'' by the interpretation is true). For example, one can take ''D'' to be the set of
integers An integer is the number zero (), a positive natural number (, , , etc.) or a negative integer with a minus sign ( −1, −2, −3, etc.). The negative numbers are the additive inverses of the corresponding positive numbers. In the language ...
. Non-logical symbols are interpreted as follows: * The interpretation of an ''n''-ary function symbol is a function from ''D''''n'' to ''D''. For example, if the domain of discourse is the set of integers, a function symbol ''f'' of arity 2 can be interpreted as the function that gives the sum of its arguments. In other words, the symbol ''f'' is associated with the function which, in this interpretation, is addition. * The interpretation of a constant symbol (a function symbol of arity 0) is a function from ''D''0 (a set whose only member is the empty
tuple In mathematics, a tuple is a finite ordered list (sequence) of elements. An -tuple is a sequence (or ordered list) of elements, where is a non-negative integer. There is only one 0-tuple, referred to as ''the empty tuple''. An -tuple is defi ...
) to ''D'', which can be simply identified with an object in ''D''. For example, an interpretation may assign the value I(c)=10 to the constant symbol c. * The interpretation of an ''n''-ary predicate symbol is a set of ''n''-tuples of elements of ''D'', giving the arguments for which the predicate is true. 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. According to this interpretation, the predicate ''P'' would be true if its first argument is less than its second argument. Equivalently, predicate symbols may be assigned boolean-valued functions from ''D''''n'' to \.


Evaluation of truth values

A formula evaluates to true or false given an interpretation and a variable 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 y = x. The truth value of this formula changes depending on whether ''x'' and ''y'' denote the same individual. 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: * ''Variables''. Each variable ''x'' evaluates to ''μ''(''x'') * ''Functions''. Given terms t_1, \ldots, t_n that have been evaluated to elements d_1, \ldots, d_n of the domain of discourse, and a ''n''-ary function symbol ''f'', the term f(t_1, \ldots, t_n) evaluates to (I(f))(d_1,\ldots,d_n). Next, each formula is assigned a truth value. The inductive definition used to make this assignment is called the T-schema. * ''Atomic formulas (1)''. A formula P(t_1,\ldots,t_n) is associated the value true or false depending on whether \langle v_1,\ldots,v_n \rangle \in I(P), where v_1,\ldots,v_n are the evaluation of the terms t_1,\ldots,t_n and I(P) is the interpretation of P, which by assumption is a subset of D^n. * ''Atomic formulas (2)''. A formula t_1 = t_2 is assigned true if t_1 and t_2 evaluate to the same object of the domain of discourse (see the section on equality below). * ''Logical connectives''. A formula in the form \neg \varphi, \varphi \rightarrow \psi, etc. is evaluated according to the
truth table A truth table is a mathematical table used in logic—specifically in connection with Boolean algebra, boolean functions, and propositional calculus—which sets out the functional values of logical expressions on each of their functional arg ...
for the connective in question, as in propositional logic. * ''Existential quantifiers''. A formula \exists x \varphi(x) is true according to ''M'' and \mu if there exists an evaluation \mu' of the variables that only differs from \mu regarding the evaluation of ''x'' and such that φ is true according to the interpretation ''M'' and the variable assignment \mu'. This formal definition captures the idea that \exists x \varphi(x) is true if and only if there is a way to choose a value for ''x'' such that φ(''x'') is satisfied. * ''Universal quantifiers''. A formula \forall x \varphi(x) is true according to ''M'' and \mu if φ(''x'') is true for every pair composed by the interpretation ''M'' and some variable assignment \mu' that differs from \mu only on the value of ''x''. This captures the idea that \forall x \varphi(x) is true if every possible choice of a value for ''x'' causes φ(''x'') to be true. 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 to ''M'' and \mu if and only if it is true according to ''M'' and every other variable assignment \mu'. There is a second common approach to defining truth values that does not rely on variable assignment functions. 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 ''c''''d'' 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: * ''Existential quantifiers (alternate)''. A formula \exists x \varphi(x) is true according to ''M'' if there is some ''d'' in the domain of discourse such that \varphi(c_d) holds. Here \varphi(c_d) is the result of substituting ''c''''d'' for every free occurrence of ''x'' in φ. * ''Universal quantifiers (alternate)''. A formula \forall x \varphi(x) is true according to ''M'' if, for every ''d'' in the domain of discourse, \varphi(c_d) is true according to ''M''. This alternate approach gives exactly the same truth values to all sentences as the approach via variable assignments.


Validity, satisfiability, and logical consequence

If a sentence φ evaluates to ''true'' under a given interpretation ''M'', one says that ''M'' ''satisfies'' φ; this is denoted M \vDash \varphi. A sentence is ''satisfiable'' if there is some interpretation under which it is true. This is a bit different from the symbol \vDash from model theory, where M\vDash\phi denotes satisfiability in a model, i.e. "there is a suitable assignment of values in M's domain to variable symbols of \phi". 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 x_1, ..., x_n 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 x_1, ..., x_n. This has the same effect as saying that a formula φ is satisfied if and only if its
universal closure In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other w ...
\forall x_1 \dots \forall x_n \phi (x_1, \dots, x_n) is satisfied. A formula is ''logically valid'' (or simply ''valid'') if it is true in every interpretation. These formulas play a role similar to tautologies in propositional logic. A formula φ is a ''logical consequence'' of a formula ψ if every interpretation that makes ψ true also makes φ true. In this case one says that φ is logically implied by ψ.


Algebraizations

An alternate approach to the semantics of first-order logic proceeds via
abstract algebra In mathematics, more specifically algebra, abstract algebra or modern algebra is the study of algebraic structures. Algebraic structures include groups, rings, fields, modules, vector spaces, lattices, and algebras over a field. The ter ...
. This approach generalizes the Lindenbaum–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: *
Cylindric algebra In mathematics, the notion of cylindric algebra, invented by Alfred Tarski, arises naturally in the algebraization of first-order logic with equality. This is comparable to the role Boolean algebras play for propositional logic. Cylindric algebr ...
, by
Alfred Tarski Alfred Tarski (, born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician a ...
and colleagues; * Polyadic algebra, by
Paul Halmos Paul Richard Halmos ( hu, Halmos Pál; March 3, 1916 – October 2, 2006) was a Hungarian-born American mathematician and statistician who made fundamental advances in the areas of mathematical logic, probability theory, statistics, operator ...
; *
Predicate functor logic In mathematical logic, predicate functor logic (PFL) is one of several ways to express first-order logic (also known as predicate logic) by purely algebraic means, i.e., without quantified variables. PFL employs a small number of algebraic device ...
, mainly due to
Willard Quine Willard Van Orman Quine (; known to his friends as "Van"; June 25, 1908 – December 25, 2000) was an American philosopher and logician in the analytic tradition, recognized as "one of the most influential philosophers of the twentieth century" ...
. These
algebra Algebra () is one of the broad areas of mathematics. Roughly speaking, algebra is the study of mathematical symbols and the rules for manipulating these symbols in formulas; it is a unifying thread of almost all of mathematics. Elementary ...
s are all lattices that properly extend the two-element Boolean algebra. Tarski and Givant (1987) showed that the fragment of first-order logic that has no
atomic sentence In logic and analytic philosophy, an atomic sentence is a type of declarative sentence which is either true or false (may also be referred to as a proposition, statement or truthbearer) and which cannot be broken down into other simpler sentences ...
lying in the scope of more than three quantifiers has the same expressive power as
relation algebra In mathematics and abstract algebra, a relation algebra is a residuated Boolean algebra expanded with an involution called converse, a unary operation. The motivating example of a relation algebra is the algebra 2''X''² of all binary relations ...
. This fragment is of great interest because it suffices for
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearl ...
and most
axiomatic set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly concern ...
, including the canonical ZFC. They also prove that first-order logic with a primitive
ordered pair In mathematics, an ordered pair (''a'', ''b'') is a pair of objects. The order in which the objects appear in the pair is significant: the ordered pair (''a'', ''b'') is different from the ordered pair (''b'', ''a'') unless ''a'' = ''b''. (In con ...
is equivalent to a relation algebra with two ordered pair
projection function In set theory, a projection is one of two closely related types of functions or operations, namely: * A set-theoretic operation typified by the ''j''th projection map, written \mathrm_, that takes an element \vec = (x_1,\ \ldots,\ x_j,\ \ldots,\ x ...
s.


First-order theories, models, and elementary classes

A ''first-order theory'' of a particular signature is a set of
axiom An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or ...
s, which are sentences consisting of symbols from that signature. The set of axioms is often finite or
recursively enumerable In computability theory, a set ''S'' of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if: *There is an algorithm such that the ...
, in which case the theory is called ''effective''. 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 a ''model'' of the theory. An ''
elementary class In model theory, a branch of mathematical logic, an elementary class (or axiomatizable class) is a class consisting of all structures satisfying a fixed first-order theory. Definition A class ''K'' of structures of a signature σ is called an ...
'' is the set of all structures satisfying a particular theory. These classes are a main subject of study in
model theory In mathematical logic, model theory is the study of the relationship between theory (mathematical logic), formal theories (a collection of Sentence (mathematical logic), sentences in a formal language expressing statements about a Structure (math ...
. Many theories have an '' intended interpretation'', a certain model that is kept in mind when studying the theory. For example, the intended interpretation of
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearl ...
consists of the usual
natural number In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country"). Numbers used for counting are called '' cardinal ...
s with their usual operations. However, the Löwenheim–Skolem theorem shows that most first-order theories will also have other, nonstandard models. A theory is '' consistent'' if it is not possible to prove a contradiction from the axioms of the theory. A theory is ''
complete Complete may refer to: Logic * Completeness (logic) * Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable Mathematics * The completeness of the real numbers, which implies t ...
'' 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.


Empty domains

The definition above requires that the domain of discourse of any interpretation must be nonempty. There are settings, such as inclusive logic, where empty domains are permitted. Moreover, if a class of algebraic structures includes an empty structure (for example, there is an empty
poset In mathematics, especially order theory, a partially ordered set (also poset) formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary r ...
), 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: * Many common rules of inference are only valid when the domain of discourse is required to be nonempty. One example is the rule stating that \varphi \lor \exists x \psi implies \exists x (\varphi \lor \psi) when ''x'' is not a free variable in \varphi. This rule, which is used to put formulas into
prenex normal form A formula of the predicate calculus is in prenex normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier-free part, called the matrix. Together with the normal forms in pro ...
, is sound in nonempty domains, but unsound if the empty domain is permitted. * The definition of truth in an interpretation that uses a variable assignment function cannot work with empty domains, because there are no variable assignment functions whose range is empty. (Similarly, one cannot assign interpretations to constant symbols.) This truth definition requires that one must select a variable assignment function (μ above) before truth values for even atomic formulas can be defined. Then the truth value of a sentence is defined to be its truth value under any variable assignment, and it is proved that this truth value does not depend on which assignment is chosen. This technique does not work if there are no assignment functions at all; it must be changed to accommodate empty domains. 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.


Deductive systems

A ''deductive 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, including
Hilbert-style deductive system :''In mathematical physics, ''Hilbert system'' is an infrequently used term for a physical system described by a C*-algebra.'' In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductiv ...
s,
natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use ax ...
, the
sequent calculus In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...
, the tableaux method, and resolution. 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 called ''derivations'' in proof theory. They are also often called ''proofs'', but are completely formalized unlike natural-language
mathematical proofs A mathematical proof is an inferential argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proo ...
. A deductive system is ''sound'' if any formula that can be derived in the system is logically valid. Conversely, a deductive system is ''complete'' 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 called ''effective''. 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 only
semidecidable In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer. Zeroth-order logic (propositional logic) is decidable, whereas first-order and higher-order logic are not. Logical systems a ...
: 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.


Rules of inference

A ''
rule of inference In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...
'' 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 the ''rule of substitution''. 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 φ. 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. (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''.) To see why the restriction on bound variables is necessary, consider the logically valid formula φ given by \exists x (x = y), in the signature of (0,1,+,×,=) of arithmetic. If ''t'' is the term "x + 1", the formula φ 't''/''y''is \exists x ( x = x+1), which will be false in many interpretations. The problem is that the free variable ''x'' of ''t'' became bound during the substitution. The intended replacement can be obtained by renaming the bound variable ''x'' of φ to something else, say ''z'', so that the formula after substitution is \exists z ( z = x+1), 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.


Hilbert-style systems and natural deduction

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. The logical axioms consist of several
axiom schema In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom. Formal definition An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables ap ...
s 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 only
modus ponens In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference ...
and
universal generalization In predicate logic, generalization (also universal generalization or universal introduction,Moore and Parker GEN) is a valid inference rule. It states that if \vdash \!P(x) has been derived, then \vdash \!\forall x \, P(x) can be derived. Gener ...
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.


Sequent calculus

The sequent calculus was developed to study the properties of natural deduction systems. Instead of working with one formula at a time, it uses ''sequents'', which are expressions of the form :A_1, \ldots, A_n \vdash B_1, \ldots, B_k, where A1, ..., A''n'', B1, ..., B''k'' are formulas and the turnstile symbol \vdash is used as punctuation to separate the two halves. Intuitively, a sequent expresses the idea that (A_1 \land \cdots\land A_n) implies (B_1\lor\cdots\lor B_k).


Tableaux method

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 \lnot A at its root; the tree branches in a way that reflects the structure of the formula. For example, to show that C \lor D is unsatisfiable requires showing that C and D are each unsatisfiable; this corresponds to a branching point in the tree with parent C \lor D and children C and D.


Resolution

The resolution rule is a single rule of inference that, together with unification, 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 through
Skolemization In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its ...
. The resolution rule states that from the hypotheses A_1 \lor\cdots\lor A_k \lor C and B_1\lor\cdots\lor B_l\lor\lnot C, the conclusion A_1\lor\cdots\lor A_k\lor B_1\lor\cdots\lor B_l can be obtained.


Provable identities

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 in
prenex normal form A formula of the predicate calculus is in prenex normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier-free part, called the matrix. Together with the normal forms in pro ...
. Some provable identities include: :\lnot \forall x \, P(x) \Leftrightarrow \exists x \, \lnot P(x) :\lnot \exists x \, P(x) \Leftrightarrow \forall x \, \lnot P(x) :\forall x \, \forall y \, P(x,y) \Leftrightarrow \forall y \, \forall x \, P(x,y) :\exists x \, \exists y \, P(x,y) \Leftrightarrow \exists y \, \exists x \, P(x,y) :\forall x \, P(x) \land \forall x \, Q(x) \Leftrightarrow \forall x \, (P(x) \land Q(x)) :\exists x \, P(x) \lor \exists x \, Q(x) \Leftrightarrow \exists x \, (P(x) \lor Q(x)) :P \land \exists x \, Q(x) \Leftrightarrow \exists x \, (P \land Q(x)) (where x must not occur free in P) :P \lor \forall x \, Q(x) \Leftrightarrow \forall x \, (P \lor Q(x)) (where x must not occur free in P)


Equality and its axioms

There are several different conventions for using equality (or identity) in first-order logic. 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. This approach also adds certain axioms about equality to the deductive system employed. These equality axioms are: * ''Reflexivity''. For each variable ''x'', ''x'' = ''x''. * ''Substitution for functions''. For all variables ''x'' and ''y'', and any function symbol ''f'', *:''x'' = ''y'' → ''f''(..., ''x'', ...) = ''f''(..., ''y'', ...). * ''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'', then *:''x'' = ''y'' → (φ → φ'). These are
axiom schema In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom. Formal definition An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables ap ...
s, each of which specifies an infinite set of axioms. The third schema is known as '' Leibniz's law'', "the principle of substitutivity", "the indiscernibility of identicals", or "the replacement property". The second schema, involving the function symbol ''f'', is (equivalent to) a special case of the third schema, using the formula :''x'' = ''y'' → (''f''(..., ''x'', ...) = ''z'' → ''f''(..., ''y'', ...) = ''z''). Many other properties of equality are consequences of the axioms above, for example: * ''Symmetry''. If ''x'' = ''y'' then ''y'' = ''x''. * ''Transitivity''. If ''x'' = ''y'' and ''y'' = ''z'' then ''x'' = ''z''.


First-order logic without equality

An alternate approach considers the equality relation to be a non-logical symbol. This convention is known as ''first-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 arbitrary
equivalence relation In mathematics, an equivalence relation is a binary relation that is reflexive, symmetric and transitive. The equipollence relation between line segments in geometry is a common example of an equivalence relation. Each equivalence relatio ...
on the domain of discourse that is congruent with respect to the functions and relations of the interpretation. 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''. 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 the
Löwenheim–Skolem theorem In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem. The precise formulation is given below. It implies that if a countable first-ord ...
so that only normal models are considered. First-order logic without equality is often employed in the context of
second-order arithmetic In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. A precur ...
and other higher-order theories of arithmetic, where the equality relation between sets of natural numbers is usually omitted.


Defining equality within a theory

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. 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 to
define A definition is a statement of the meaning of a term (a word, phrase, or other set of symbols). Definitions can be classified into two large categories: intensional definitions (which try to give the sense of a term), and extensional defini ...
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. Some theories allow other ''ad hoc'' definitions of equality: * In the theory of
partial order In mathematics, especially order theory, a partially ordered set (also poset) formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary ...
s with one relation symbol ≤, one could define ''s'' = ''t'' to be an abbreviation for ''s'' ≤ ''t'' ∧ ''t'' ≤ ''s''. * In set theory with one relation ∈, one may define ''s'' = ''t'' to be an abbreviation for . This definition of equality then automatically satisfies the axioms for equality. In this case, one should replace the usual
axiom of extensionality In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of extensionality, or axiom of extension, is one of the axioms of Zermelo–Fraenkel set theory. It says that sets having the same elements ...
, which can be stated as \forall x \forall y \forall z (z \in x \Leftrightarrow z \in y) \Rightarrow x = y/math>, with an alternative formulation \forall x \forall y \forall z (z \in x \Leftrightarrow z \in y) \Rightarrow \forall z (x \in z \Leftrightarrow y \in z) /math>, which says that if sets ''x'' and ''y'' have the same elements, then they also belong to the same sets.


Metalogical properties

One motivation for the use of first-order logic, rather than
higher-order logic mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
, is that first-order logic has many
metalogic Metalogic is the study of the metatheory of logic. Whereas ''logic'' studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems.Harry GenslerIntroduction to Logic Routledge, ...
al 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.


Completeness and undecidability

Gödel's completeness theorem Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. The completeness theorem applies to any first-order theory: ...
, proved by
Kurt Gödel Kurt Friedrich Gödel ( , ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel had an imm ...
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 is
semidecidable In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer. Zeroth-order logic (propositional logic) is decidable, whereas first-order and higher-order logic are not. Logical systems a ...
: it is possible to make an effective enumeration of all pairs of sentences (φ,ψ) such that ψ is a logical consequence of φ. Unlike
propositional logic Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
, first-order logic is undecidable (although semidecidable), provided that the language has at least one predicate of arity at least 2 (other than equality). This means that there is no
decision procedure In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm wheth ...
that determines whether arbitrary formulas are logically valid. This result was established independently by
Alonzo Church Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scien ...
and
Alan Turing Alan Mathison Turing (; 23 June 1912 – 7 June 1954) was an English mathematician, computer scientist, logician, cryptanalyst, philosopher, and theoretical biologist. Turing was highly influential in the development of theoretical ...
in 1936 and 1937, respectively, giving a negative answer to the
Entscheidungsproblem In mathematics and computer science, the ' (, ) is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem asks for an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the state ...
posed by
David Hilbert David Hilbert (; ; 23 January 1862 – 14 February 1943) was a German mathematician, one of the most influential mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many ...
and Wilhelm Ackermann in 1928. Their proofs demonstrate a connection between the unsolvability of the decision problem for first-order logic and the unsolvability of the
halting problem In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a ...
. There are systems weaker than full first-order logic for which the logical consequence relation is decidable. These include propositional logic and monadic 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 the
guarded fragment Guarded logic is a choice set of dynamic logic involved in choices, where outcomes are limited. A simple example of guarded logic is as follows: if X is true, then Y, else Z can be expressed in dynamic logic as (X?;Y)∪(~X?;Z). This shows a guard ...
of first-order logic, as well as two-variable logic. The
Bernays–Schönfinkel class The Bernays–Schönfinkel class (also known as Bernays–Schönfinkel–Ramsey class) of formulas, named after Paul Bernays, Moses Schönfinkel and Frank P. Ramsey, is a fragment of first-order logic formulas where satisfiability is decidable. I ...
of first-order formulas is also decidable. Decidable subsets of first-order logic are also studied in the framework of description logics.


The Löwenheim–Skolem theorem

The
Löwenheim–Skolem theorem In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem. The precise formulation is given below. It implies that if a countable first-ord ...
shows that if a first-order theory of
cardinality In mathematics, the cardinality of a set is a measure of the number of elements of the set. For example, the set A = \ contains 3 elements, and therefore A has a cardinality of 3. Beginning in the late 19th century, this concept was generalized ...
λ has an infinite model, then it has models of every infinite cardinality greater than or equal to λ. One of the earliest results in
model theory In mathematical logic, model theory is the study of the relationship between theory (mathematical logic), formal theories (a collection of Sentence (mathematical logic), sentences in a formal language expressing statements about a Structure (math ...
, it implies that it is not possible to characterize
countability In mathematics, a set is countable if either it is finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function from it into the natural numbe ...
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 be categorically 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 some nonstandard models. When the Löwenheim–Skolem theorem is applied to first-order set theories, the nonintuitive consequences are known as
Skolem's paradox In mathematical logic and philosophy, Skolem's paradox is a seeming contradiction that arises from the downward Löwenheim–Skolem theorem. Thoralf Skolem (1922) was the first to discuss the seemingly contradictory aspects of the theorem, and to ...
.


The compactness theorem

The
compactness theorem In mathematical logic, 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. This theorem is an important tool in model theory, as it provides a useful (but generally ...
states that a set of first-order sentences has a model if and only if every finite subset of it has a model. 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 finite graphs 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 a
directed graph In mathematics, and more specifically in graph theory, a directed graph (or digraph) is a graph that is made up of a set of vertices connected by directed edges, often called arcs. Definition In formal terms, a directed graph is an ordered pa ...
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 different connected 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 the
logic of graphs In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using sentences of mathematical logic. There are several variations in the types of logical operation that ...
, that expresses the idea that there is a path from ''x'' to ''y''. Connectedness can be expressed in
second-order logic In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies on ...
, however, but not with only existential set quantifiers, as \Sigma_1^1 also enjoys compactness.


Lindström's theorem

Per Lindström Per "Pelle" Lindström (9 April 1936 – 21 August 2009, Gothenburg)ASLbr>Newsletter September 2009 was a Swedish logician, after whom Lindström's theorem and the Lindström quantifier are named. (He also independently discovered Ehrenfeucht� ...
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: * 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. * 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.


Limitations

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 the
counting quantifiers A counting quantifier is a mathematical term for a quantifier of the form "there exists at least ''k'' elements that satisfy property ''X''". In first-order logic with equality, counting quantifiers can be defined in terms of ordinary quantifiers, ...
\exists^ and \exists^.


Expressiveness

The
Löwenheim–Skolem theorem In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem. The precise formulation is given below. It implies that if a countable first-ord ...
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 be categorical. 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. This expressiveness comes at a metalogical cost, however: by
Lindström's theorem In mathematical logic, Lindström's theorem (named after Swedish logician Per Lindström, who published it in 1969) states that first-order logic is the '' strongest logic'' (satisfying certain conditions, e.g. closure under classical negation) h ...
, the compactness theorem and the downward Löwenheim–Skolem theorem cannot hold in any logic stronger than first-order.


Formalizing natural languages

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 for knowledge representation languages, such as FO(.). 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".


Restrictions, extensions, and variations

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.


Restricted languages

First-order logic can be studied in languages with fewer logical symbols than were described above. * Because \exists x \varphi(x) can be expressed as \neg \forall x \neg \varphi(x), and \forall x \varphi(x) can be expressed as \neg \exists x \neg \varphi(x), either of the two quantifiers \exists and \forall can be dropped. * Since \varphi \lor \psi can be expressed as \lnot (\lnot \varphi \land \lnot \psi) and \varphi \land \psi can be expressed as \lnot(\lnot \varphi \lor \lnot \psi), either \vee or \wedge can be dropped. In other words, it is sufficient to have \neg and \vee, or \neg and \wedge, as the only logical connectives. * Similarly, it is sufficient to have only \neg and \rightarrow as logical connectives, or to have only the Sheffer stroke (NAND) or the Peirce arrow (NOR) operator. * It is possible to entirely avoid function symbols and constant symbols, rewriting them via predicate symbols in an appropriate way. For example, instead of using a constant symbol \; 0 one may use a predicate \; 0(x) (interpreted as \; x=0 ), and replace every predicate such as \; P(0,y) with \forall x \;(0(x) \rightarrow P(x,y)) . A function such as f(x_1,x_2,...,x_n) will similarly be replaced by a predicate F(x_1,x_2,...,x_n,y) interpreted as y = f(x_1,x_2,...,x_n) . This change requires adding additional axioms to the theory at hand, so that interpretations of the predicate symbols used have the correct semantics. 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 a
pairing function In mathematics, a pairing function is a process to uniquely encode two natural numbers into a single natural number. Any pairing function can be used in set theory to prove that integers and rational numbers have the same cardinality as natural ...
. This is a function of arity 2 that takes pairs of elements of the domain and returns an
ordered pair In mathematics, an ordered pair (''a'', ''b'') is a pair of objects. The order in which the objects appear in the pair is significant: the ordered pair (''a'', ''b'') is different from the ordered pair (''b'', ''a'') unless ''a'' = ''b''. (In con ...
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.


Many-sorted logic

Ordinary first-order interpretations have a single domain of discourse over which all quantifiers range. ''Many-sorted first-order logic'' allows variables to have different ''sorts'', which have different domains. This is also called ''typed first-order logic'', and the sorts called ''types'' (as in
data type In computer science and computer programming, a data type (or simply type) is a set of possible values and a set of allowed operations on it. A data type tells the compiler or interpreter how the programmer intends to use the data. Most progra ...
), but it is not the same as first-order
type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a founda ...
. Many-sorted first-order logic is often used in the study of
second-order arithmetic In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. A precur ...
. When there are only finitely many sorts in a theory, many-sorted first-order logic can be reduced to single-sorted first-order logic. 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 P_1(x) and P_2(x) and the axiom :\forall x ( P_1(x) \lor P_2(x)) \land \lnot \exists x (P_1(x) \land P_2(x)). Then the elements satisfying P_1 are thought of as elements of the first sort, and elements satisfying P_2 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 φ(''x''), one writes :\exists x (P_1(x) \land \varphi(x)).


Additional quantifiers

Additional quantifiers can be added to first-order logic. * Sometimes it is useful to say that " holds for exactly one ''x''", which can be expressed as . This notation, called
uniqueness quantification In mathematics and logic, the term "uniqueness" refers to the property of being the one and only object satisfying a certain condition. This sort of quantification is known as uniqueness quantification or unique existential quantification, and ...
, may be taken to abbreviate a formula such as . *''First-order logic with extra quantifiers'' has new quantifiers ''Qx'',..., with meanings such as "there are many ''x'' such that ...". Also see
branching quantifier In logic a branching quantifier, also called a Henkin quantifier, finite partially ordered quantifier or even nonlinear quantifier, is a partial ordering :\langle Qx_1\dots Qx_n\rangle of quantifiers for ''Q'' ∈ . It is a special case ...
s and the plural quantifiers of
George Boolos George Stephen Boolos (; 4 September 1940 – 27 May 1996) was an American philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology. Life Boolos is of Greek- Jewish descent. He graduated with an A.B. ...
and others. * ''
Bounded quantifier In the study of formal theories in mathematical logic, bounded quantifiers (a.k.a. restricted quantifiers) are often included in a formal language in addition to the standard quantifiers "∀" and "∃". Bounded quantifiers differ from "∀" and ...
s'' are often used in the study of set theory or arithmetic.


Infinitary logics

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 including
topology In mathematics, topology (from the Greek words , and ) is concerned with the properties of a geometric object that are preserved under continuous deformations, such as stretching, twisting, crumpling, and bending; that is, without closing ...
and
model theory In mathematical logic, model theory is the study of the relationship between theory (mathematical logic), formal theories (a collection of Sentence (mathematical logic), sentences in a formal language expressing statements about a Structure (math ...
. 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 denoted ''L''αβ, where α and β are each either
cardinal number In mathematics, cardinal numbers, or cardinals for short, are a generalization of the natural numbers used to measure the cardinality (size) of sets. The cardinality of a finite set is a natural number: the number of elements in the set. ...
s or the symbol ∞. In this notation, ordinary first-order logic is ''L''ωω. In the logic ''L''∞ω, 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 as ''L''κω. For example, ''L''ω1ω permits
countable In mathematics, a set is countable if either it is finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function from it into the natural numbers ...
conjunctions and disjunctions. 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. In other infinitary logics, a subformula may be in the scope of infinitely many quantifiers. For example, in ''L''κ∞, a single universal or existential quantifier may bind arbitrarily many variables simultaneously. Similarly, the logic ''L''κλ permits simultaneous quantification over fewer than λ variables, as well as conjunctions and disjunctions of size less than κ.


Non-classical and modal logics

*'' Intuitionistic first-order logic'' uses intuitionistic rather than classical propositional calculus; for example, ¬¬φ need not be equivalent to φ. *First-order ''
modal logic Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend ot ...
'' 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 fuzzy logics'' are first-order extensions of propositional fuzzy logics rather than classical
propositional calculus Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
.


Fixpoint logic

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


Higher-order logics

The characteristic feature of first-order logic is that individuals can be quantified, but not predicates. Thus :\exists a ( \text(a)) is a legal first-order formula, but :\exists \text ( \text(a)) is not, in most formalizations of first-order logic.
Second-order logic In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies on ...
extends first-order logic by adding the latter type of quantification. Other
higher-order logic mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
s allow quantification over even higher types 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 as ''full 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 and formal methods

Automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ...
refers to the development of computer programs that search and find derivations (formal proofs) of mathematical theorems. 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. Thus complicated heuristic functions are developed to attempt to find a derivation in less time than a blind search. The related area of automated proof 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 as Metamath, insist on having a complete derivation as input. Others, such as Mizar and
Isabelle Isabel is a female name of Spanish origin. Isabelle is a name that is similar, but it is of French origin. It originates as the medieval Spanish form of ''Elizabeth (given name), Elisabeth'' (ultimately Hebrew ''Elisheba, Elisheva''), Arising in ...
, 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 as
proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof edi ...
s. 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, Avigad, ''et al.'' (2007) discuss the process of formally verifying a proof of the
prime number theorem In mathematics, the prime number theorem (PNT) describes the asymptotic distribution of the prime numbers among the positive integers. It formalizes the intuitive idea that primes become less common as they become larger by precisely quantifying t ...
. The formalized proof required approximately 30,000 lines of input to the Isabelle proof verifier.
results are often formalized as a series of lemmas, for which derivations can be constructed separately. Automated theorem provers are also used to implement
formal verification In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal met ...
in computer science. In this setting, theorem provers are used to verify the correctness of programs and of hardware such as
processors A central processing unit (CPU), also called a central processor, main processor or just processor, is the electronic circuitry that executes instructions comprising a computer program. The CPU performs basic arithmetic, logic, controlling, a ...
with respect to a
formal specification In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verif ...
. 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 of
model checking In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software system ...
, efficient
algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...
s are known to decide whether an input finite structure satisfies a first-order formula, in addition to
computational complexity In computer science, the computational complexity or simply complexity of an algorithm is the amount of resources required to run it. Particular focus is given to computation time (generally measured by the number of needed elementary operations) ...
bounds: see .


See also

*
ACL2 ACL2 ("A Computational Logic for Applicative Common Lisp") is a software system consisting of a programming language, created by Timothy Still it was an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed ...
— A Computational Logic for Applicative Common Lisp *
Aristotelian logic In philosophy, term logic, also known as traditional logic, syllogistic logic or Aristotelian logic, is a loose name for an approach to formal logic that began with Aristotle and was developed further in ancient history mostly by his followers, ...
*
Equiconsistency In mathematical logic, two theories are equiconsistent if the consistency of one theory implies the consistency of the other theory, and vice versa. In this case, they are, roughly speaking, "as consistent as each other". In general, it is not ...
* Ehrenfeucht-Fraisse game *
Extension by definitions In mathematical logic, more specifically in the proof theory of first-order theories, extensions by definitions formalize the introduction of new symbols by means of a definition. For example, it is common in naive set theory to introduce a symbol ...
*
Extension (predicate logic) The extension of a predicatea truth-valued functionis the set of tuples of values that, used as arguments, satisfy the predicate. Such a set of tuples is a relation. Examples For example, the statement "''d2'' is the weekday following ''d1''" c ...
*
Herbrandization {{Short description, Proof of Herbrand's theorem The Herbrandization of a logical formula (named after Jacques Herbrand) is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formul ...
* List of logic symbols * Löwenheim number *
Nonfirstorderizability In formal logic, nonfirstorderizability is the inability of a natural-language statement to be adequately captured by a formula of first-order logic. Specifically, a statement is nonfirstorderizable if there is no formula of first-order logic whic ...
*
Prenex normal form A formula of the predicate calculus is in prenex normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier-free part, called the matrix. Together with the normal forms in pro ...
*
Prior Analytics The ''Prior Analytics'' ( grc-gre, Ἀναλυτικὰ Πρότερα; la, Analytica Priora) is a work by Aristotle on reasoning, known as his syllogistic, composed around 350 BCE. Being one of the six extant Aristotelian writings on logic a ...
*
Prolog Prolog is a logic programming language associated with artificial intelligence and computational linguistics. Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily ...
* Relational algebra *
Relational model The relational model (RM) is an approach to managing data using a structure and language consistent with first-order predicate logic, first described in 1969 by English computer scientist Edgar F. Codd, where all data is represented in terms of t ...
* Skolem normal form * Tarski's World *
Truth table A truth table is a mathematical table used in logic—specifically in connection with Boolean algebra, boolean functions, and propositional calculus—which sets out the functional values of logical expressions on each of their functional arg ...
* Type (model theory)


Notes


References

* * Andrews, Peter B. (2002);
An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof
', 2nd ed., Berlin: Kluwer Academic Publishers. Available from Springer. * Avigad, Jeremy; Donnelly, Kevin; Gray, David; and Raff, Paul (2007); "A formally verified proof of the prime number theorem", ''ACM Transactions on Computational Logic'', vol. 9 no. 1 * * * Barwise, Jon; and Etchemendy, John (2000); ''Language Proof and Logic'', Stanford, CA: CSLI Publications (Distributed by the University of Chicago Press) * Bocheński, Józef Maria (2007); ''A Précis of Mathematical Logic'', Dordrecht, NL: D. Reidel, translated from the French and German editions by Otto Bird * Ferreirós, José (2001)
''The Road to Modern Logic — An Interpretation''
Bulletin of Symbolic Logic, Volume 7, Issue 4, 2001, pp. 441–484, , * * Hilbert, David; and Ackermann, Wilhelm (1950); ''
Principles of Mathematical Logic ''Principles of Mathematical Logic'' is the 1950 American translation of the 1938 second edition of David Hilbert's and Wilhelm Ackermann's classic text ''Grundzüge der theoretischen Logik'', on elementary mathematical logic. The 1928 first editi ...
'', Chelsea (English translation of ''Grundzüge der theoretischen Logik'', 1928 German first edition) * Hodges, Wilfrid (2001); "Classical Logic I: First-Order Logic", in Goble, Lou (ed.); ''The Blackwell Guide to Philosophical Logic'', Blackwell * Ebbinghaus, Heinz-Dieter; Flum, Jörg; and Thomas, Wolfgang (1994)
Logic''
Undergraduate Texts in Mathematics Undergraduate Texts in Mathematics (UTM) (ISSN 0172-6056) is a series of undergraduate-level textbooks in mathematics published by Springer-Verlag. The books in this series, like the other Springer-Verlag mathematics series, are small yellow bo ...
, Berlin, DE/New York, NY:
Springer-Verlag Springer Science+Business Media, commonly known as Springer, is a German multinational publishing company of books, e-books and peer-reviewed journals in science, humanities, technical and medical (STM) publishing. Originally founded in 1842 ...
, Second Edition, * Tarski, Alfred and Givant, Steven (1987); ''A Formalization of Set Theory without Variables''. Vol.41 of American Mathematical Society colloquium publications, Providence RI: American Mathematical Society,


External links

* *
Stanford Encyclopedia of Philosophy The ''Stanford Encyclopedia of Philosophy'' (''SEP'') combines an online encyclopedia of philosophy with peer-reviewed publication of original papers in philosophy, freely accessible to Internet users. It is maintained by Stanford University. E ...
: Shapiro, Stewart;
Classical Logic
. Covers syntax, model theory, and metatheory for first-order logic in the natural deduction style. * Magnus, P. D.;
forall x: an introduction to formal logic
'. Covers formal semantics and proof theory for first-order logic.

an ongoing online project to reconstruct mathematics as a huge first-order theory, using first-order logic and the
axiomatic set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly concern ...
ZFC. ''
Principia Mathematica The ''Principia Mathematica'' (often abbreviated ''PM'') is a three-volume work on the foundations of mathematics written by mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913. ...
'' modernized. * Podnieks, Karl;
Introduction to mathematical logic
'

(typeset by John Fremlin). These notes cover part of a past Cambridge Mathematical Tripos course taught to undergraduate students (usually) within their third year. The course is entitled "Logic, Computation and Set Theory" and covers Ordinals and cardinals, Posets and Zorn's Lemma, Propositional logic, Predicate logic, Set theory and Consistency issues related to ZFC and other set theories.
Tree Proof Generator
can validate or invalidate formulas of first-order logic through the semantic tableaux method. {{DEFAULTSORT:First-Order Logic Systems of formal logic Predicate logic Model theory