First-order logic is a formal logic used in
mathematicsMathematics is the science and study of quantity, structure, space, and change. Mathematicians seek out patterns, formulate new conjectures, and establish truth by rigorous deduction from appropriately chosen axioms and definitions....
,
philosophyPhilosophy is the study of general and fundamental problems concerning matters such as existence, knowledge, values, reason, mind, and language. Philosophy is distinguished from other ways of addressing these questions by its critical, generally systematic approach and its reliance on reasoned...
,
linguisticsLinguistics is the scientific study of natural language. Linguistics encompasses a number of sub-fields. An important topical division is between the study of language structure and the study of meaning...
, and
computer scienceComputer science is the study of the theoretical foundations of information and computation, and of practical techniques for their implementation and application in computer systems. It is frequently described as the systematic study of algorithmic processes that create, describe and transform...
. It goes by many names, including:
first-order predicate calculus, the
lower predicate calculus, and
predicate logicIn mathematical logic, predicate logic is the generic term for symbolic formal systems like first-order logic, second-order logic, many-sorted logic or infinitary logic. This formal system is distinguished from other systems in that its formulas contain variables which can be quantified. Two common...
. First-order logic is distinguished from propositional logic by its use of quantifiers; each interpretation of first-order logic includes a
domain of discourseThe domain of discourse, sometimes called the universe of discourse, logical discourse, or simply discourse, is an analytic tool used in deductive logic, especially predicate logic...
over which the quantifiers range.
There are many
deductive systemA deductive system consists of the axioms and rules of inference that can be used to derive the theorems of the system....
s for first-order logic that are sound (only deriving correct results) and complete (able to derive any logically valid implication). Although the logical consequence relation is only semidecidable, much progress has been made in
automated theorem provingAutomated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
in first-order logic. First-order logic also satisfies several
metalogicMetalogic is the study of the metatheory of logic. While logic is the study of the manner in which logical systems can be used to decide the correctness of arguments, metalogic studies the properties of the logical systems themselves...
al theorems that make it amenable to analysis in
proof theoryProof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, such as the
Löwenheim–Skolem theoremIn mathematical logic, the Löwenheim–Skolem theorem states that if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ...
and the
compactness theoremIn 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...
.
First-order logic is of great importance to the
foundations of mathematicsFoundations of mathematics is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, type theory and recursion theory...
, where it has become the standard formal logic for
axiomatic systemIn mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A mathematical theory consists of an axiomatic system and all its derived theorems...
s. It has sufficient expressive power to formalize two important mathematical theories:
Zermelo–Fraenkel (ZFC)Zermelo–Fraenkel set theory with the axiom of choice, commonly abbreviated ZFC, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics...
set theory and (first-order) Peano arithmetic. However, no axiom system in first order logic is strong enough to fully (categorically) describe infinite structures such as the
natural numberIn mathematics, there are two conventions for the set of natural numbers: it is either the set of positive integers {, , , ...} according to the traditional definition or the set of non-negative integers {, 1, 2, ...} according to...
s or the
real lineIn mathematics, the real line is the line whose points correspond to the real numbers. That is, the real line is the set R of all real numbers, viewed as a geometric space...
. Categorical axiom systems for these structures can be obtained in stronger logics such as
second-order logicIn 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....
.
A history of first-order logic and an account of its emergence over other formal logics is provided by Ferreirós (2001).
Introduction
While propositional logic deals with simple declarative propositions, first-order logic additionally covers
predicateSometimes it is inconvenient or impossible to describe a set by listing all of its elements. Another useful way to define a set is by specifying a property that the elements of the set have in common. The notation P is used to denote a sentence or statement P concerning the variable object x...
s and
quantificationQuantification has two distinct sense. In mathematics and empirical science, it is the act of counting and measuring that maps human sense observations and experiences into members of some set of numbers. Quantification in this sense is fundamental to the scientific method.In logic, quantification...
.
A predicate resembles a function that returns either True or False. Consider the following sentences: "Socrates is a philosopher", "Plato is a philosopher". In propositional logic these are treated as two unrelated propositions, denoted for example by
p and
q. In first-order logic, however, the sentences can be expressed in a more parallel manner using the predicate Phil(
a), which asserts that the object represented by
a is a philosopher. Thus if
a represents Socrates then Phil(
a) asserts the first proposition,
p; if
a represents Plato then Phil(
a) asserts the second proposition,
q. A key aspect of first-order logic is visible here: the string "Phil" is a syntactic entity which is given semantic meaning by declaring that Phil(
a) holds exactly when
a is a philosopher. An assignment of semantic meaning is called an interpretation.
First-order logic allows reasoning about properties that are shared by many objects, through the use of variables. For example, let Phil(
a) assert that
a is a philosopher and let Schol(
a) assert that
a is a scholar. Then the formula
asserts that if
a is a philosopher then
a is a scholar. The symbol is used to denote a
conditionalThe material conditional, also known as the material implication or truth functional conditional, expresses a property of certain conditionals in logic. In propositional logic, it expresses a binary truth function from truth-values to truth-values. In predicate logic, it can be viewed as a subset...
(if/then) statement. The hypothesis lies to the left of the arrow and the conclusion to the right. The truth of this formula depends on which object is denoted by
a, and on the interpretations of "Phil" and "Schol".
Assertions of the form "for every
a, if
a is a philosopher then
a is a scholar" require both the use of variables and the use of a quantifier. Again, let Phil(
a) assert
a is a philosopher and let Schol(
a) assert that
a is a scholar. Then the first-order sentence
asserts that no matter what
a represents, if
a is a philosopher then
a is scholar. Here , the universal quantifier, expresses the idea that the claim in parentheses holds for
all choices of
a.
To show that the claim "If
a is a philosopher then
a is a scholar" is false, one would show there is some philosopher who is not a scholar. This counterclaim can be expressed with the existential quantifier :
Here:
- is the negation operator: is true if and only if is false, in other words if and only if a is not a scholar.
- is the conjunction operator: asserts that a is a philosopher and also not a scholar.
The predicates Phil(
a) and Schol(
a) take only one parameter each. First-order logic can also express predicates with more than one parameter. For example, "there is someone who can be fooled every time" can be expressed as:
Here Person(
x) is interpreted to mean
x is a person, Time(
y) to mean that
y is a moment of time, and Canfool(
x,
y) to mean that (person)
x can be fooled at (time)
y.
The
range of the quantifiers is the set of objects that can be used to satisfy them. (In the informal examples in this section, the range of the quantifiers was left unspecified.) In addition to specifying the meaning of predicate symbols such as Person and Time, an interpretation must specify a nonempty set, known as the
domain of discourseThe domain of discourse, sometimes called the universe of discourse, logical discourse, or simply discourse, is an analytic tool used in deductive logic, especially predicate logic...
or universe, as a range for the quantifiers. Thus a statement of the form is said to be true, under a particular interpretation, if there is some object in the domain of discourse of that interpretation that satisfies the predicate that the interpretation uses to assign meaning to the symbol Phil.
Syntax
There are two key parts of first order logic. The
syntaxIn linguistics, syntax is the study of the principles and rules for constructing sentences in natural languages...
determines which collections of symbols are legal expressions in first-order logic, while the
semanticsSemantics is the study of meaning, usually in language. The word "semantics" itself denotes a range of ideas, from the popular to the highly technical. It is often used in ordinary language to denote a problem of understanding that comes down to word selection or connotation. This problem of...
determine the meanings behind these expressions.
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 legal. There are two key types of legal expressions:
terms, which intuitively represent objects, and
formulas, which intuitively express predicates that can be true or false. The terms and formulas of first-order logic are strings of
symbols which together form the
alphabet of the language. As with all
formal languageA formal language is a set of words, i.e. finite strings of letters, symbols, or tokens. The set from which these letters are taken is called the alphabet over which the language is defined...
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 always represents "and"; it is never interpreted as "or". On the other hand, a non-logical predicate symbol such as Phil(
x) could be interpreted to mean "
x is a philosopher", "
x is a cat", or any other unary predicate, depending on the interpretation at hand.
Logical symbols
There are several logical symbols in the alphabet, which vary by author but usually include:
- The quantifier symbols and
- The logical connective
In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependant on the respective truth values of the original sentences.Each logical connective can be expressed as a...
s: for conjunction, for disjunction, for implication, for biconditional, for negation. Occasionally other logical connective symbols are included. Some authors use and instead of and , especially in contexts where is used for other purposes. Moreover, , tilde (~) and & may replace , and , especially if these symbols are not available for technical reasons.
- 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: x0, x1, x2, … .
- An equality symbol (sometimes, identity symbol) =; see the section on equality below.
Though it should be noted that not all of these symbols are required - only one of the quantifiers, negation and conjunction, variables, brackets and equality suffice. There are numerous minor variations that may define additional logical symbols:
- Sometimes the truth constants T or for "true" and F or for "false" are included. Without any such logical operators of valence 0, these two constants can only be expressed using quantifiers.
- Sometimes additional logical connectives, such as the Sheffer stroke
In Boolean functions and propositional calculus, the Sheffer stroke, named after Henry M. Sheffer, written "|" or "↑", denotes a logical operation that is equivalent to the negation of the conjunction operation, expressed in ordinary language as "not both"...
(NAND) and exclusive or operators are included.
Non-logical symbols
The non-logical symbols represent predicates (relations), functions and constants on the domain of discourse. It used to be standard practice to use a fixed, infinite set of non-logical symbols for all purposes. 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.
The traditional approach is to have only one, infinite, set of non-logical symbols (one signature) for all applications. Consequently, under the traditional approach there is only one language of first-order logic. This approach is still common, especially in philosophically oriented books.
- For every integer n ≥ 0 there is a collection of n-ary
In logic, mathematics, and computer science, the arity of a function or operation is the number of arguments or operands that the function takes. The arity of a relation is the number of domains in the corresponding Cartesian product. The term springs from such words as unary, binary, ternary,...
, or n-place, predicate symbols. Because they represent relationsIn mathematics , a relation is a property that assigns truth values to combinations of k individuals. Typically, the property describes a possible connection between the components of a k-tuple...
between n elements, they are also called relation symbols. For each arity n we have an infinite supply of them:
- Pn0, Pn1, Pn2, Pn3, …
- For every integer n ≥ 0 there are infinitely many n-ary function symbols:
- f n0, f n1, f n2, f n3, …
In contemporary mathematical logic, the signature varies by application. Typical signatures in mathematics are {1, ×} or just {×} for
groupIn mathematics, a group is an algebraic structure consisting of a set together with an operation that combines any two of its elements to form a third element. To qualify as a group, the set and the operation must satisfy a few conditions called group axioms, namely closure, associativity, identity...
s, or {0, 1, +, ×, <} for
ordered fieldIn mathematics, an ordered field is a field together with a total ordering of its elements that agrees in a certain sense with the field operations...
s. There are no restrictions on the number of non-logical symbols. The signature can be
emptyIn mathematics, and more specifically set theory, the empty set is the unique set having no members; its size is zero. Some axiomatic set theories assure that the empty set exists by including an axiom of empty set; in other theories, its existence can be deduced...
, finite, or infinite, even uncountable. Uncountable signatures occur for example in modern proofs of the Löwenheim-Skolem theorem.
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
In logic, mathematics, and computer science, the arity of a function or operation is the number of arguments or operands that the function takes. The arity of a relation is the number of domains in the corresponding Cartesian product. The term springs from such words as unary, binary, ternary,...
, number of arguments) greater than or equal to 0. These which are often denoted by uppercase letters P, Q, R,... .
- Relations of valence 0 can be identified with propositional variable
In mathematical logic, a propositional variable is a variable which can either be true or false...
s. For example, P, which can stand for any statement.
- For example, P(x) is a predicate variable of valence 1. One possible interpretation is "x is a man".
- Q(x,y) is a predicate variable of valence 2. Possible interpretations include "x is greater than y" and "x is the father of y".
- A function symbol, with some valence greater than or equal to 0. These are often denoted by lowercase letters f, g, h,... .
- Examples: f(x) may be interpreted as for "the father of x". In arithmetic
Arithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple day-to-day counting to advanced science and business calculations, such as addition, subtraction, multiplication and division...
, it may stand for "-x". In set theoryThe modern study of set theory was initiated by Cantor and Dedekind in the 1870s. After the discovery of paradoxes in informal set theory, numerous axiom systems were proposed in the early twentieth century, of which the Zermelo–Fraenkel axioms, with the axiom of choice, are the best-known.The...
, it may stand for "the power setIn mathematics, given a set S, the power set of S, written , P, ℘ or 2
S, is the set of all subsets of S. In axiomatic set theory In mathematics, given a set S, the power set (or powerset) of S, written , P(S), ℘(S) or 2
S, is the set of all subsets of S. In...
of x". In arithmeticArithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple day-to-day counting to advanced science and business calculations, such as addition, subtraction, multiplication and division...
, g(x,y) may stand for "x+y". In set theoryThe modern study of set theory was initiated by Cantor and Dedekind in the 1870s. After the discovery of paradoxes in informal set theory, numerous axiom systems were proposed in the early twentieth century, of which the Zermelo–Fraenkel axioms, with the axiom of choice, are the best-known.The...
, 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 a, b, c,... . The symbol a may stand for Socrates. In arithmetic
Arithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple day-to-day counting to advanced science and business calculations, such as addition, subtraction, multiplication and division...
, it may stand for 0. In set theoryThe modern study of set theory was initiated by Cantor and Dedekind in the 1870s. After the discovery of paradoxes in informal set theory, numerous axiom systems were proposed in the early twentieth century, of which the Zermelo–Fraenkel axioms, with the axiom of choice, are the best-known.The...
, such a constant may stand for the empty setIn mathematics, and more specifically set theory, the empty set is the unique set having no members; its size is zero. Some axiomatic set theories assure that the empty set exists by including an axiom of empty set; in other theories, its existence can be deduced...
.
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 ruleIn 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 strings of the language. It does not describe anything...
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 grammarA formal grammar is a set of rules for forming strings in a formal language. These rules that make up the grammar describe how to form strings from the language's alphabet that are valid according to the language's syntax...
for terms and formulas. These rules are generally
context-freeIn formal language theory, a context-free grammar is a grammar in which every production rule is of the formwhere V is a single nonterminal symbol, and w is a string of terminals and/or nonterminals ....
(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
termsThe word term is from the Latin terminus which literally means "boundary line, limit", from the Proto-Indo-European root "peg, post, boundary"....
is inductively defined by the following rules:
- Variables. Any variable is a term.
- Functions. Any expression f(t1,...,tn) of n arguments (where each argument ti is a term and f is a function symbol of valence n) is a term.
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 formulaIn the formal languages used in mathematical logic and computer science, a well-formed formula or simply formula is an idea, abstraction or concept which is expressed using the symbols and formation rules of a particular formal language...
s or
wffs) is inductively defined by the following rules:
- Predicate symbols. If P is an n-ary predicate symbol and t1, ..., tn are terms then P(t1,...,tn) is a formula.
- Equality. If the equality symbol is considered part of logic, and t1 and t2 are terms, then t1 = t2 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 and 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 formulaIn mathematical logic, an atomic 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 subformulas. Atoms are thus the simplest well-formed formulas of the logic...
s.
For example,
is a formula, if
f is a unary function symbol,
P a unary predicate symbol, and Q a ternary predicate symbol. On the other hand, 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 (in other words, there is a unique
parse treeA concrete syntax tree or parse tree is an tree that represents the syntactic structure of a string according to some formal grammar. In a parse tree, the interior nodes are labeled by non-terminals of the grammar, while the leaf nodes are labeled by terminals of the grammar. A program that...
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.
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 operationsIn mathematics and computer programming, an expression or string of symbols is intended to represent a numerical value; a properly-formed expression may be evaluated in an unambiguous way. But in practice, an expression with multiple terms and operators may be written with parentheses, in...
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.
The definitions above use infix notation for binary connectives such as . A less common convention is
Polish notationPolish notation, also known as prefix notation, is a form of notation for logic, arithmetic, and algebra. Its distinguishing feature is that it places operators to the left of their operands. If the arity of the operators is fixed, the result is a syntax lacking parentheses or other brackets, that...
, in which one writes , , and so on in front of their arguments rather than between them. This convention allows all punctuation symbols to be discarded. Polish notation is compact and elegant, but rarely used in practice because it is hard for humans to read it. In Polish notation, the formula
becomes
Example
In mathematics the language of ordered abelian groups has one constant symbol 0, one unary function symbol −, one binary function symbol +, and one binary relation symbol ≤. 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 is a formula, which is usually written as
Free and bound variables
In a formula, a variable may occur
free or
bound. Intuitively, a variable is free in a formula if it is not quantified: in , variable
x is free while
y is bound. The free and bound variables of a formula are defined inductively as follows.
- Atomic formulas. If φ is an atomic formula then x is free in φ if and only if x occurs in φ, and x is never bound in φ.
- Negation. x is free in φ if and only if x is free in φ. x is bound in φ if and only if x is bound in φ.
- Binary connectives. x is free in (φ ψ) if and only if x is free in either φ or ψ. x is bound in (φ ψ) if and only if x is bound in either φ or ψ. The same rule applies to any other binary connective in place of .
- Quantifiers. x is free in y φ if and only if x is free in φ and x is a different symbol than y. Also, x is bound in y φ if and only if x is y or x is bound in φ. The same rule holds with in place of .
For example, in
x y (
P(
x)
Q(
x,
f(
x),
z)),
x and
y are bound variables,
z is a free variable, and
w is neither because it does not occur in the formula.
Freeness and boundness can be also specialized to specific occurrences of variables in a formula. For example, in , the first occurrence of
x is free while the second is bound. In other words, the
x in is free while the in is bound.
A formula with no free variables is called a
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.
Semantics
An
interpretationAn interpretation is an assignment of "meaning" to the symbols of a language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any "meaning" until they are given some interpretation...
of a first-order language assigns a denotation to all non-logical constants in that language. It also determines a
domain of discourseThe domain of discourse, sometimes called the universe of discourse, logical discourse, or simply discourse, is an analytic tool used in deductive logic, especially predicate logic...
that specifies the range of the quantifiers. The result is that each term is assigned an object that it represents, and each sentence is assigned a truth value. In this way, an interpretation provides semantic meaning to the terms and formulas of the language. The study of the interpretations of formal languages is called formal semantics.
The domain of discourse
D is a nonempty set of "objects" of some kind. Intuitively, a first-order formula is a statement about these objects; for example, states the existence of an object
x such that the predicate
P is true where referred to it. The domain of discourse is the set of considered objects. For example, one can take to be the set of integer numbers.
The interpretation of a function symbol is a function. For example, if the domain of discourse consists of integers, a function symbol
f of arity 2 can be interpreted as the function that gives the sum of its arguments. In other words, the symbol
f is associated with the function
I(f) which, in this interpretation, is addition.
The interpretation of a constant symbol is a function from the one-element set
D0 to
D, which can be simply identified with an object in
D. For example, an interpretation may assign the value to the constant symbol .
The interpretation of an
n-ary predicate symbol is a set of
n-tuples of elements of the domain of discourse. This means that, given an interpretation, a predicate symbol, and
n elements of the domain of discourse, one can tell whether the predicate is true of those elements according to the given interpretation. 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 the second.
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 nonempty set
D that forms the domain of discourse and an interpretation
I of the non-logical terms of the signature. This interpretation is itself a function:
- Each function symbol f of arity n is assigned a function I(f) from to . In particular, each constant symbol of the signature is assigned an individual in the domain of discourse.
- Each predicate symbol P of arity n is assigned a relation I(P) over or, equivalently, a function from to . Thus each predicate symbol is interpreted by a Boolean-valued function
A boolean-valued function, in some usages is a predicate or a proposition, is a function of the type f : X → B, where X is an arbitrary set and where B is a boolean domain....
on D.
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 . 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 that have been evaluated to elements of the domain of discourse, and a n-ary function symbol f, the term evaluates to .
Next, each formula is assigned a truth value. The inductive definition used to make this assignment is called the
T-schemaThe T-schema or truth schema is the inductive definition that lies at the heart of any realisation of Alfred Tarski's semantic theory of truth, expressing the commutation of truth over logical operators....
.
- Atomic formulas (1). A formula is associated the value true or false depending on whether , where are the evaluation of the terms and is the interpretation of , which by assumption is a subset of .
- Atomic formulas (2). A formula is assigned true if and evaluate to the same object of the domain of discourse (see the section on equality below).
- Logical connectives. A formula in the form , , 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—to compute the functional values of logical expressions on each of their functional arguments, that is, on each combination of values taken by their...
for the connective in question, as in propositional logic.
- Existential quantifiers. A formula is true according to M and if there exists an evaluation of the variables that only differs from regarding the evaluation of x and such that φ is true according to the interpretation M and the variable assignment . This formal definition captures the idea that 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 is true according to M and if φ(x) is true for every pair composed by the interpretation M and some variable assignment that differs from only on the value of x. This captures the idea that 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 if and only if is true according to
M and any other variable assignment .
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
cd 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 is true according to M if there is some d in the domain of discourse such that holds. Here is the result of substituting cd for every free occurrence of x in φ.
- Universal quantifiers (alternate). A formula is true according to M if, for every d in the domain of discourse, 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 . A sentence is
satisfiable if there is some interpretation under which it is true.
Satisfiability of formulas with free variables is more complicated, because an interpretation on its own does not determine the truth value of such a formula. The most common convention is that a formula with free variables is said to be satisfied by an interpretation if the formula remains true regardless which individuals from the domain of discourse are assigned to its free variables. This has the same effect as saying that a formula is satisfied if and only if its universal closure is satisfied.
A formula is
logically valid (or simply
valid) if it is true in every interpretation. These formulas play a role similar to
tautologiesIn propositional logic, a tautology is a propositional formula that is true under any possible valuation of its propositional variables. For example, the propositional formula is a tautology, because the statement is true for any valuation of A...
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 algebraAbstract algebra is the subject area of mathematics that studies algebraic structures, such as groups, rings, fields, modules, vector spaces, and algebras...
. This approach generalizes the
Lindenbaum–Tarski algebraIn mathematical logic, the Lindenbaum–Tarski algebra of a logical theory T consists of the equivalence classes of sentences of the theory, under the equivalence relation ~ defined such that p ~ q exactly when p and q are provably equivalent in T...
s 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
The notion of cylindric algebra, invented by Alfred Tarski, arises naturally in the algebraization of first-order logic. This is comparable to the role Boolean algebras play for propositional logic...
, by Alfred TarskiAlfred Tarski was a Polish logician and mathematician...
and his coworkers;
- Polyadic algebra
Polyadic algebras are an algebraic structure introduced by Paul Halmos. They are related to propositional calculus in a way analogous to the relationship between Boolean algebras and Boolean logic....
, by Paul HalmosPaul Richard Halmos was a Hungarian-born Jewish American mathematician who made fundamental advances in the areas of probability theory, statistics, operator theory, ergodic theory, functional analysis , and mathematical logic...
;
- Predicate functor logic
In mathematical logic, predicate functor logic is one of several ways to express first-order logic by purely algebraic means, i.e., without quantified variables. PFL employs a small number of algebraic devices called predicate functors that operate on terms to yield terms...
, mainly due to Willard QuineWillard Van Orman Quine was an American philosopher and logician in the analytic tradition...
.
These
algebraAlgebra is the branch of mathematics concerning the study of the rules of operations and the things which can be constructed from them, including terms, polynomials, equations and algebraic structures...
s are all
latticesIn mathematics, a lattice is a partially ordered set in which any two elements have a unique supremum and an infimum . Lattices can also be characterized as algebraic structures satisfying certain axiomatic identities...
that properly extend the
two-element Boolean algebraIn mathematics and abstract algebra, the two-element Boolean algebra is the Boolean algebra whose underlying set B is the Boolean domain. The elements of the Boolean domain are 1 and 0 by convention, so that B={0,1}...
.
Tarski and Givant (1987) showed that the fragment of first-order logic that has no
atomic sentence Molecular sentence which is a sentence composed of atomic sentences also redirects here.In Logic, sentences are those strings of words or symbols which are either true or false. In philosophy, such sentences are sometimes called truthbearers...
lying in the scope of more than three quantifiers, has the same expressive power as
relation algebraIn mathematics and abstract algebra, a relation algebra is a residuated Boolean algebra equipped with an involution called "converse". The motivating example of a relation algebra is the algebra 2X² of all binary relations on a set X, with R•S interpreted as the usual composition of...
. This fragment is of great interest because it suffices for Peano arithmetic and most axiomatic set theory, including the canonical
ZFCZermelo–Fraenkel set theory with the axiom of choice, commonly abbreviated ZFC, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics...
. They also prove that first-order logic with a primitive
ordered pairIn mathematics, an ordered pair is a collection of objects having two coordinates , such that one can always uniquely determine the object, which is the first coordinate of the pair as well as the second coordinate...
is equivalent to a relation algebra with two ordered pair projection functions.
First-order theories, models, and elementary classes
A
first-order theory consists of a set of
axiomIn traditional logic, an axiom or postulate is a proposition that is not proved or demonstrated but considered to be either self-evident, or subject to necessary decision...
s in a particular first-order signature. The set of axioms is often finite or recursively enumerable, in which case the theory is called
effective. Some authors require theories to also include all logical consequences of the axioms.
A first-order structure that satisfies all sentences in a given theory is said to be a
model of the theory. An
elementary classIn the branch of mathematical logic called model theory, an elementary class is a class consisting of all structures satisfying a fixed first-order theory.- Definition :...
is the set of all structures satisfying a particular theory. These classes are a main subject of study in
model theoryIn mathematics, model theory is the study of mathematical structures such as groups, fields, graphs, or even universes of set theory, using tools from mathematical logic. A structure that gives meaning to the sentences of a formal language is called a model for the language...
.
Many theories have an
intended interpretationOne who constructs a syntactical system usually has in mind from the outset some interpretation of this system. While this intended interpretation can have no explicit indication in the syntactical rules - since these rules must be strictly formal - the author's intention respecting interpretation...
, a certain model that is kept in mind when studying the theory. For example, the intended interpretation of Peano arithmetic consists of the usual
natural numberIn mathematics, there are two conventions for the set of natural numbers: it is either the set of positive integers {, , , ...} according to the traditional definition or the set of non-negative integers {, 1, 2, ...} according to...
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
consistentConsistency can refer to:* Consistency * Consistency , the psychological need to be consistent with prior acts and statements* "Consistency", an 1887 speech by Mark Twain...
if it is not possible to prove a contradiction from the axioms of the theory. A theory is
completeIn mathematical logic, a theory is complete if it is a maximal consistent set of sentences, i.e., if it is consistent, and none of its proper extensions is consistent...
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 a nonempty set. There are settings, such as
free logicFree logic is a logic with no existential presuppositions. Alternatively, it is a logic whose theorems are valid in all domains, including the empty domain.- Explanation :...
, where empty domains are permitted. Moreover, if a class of algebraic structures includes an empty structure (for example, there is an empty poset), that class can only be an elementary class in first-order logic if empty domains are permitted or the empty structure is removed from the class.
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 implies when x is not a free variable in φ. This rule, which is used to put formulas into prenex normal form
A formula of the predicate calculus is in prenex normal form if it is written as a string of quantifiers followed by a quantifier-free part .Every formula is equivalent in classical logic to a formula in prenex normal form...
, 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 systems,
natural deductionIn logic, natural deduction is an approach to proof theory that attempts to provide a deductive system which is a formal model of logical reasoning as it "naturally" occurs. This approach is in contrast to axiomatic systems which use axioms....
, the
sequent calculusIn proof theory and mathematical logic, sequent calculus is a widely known family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934, as a tool for studying natural...
, the
tableaux methodIn proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulas of first-order logic. The tableau method can also determine the satisfiability of finite sets of formulas of various logics...
, and
resolutionIn mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic...
. 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 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 whether that interpretation is about mathematics, economics, or some other area.
In general, logical consequence in first-order logic is only semidecidable: if a sentence A logically implies a sentence B then this can be discovered (for example, by searching for a proof until one is found, using some effective, sound, complete proof system). 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 inferenceIn logic, a rule of inference is a syntactic rule used in a formal system which is used to produce valid statements within that system. A formal system is composed of a formal language and a deductive system...
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] (often denoted φ[
x/
t]) 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 , in the signature of (0,1,+, ×,=) of arithmetic. If
t is the term "x + 1", the formula φ[
t/
y] is , 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 , 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 schemes 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 schemes of logical axioms. It is common to have only
modus ponensIn classical logic, modus ponendo ponens is a valid, simple argument form sometimes referred to as affirming the antecedent or the law of detachment...
and
universal generalizationIn mathematical logic, generalization is an inference rule of predicate calculus. It states that if has been derived, then can be derived.- Generalization with hypotheses :...
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
where A
1, ..., A
n, B
1, ..., B
k are formulas and the turnstile symbol is used as punctuation to separate the two halves. Intuitively, a sequent expresses the idea that implies .
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 at its root; the tree branches in a way that reflects the structure of the formula. For example, to show that is unsatisfiable requires showing that C and D are each unsatisfiable; the corresponds to a branching point in the tree with parent and children C and D.
Resolution
The
resolution ruleIn mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic...
is a single rule of inference that, together with
unificationIn mathematical logic, in particular as applied to computer science, a unification of two terms is a join with respect to a specialisation order. That is, we suppose a preorder on a set of terms, for which t* ≤ t means that t* is obtained from t by substituting some term for one or more free...
, 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. The resolution rule states that from the hypotheses and , the conclusion can be obtained.
Provable identities
The following sentences can be called "identities" because the main connective in each is the
biconditionalIn logic and mathematics, the logical biconditional is a logical operator connecting two statements to assert "p if and only if q", where p is a hypothesis and q is a conclusion...
. (where must not occur free in ) (where must not occur free in )
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. 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 schemes, each of which specifies an infinite set of axioms. The third scheme is known as
Leibniz's law, "the principle of substitutivity", "the indiscernibility of identicals", or "the replacement property". The second scheme, involving the function symbol
f, is (equivalent to) a special case of the third scheme, 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 relationIn mathematics, an equivalence relation is, loosely, a binary relation on a set that specifies how to split up the set into subsets such that every element of the larger set is in exactly one of the subsets...
on the domain of discourse that is
congruentIn abstract algebra, a congruence relation is an equivalence relation on an algebraic structure that is compatible with the structure...
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 theoremIn mathematical logic, the Löwenheim–Skolem theorem states that if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ...
so that only normal models are considered.
First-order logic without equality is often employed in the context of
second-order arithmeticIn 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. It was introduced by...
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 schemes 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 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 orders 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 x (s x t x) x (x s x t). 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.- Formal statement :...
, , by , i.e. if x and y have the same elements, then they belong to the same sets.
Metalogical properties
One motivation for the use of first-order logic, rather than
higher-order logicIn mathematics and logic, a higher-order logic is distinguished from first-order logic in a number of ways. One of these is the type of variables appearing in quantifications; in first-order logic, roughly speaking, it is forbidden to quantify over predicates. See second-order logic for systems in...
, is that first-order logic has many
metalogicMetalogic is the study of the metatheory of logic. While logic is the study of the manner in which logical systems can be used to decide the correctness of arguments, metalogic studies the properties of the logical systems themselves...
al properties that stronger logics do not. 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 theoremGö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. It was first proved by Kurt Gödel in 1929....
, proved by
Kurt GödelKurt Gödel was an Austrian-American logician, mathematician and philosopher. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the 20th century, a time when many, such as Bertrand Russell, A. N...
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: it is possible to make an effective enumeration of all pairs of sentences (φ,ψ) such that ψ is a logical consequence of φ.
Unlike propositional logic, first-order logic is
undecidableIn logic, the term decidable refers to the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively determined...
(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 that determines whether arbitrary formulas are logically valid. This result was established independently by
Alonzo ChurchAlonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.- Life :Alonzo...
and
Alan TuringAlan Mathison Turing, OBE, FRS , was an English mathematician, logician, cryptanalyst, and computer scientist. He was influential in the development of computer science and provided an influential formalisation of the concept of the algorithm and computation with the Turing machine...
in 1936 and 1937, respectively, giving a negative answer to the
EntscheidungsproblemIn mathematics, the is a challenge posed by David Hilbert in 1928. The asks for an algorithm that will take as input a description of a formal language and a mathematical statement in the language and produce as output either "True" or "False" according to whether the statement is true or false...
posed by
David HilbertDavid Hilbert was a German mathematician, recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. He discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of geometry...
in 1928. Their proofs demonstrate a connection between the unsolvability of the decision problem for first-order logic and the unsolvability of the
halting problemIn computability theory, the halting problem is a decision problem which can be stated as follows: given a description of a program, decide whether the program finishes running or will run forever...
.
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. The
Bernays–Schönfinkel classThe Bernays–Schönfinkel class of formulas, named after Paul Bernays and Moses Schönfinkel The Bernays–Schönfinkel class (also known as Bernays–Schönfinkel-Ramsey class) of formulas, named after Paul Bernays and Moses Schönfinkel The Bernays–Schönfinkel class (also known as...
of first-order formulas is also decidable.
The Löwenheim–Skolem theorem
The
Löwenheim–Skolem theoremIn mathematical logic, the Löwenheim–Skolem theorem states that if a countable first-order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ...
shows that if a first-order theory of
cardinalityIn mathematics, the cardinality of a set is a measure of the "number of elements of the set". For example, the set A = {2, 4, 6} contains 3 elements, and therefore A has a cardinality of 3...
λ has any infinite model then it has models of every infinite
cardinalityIn mathematics, the cardinality of a set is a measure of the "number of elements of the set". For example, the set A = {2, 4, 6} contains 3 elements, and therefore A has a cardinality of 3...
greater than or equal to λ. One of the earliest results in model theory, it implies that it is not possible to characterize
countabilityIn mathematics, a countable set is a set with the same cardinality as some subset of the set of natural numbers. A set that is not countable is called uncountable...
or uncountability in a first-order language. 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, this means 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 paradoxIn mathematical logic and philosophy, Skolem's paradox is a seeming contradiction that arises from the downward Löwenheim-Skolem theorem. Thoralf Skolem was the first to discuss the seemingly contradictory aspects of the theorem, and to discover the relativity of set-theoretic notions now known as...
.
The compactness theorem
The
compactness theoremIn 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...
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
graphsIn mathematics, a graph is an abstract representation of a set of objects where some pairs of the objects are connected by links. The interconnected objects are represented by mathematical abstractions called vertices, and the links that connect some pairs of vertices are called edges...
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 graphA directed graph or digraph is a pair G= of:* a set V, whose elements are called vertices or nodes,* a set A of ordered pairs of vertices, called arcs, directed edges, or arrows .It differs from an ordinary or undirected graph, in that the latter is defined in terms of unordered pairs of...
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 componentsIn graph theory, a connected component of an undirected graph is a subgraph in which any two vertices are connected to each other by paths, and to which no more vertices or edges can be added while preserving its connectivity. That is, it is a maximal connected subgraph. For example, the graph...
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 signature of graphs, that expresses the idea that there is a path from
x to
y. Connectedness can be expressed in second-order logic, however.
Lindström's theorem
Per Lindström showed that the metalogical properties just discussed actually characterize first-order logic in the sense that no stronger logic has the properties. Lindström defined a class of abstract logical systems, so that it makes sense to say that one system is stronger than another. 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.
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 can be expressed as , and can be expressed as , either of the two quantifiers and can be dropped.
- Since can be expressed as and can be expressed as , either or can be dropped. In other words, it is sufficient to have and , or and , as the only logical connectives.
- Similarly, it is sufficient to have only and as logical connectives, or to have only the Sheffer stroke
In Boolean functions and propositional calculus, the Sheffer stroke, named after Henry M. Sheffer, written "|" or "↑", denotes a logical operation that is equivalent to the negation of the conjunction operation, expressed in ordinary language as "not both"...
(NAND) or the NOR operator.
- It is possible to entirely avoid function symbols and constant symbols, rewriting them via predicate symbols in a appropriate way. For example, instead of using a constant symbol one may use a predicate (interpreted as ), and replace every predicate such as with . A function such as will similarly be replaced by a predicate interpreted as . This change requires adding additional axioms to the theory at hand, so that interpretations of the 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 schemes 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 functionIn 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 numbers...
. This is a function of arity 2 that takes pairs of elements of the domain and returns an
ordered pairIn mathematics, an ordered pair is a collection of objects having two coordinates , such that one can always uniquely determine the object, which is the first coordinate of the pair as well as the second coordinate...
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 typeA data type in programming languages is a set of values and the operations on those values.-Overview:Almost all programming languages explicitly include the notion of data type, though different languages may use different terminology...
), but it is not the same as first-order
type theoryIn mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
. Many-sorted first-order logic is often used in the study of
second-order arithmeticIn 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. It was introduced by...
.
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 and and the axiom.
Then the elements satisfying are thought of as elements of the first sort, and elements satisfying as elements of the second sort. One can quantify over each sort by using the corresponding predicate symbol to limit the range of quantification. For example, to say there is an element of the first sort satisfying formula φ(
x), one writes.
Additional quantifiers
Additional quantifiers can be added to first-order logic.
- Sometimes it is useful to say that "P(x) holds for exactly one x", which can be expressed as x P(x). This notation, called uniqueness quantification
In mathematics and logic, the phrase "there is one and only one" is used to indicate that exactly one object with a certain property exists. In mathematical logic, this sort of quantification is known as uniqueness quantification or unique existential quantification.Uniqueness quantification is...
, may be taken to abbreviate a formula such as x (P(x) y (P(y) (x = y))).
- 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 is a partial orderingof quantifiers for Q∈{∀,∃}. In classical logic, quantifier prefixes are linearly ordered such that the value of a variable ym bound by a quantifier Qm depends on the value of the variablesbound by quantifierspreceding...
s and the plural quantifierIn mathematics and logic, plural quantification is the theory that an individual variable x may take on plural, as well as singular values. As well as substituting individual objects such as Alice, the number 1, the tallest building in London etc...
s of George BoolosGeorge Stephen Boolos was a philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology.- Life :...
and others.
- Bounded quantifier
In the study of formal theories in mathematical logic, bounded quantifiers are often added to a language in addition to the standard quantifiers "∀" and "∃". Bounded quantifiers differ from "∀" and "∃" in that bounded quantifiers restrict the range of the quantified variable...
s are often used in the study of set theory or arithmetic.
Infinitary logics
Infinitary logicAn infinitary logic is a logic that allows infinitely long statements and/or infinitely long proofs. Some infinitary logics may have different properties from those of standard first-order logic. In particular, infinitary logics may fail to be compact or complete. Notions of compactness and...
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 numberIn mathematics, cardinal numbers, or cardinals for short, are a generalization of the natural numbers used to measure the cardinality of sets. The cardinality of a finite set is a natural number – the number of elements in the set. The transfinite cardinal numbers describe the sizes of infinite...
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
countableIn mathematics, a countable set is a set with the same cardinality as some subset of the set of natural numbers. A set that is not countable is called uncountable...
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
Intuitionistic logic, or constructivist logic, is the symbolic logic system originally developed by Arend Heyting to provide a formal basis for Brouwer's programme of intuitionism. The system preserves justification, rather than truth, across transformations yielding derived propositions...
uses intuitionistic rather than classical propositional calculus; for example, ¬¬φ need not be equivalent to φ. Similarly, first-order fuzzy logicsT-norm fuzzy logics are a family of non-classical logics, informally delimited by having a semantics which takes the real unit interval [0, 1] for the system of truth values and functions called t-norms for permissible interpretations of conjunction...
are first-order extensions of propositional fuzzy logics rather than classical logic.
- Infinitary logic
An infinitary logic is a logic that allows infinitely long statements and/or infinitely long proofs. Some infinitary logics may have different properties from those of standard first-order logic. In particular, infinitary logics may fail to be compact or complete. Notions of compactness and...
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 topologyTopology is a major area of mathematics concerned with spatial properties that are preserved under continuous deformations of objects, for example deformations that involve stretching, but no tearing or gluing...
and model theoryIn mathematics, model theory is the study of mathematical structures such as groups, fields, graphs, or even universes of set theory, using tools from mathematical logic. A structure that gives meaning to the sentences of a formal language is called a model for the language...
.
- First-order modal logic
A modal logic is any system of formal logic that attempts to deal with modalities. Modals qualify the truth of a judgment. For example, if it is true that "John is happy," we might qualify this statement by saying that "John is very happy," in which case the term "very" would be a modality...
has extra modal operators with meanings which can be characterised informally as, for example "it is necessary that φ" and "it is possible that φ".
Higher-order logics
The characteristic feature of first-order logic is that individuals can be quantified, but not predicates. Thus
is a legal first-order formula, but
is not.
Second-order logicIn 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....
extends first-order logic by adding the latter type of quantification. Other
higher-order logicIn mathematics and logic, a higher-order logic is distinguished from first-order logic in a number of ways. One of these is the type of variables appearing in quantifications; in first-order logic, roughly speaking, it is forbidden to quantify over predicates. See second-order logic for systems in...
s allow quantification over even higher
typesIn mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
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, known as
full semantics, is much stronger than the semantics for 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. The Löwenheim–Skolem theorem and compactness theorem become false when generalized to stronger logics.
Automated theorem proving and formal methods
Automated theorem provingAutomated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
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 spaceIn computer science, a search algorithm, broadly speaking, is an algorithm that takes a problem as input and returns a solution to the problem, usually after evaluating a number of possible solutions. Most of the algorithms studied by computer scientists that solve problems are kinds of search...
can be very large; an exhaustive search of every possible derivation is theoretically possible but
computationally infeasibleComputational Complexity may refer to:*Computational complexity theory*Computational Complexity...
for many systems of interest in mathematics. Thus complicated
heuristic functionA heuristic function, or simply a heuristic, is a function that ranks alternatives in various search algorithms at each branching step based on the available information in order to make a decision about which branch to follow during a search.-Shortest paths:For example, for shortest path...
s 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
MetamathMetamath is a computer-assisted proof checker. It has no specific logic embedded and can simply be regarded as a device to apply inference rules to formulas...
, insist on having a complete derivation as input. Others, such as Mizar and Isabelle, take a well-formatted proof sketch (which may still be very long and detailed) and fill in the missing pieces by doing simple proof searches or applying known decision procedures: the resulting derivation is then verified by a small, core "kernel". Many such systems are primarily intended for interactive use by human mathematicians: these are known as proof assistants. They may also use formal logics that are stronger than first-order logic, such as type theory. Because a full derivation of any nontrivial result in a first-order deductive system will be extremely long for a human to write, 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 methodsIn computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
in computer science. In this setting, theorem provers are used to verify the correctness of programs and of hardware such as processors with respect to a
formal specificationIn computer science, a formal specification is a mathematical description of software or hardware that may be used to develop an implementation. It describes what the system should do, not how the system should do it...
. 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.
See also
- Equiconsistency
In mathematics, specifically in mathematical logic, formal theories are studied as mathematical objects. Since some theories are powerful enough to model different mathematical objects, it is natural to wonder about their own consistency....
- 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 for the set which has no member...
- Interpretation (model theory)
In model theory, interpretation of a structure M in another structure N is a technical notion that approximates the idea of representing M inside N. For example every reduct or definitional expansion of a structure N has an interpretation in N.Many model-theoretic properties are preserved under...
- Herbrandization
The Herbrandization of a logical formula is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formulas in prenex form as part of his proof of the Löwenheim-Skolem theorem...
- Prenex normal form
A formula of the predicate calculus is in prenex normal form if it is written as a string of quantifiers followed by a quantifier-free part .Every formula is equivalent in classical logic to a formula in prenex normal form...
- Skolem normal form
Skolemization is a method for removing existential quantifiers from formal logic statements, often performed as the first step in an automated theorem prover. A formula of first-order logic is in Skolem normal form if it is in conjunctive prenex normal form with only universal first-order...
- Table of logic symbols
In logic, a set of symbols is commonly used to express logical representation. As logicians are familiar with these symbols, they are not explained each time they are used. So, for students of logic, the following table lists many common symbols together with their name, pronunciation and related...
- Type (model theory)
In model theory and related areas of mathematics, a type is a set of first-order formulas in a language with free variables which are true of a sequence of elements of an -structure . Loosely speaking, types describe possible elements of a mathematical structure...
External links
- Stanford Encyclopedia of Philosophy
The Stanford Encyclopedia of Philosophy is a freely-accessible online encyclopedia of philosophy maintained by Stanford University. Each entry is written and maintained by an expert in the field, including professors from over 65 academic institutions worldwide...
: "Classical Logic -- by Stewart Shapiro. Covers syntax, model theory, and metatheory for first-order logic in the natural deduction style.
- forall x: an introduction to formal logic, by P.D. Magnus, covers formal semantics and proof theory for first-order logic.
- Metamath: an ongoing online project to reconstruct mathematics as a huge first-order theory, using first-order logic and the axiomatic set theory ZFC
Zermelo–Fraenkel set theory with the axiom of choice, commonly abbreviated ZFC, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics...
. Principia MathematicaThe Principia Mathematica is a 3-volume work on the foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell and published in 1910, 1912 & 1913...
modernized.
- Podnieks, Karl. Introduction to mathematical logic.
- Cambridge Mathematics Tripos Notes (typeset by John Fremlin). These notes cover part of a past Cambridge Mathematics Tripos course taught to undergraduates 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.