First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of
formal systems used in
mathematics,
philosophy,
linguistics, and
computer science. First-order logic 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, 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 (over which the quantified variables range), finitely many functions from that domain to itself, finitely many
predicates
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, ...
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, 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 form ...
s for first-order logic which are both
sound (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 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 syste ...
, 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 m ...
in first-order logic. First-order logic also satisfies several
metalogical 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 parts, ...
, such as the
Löwenheim–Skolem theorem 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 generall ...
.
First-order logic is the standard for the formalization of mathematics into
axioms
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 ...
, 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 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 a ...
are axiomatizations of
number theory and
set theory, respectively, into first-order logic.
No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the
natural numbers 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 poin ...
. 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.
The foundations of first-order logic were developed independently by
Gottlob Frege 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 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 and evaluates to
true or
false. Consider the two sentences "Socrates is a philosopher" and "Plato is a philosopher". In
propositional logic, 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 co ...
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 "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'' 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 "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 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''", 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 determines which finite sequences of symbols are well-formed expressions in first-order logic, while the
semantics 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 languages, the nature of the symbols themselves is outside the scope of formal logic; they are often regarded simply as letters and punctuation symbols.
It is common to divide the symbols of the alphabet into ''logical symbols'', which always have the same meaning, and ''non-logical symbols'', whose meaning varies by interpretation. For example, the logical symbol
always represents "and"; it is never interpreted as "or", which is represented by the logical symbol
. However, a non-logical predicate symbol such as Phil(''x'') could be interpreted to mean "''x'' is a philosopher", "''x'' is a man named Philip", or any other unary predicate depending on the interpretation at hand.
Logical symbols
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 co ...
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 S ...
, for
implication, for
biconditional
In logic and mathematics, the logical biconditional, sometimes known as the material biconditional, is the logical connective (\leftrightarrow) used to conjoin two statements and to form the statement " if and only if ", where is known as th ...
, 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.)
* 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, J''pq''.
Non-logical symbols
Non-logical symbols
In logic, the formal languages used to create expressions consist of symbols, which can be broadly divided into constants and variables. The constants of a language can further be divided into logical symbols and non-logical symbols (sometimes a ...
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''.
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 fields. There are no restrictions on the number of non-logical symbols. The signature can be
empty, finite, or infinite, even
uncountable. Uncountable signatures occur for example in modern proofs of the
Löwenheim–Skolem theorem.
Though signatures might in some cases imply how non-logical symbols are to be interpreted,
interpretation of the non-logical symbols in the signature is separate (and not necessarily fixed). Signatures concern syntax rather than semantics.
In this approach, every non-logical symbol is of one of the following types:
* 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
The Latin script, also known as Roman script, is an alphabetic writing system based on the letters of the classical Latin alphabet, derived from a form of the Greek alphabet which was in use in the ancient Greek city of Cumae, in southern It ...
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 c ...
, it may stand for "-x". In
set theory, it may stand for "the
power set of x".
** In arithmetic, ''g''(''x'',''y'') may stand for "''x''+''y''". In set theory, it may stand for "the union of ''x'' and ''y''".
** 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 other ...
.
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 rules 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
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a '' chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betw ...
'' (also called ''
well-formed formulas'' 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
Equality may refer to:
Society
* Political equality, in which all members of a society are of equal standing
** Consociationalism, in which an ethnically, religiously, or linguistically divided state functions by cooperation of each group's elite ...
''. 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
is a formula, then
is a formula.
* ''Binary connectives''. If and are formulas, then (
) is a formula. Similar rules apply to other binary logical connectives.
* ''Quantifiers''. If
is a formula and ''x'' is a variable, then
(for all x,
holds) and
(there exists x such that
) 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 subformul ...
s''.
For example,
:
is a formula, if ''f'' is a unary function symbol, ''P'' a unary predicate symbol, and Q a ternary predicate symbol. However,
is not a formula, although it is a string of symbols from the alphabet.
The role of the parentheses in the definition is to ensure that any formula can only be obtained in one way—by following the inductive definition (i.e., there is a unique
parse tree 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 arithmetic. A common convention is:
*
is evaluated first
*
and
are evaluated next
* Quantifiers are evaluated next
*
is evaluated last.
Moreover, extra punctuation not required by the definition may be inserted—to make formulas easier to read. Thus the formula
:
might be written as
:
In some fields, it is common to use infix notation for binary relations and functions, instead of the prefix notation defined above. For example, in arithmetic, one typically writes "2 + 2 = 4" instead of "=(+(2,2),4)". It is common to regard formulas in infix notation as abbreviations for the corresponding formulas in prefix notation, cf. also
term structure vs. representation.
The definitions above use infix notation for binary connectives such as
. A less common convention is
Polish notation, in which one writes
,
and so on in front of their arguments rather than between them. This convention is advantageous in that it allows all punctuation symbols to be discarded. As such, Polish notation is compact and elegant, but rarely used in practice because it is hard for humans to read. In Polish notation, the formula
:
becomes
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 values 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 com ...
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