In
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
and
mathematics
Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
, second-order logic is an extension of
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
, which itself is an extension of
propositional logic
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
. Second-order logic is in turn extended by
higher-order logic
mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
and
type theory
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundat ...
.
First-order logic
quantifies only variables that range over individuals (elements of the
domain of discourse); second-order logic, in addition, also quantifies over
relations. For example, the second-order
sentence says that for every
formula ''P'', and every individual ''x'', either ''Px'' is true or not(''Px'') is true (this is the
law of excluded middle
In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradi ...
). Second-order logic also includes quantification over
set
Set, The Set, SET or SETS may refer to:
Science, technology, and mathematics Mathematics
*Set (mathematics), a collection of elements
*Category of sets, the category whose objects and morphisms are sets and total functions, respectively
Electro ...
s,
function
Function or functionality may refer to:
Computing
* Function key, a type of key on computer keyboards
* Function model, a structured representation of processes in a system
* Function object or functor or functionoid, a concept of object-oriente ...
s, and other variables (see section
below). Both first-order and second-order logic use the idea of a
domain of discourse (often called simply the "domain" or the "universe"). The domain is a set over which individual elements may be quantified.
Examples
![Kindl-Treppe Aug2021d](https://upload.wikimedia.org/wikipedia/commons/c/c3/Kindl-Treppe_Aug2021d.jpg)
First-order logic can quantify over individuals, but not over properties. That is, we can take an atomic sentence like Cube(''b'') and obtain a quantified sentence by replacing the name with a variable and attaching a quantifier:
[Professor Marc Cohen lecture notes https://faculty.washington.edu/smcohen/120/SecondOrder.pdf]
:
However, we cannot do the same with the predicate. That is, the following expression
:
is not a sentence of first-order logic, but this is a legitimate sentence of second-order logic. Here, ''P'' is a
predicate variable In mathematical logic, a predicate variable is a predicate letter which functions as a "placeholder" for a relation (between terms), but which has not been specifically assigned any particular relation (or meaning). Common symbols for denoting predi ...
and is semantically a
set
Set, The Set, SET or SETS may refer to:
Science, technology, and mathematics Mathematics
*Set (mathematics), a collection of elements
*Category of sets, the category whose objects and morphisms are sets and total functions, respectively
Electro ...
of individuals.
As a result, second-order logic has greater expressive power than first-order logic. For example, there is no way in first-order logic to identify the set of all cubes and tetrahedrons. But the existence of this set can be asserted in second-order logic as
:
We can then assert properties of this set. For instance, the following says that the set of all cubes and tetrahedrons does not contain any dodecahedrons:
:
Second-order quantification is especially useful because it gives the ability to express
reachability
In graph theory, reachability refers to the ability to get from one Vertex (graph theory), vertex to another within a graph. A vertex s can reach a vertex t (and t is reachable from s) if there exists a sequence of Glossary of graph theory#Basics, ...
properties. For example, if Parent(''x'', ''y'') denotes that ''x'' is a parent of ''y'', then first-order logic can't express the property that ''x'' is an
ancestor
An ancestor, also known as a forefather, fore-elder or a forebear, is a parent or (recursively) the parent of an antecedent (i.e., a grandparent, great-grandparent, great-great-grandparent and so forth). ''Ancestor'' is "any person from whom ...
of ''y''. In second-order logic we can express this by saying that every set of people containing ''y'' and closed under the Parent relation contains ''x'':
:
It is notable that while we have variables for predicates in second-order-logic, we don't have variables for properties of predicates. We can't say, for example, that there is a property Shape(''P'') that is true for the predicates ''P'' Cube, Tet, and Dodec. This would require
third-order logic.
Syntax and fragments
The syntax of second-order logic tells which expressions are well formed
formulas
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
. In addition to the
syntax of first-order logic, second-order logic includes many new ''sorts'' (sometimes called ''types'') of variables. These are:
* A sort of variables that range over sets of individuals. If ''S'' is a variable of this sort and ''t'' is a first-order term then the expression ''t'' ∈ ''S'' (also written ''S''(''t''), or ''St'' to save parentheses) is an
atomic formula
In mathematical logic, an atomic formula (also known as an atom or a prime formula) is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformu ...
. Sets of individuals can also be viewed as
unary relation
In mathematics, a finitary relation over sets is a subset of the Cartesian product ; that is, it is a set of ''n''-tuples consisting of elements ''x'i'' in ''X'i''. Typically, the relation describes a possible connection between the elemen ...
s on the domain.
* For each natural number ''k'' there is a sort of variables that ranges over all ''k''-ary relations on the individuals. If ''R'' is such a ''k''-ary relation variable and ''t''
1,...,''t''
''k'' are first-order terms then the expression ''R''(''t''
1,...,''t''
''k'') is an atomic formula.
* For each natural number ''k'' there is a sort of variables that ranges over all functions taking ''k'' elements of the domain and returning a single element of the domain. If ''f'' is such a ''k''-ary function variable and ''t''
1,...,''t''
''k'' are first-order terms then the expression ''f''(''t''
1,...,''t''
''k'') is a first-order term.
Each of the variables just defined may be universally and/or existentially quantified over, to build up formulas. Thus there are many kinds of quantifiers, two for each sort of variables. A ''sentence'' in second-order logic, as in first-order logic, is a well-formed formula with no free variables (of any sort).
It's possible to forgo the introduction of function variables in the definition given above (and some authors do this) because an ''n''-ary function variable can be represented by a relation variable of arity ''n''+1 and an appropriate formula for the uniqueness of the "result" in the ''n''+1 argument of the relation. (Shapiro 2000, p. 63)
Monadic second-order logic In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's ...
(MSO) is a restriction of second-order logic in which only quantification over unary relations (i.e. sets) is allowed. Quantification over functions, owing to the equivalence to relations as described above, is thus also not allowed. The second-order logic without these restrictions is sometimes called ''full second-order logic'' to distinguish it from the monadic version. Monadic second-order logic is particularly used in the context of
Courcelle's theorem In the study of graph algorithms, Courcelle's theorem is the statement that every graph property definable in the monadic second-order logic of graphs can be decided in linear time on graphs of bounded treewidth. The result was first proved by Bru ...
, an algorithmic meta-theorem in
graph theory
In mathematics, graph theory is the study of ''graphs'', which are mathematical structures used to model pairwise relations between objects. A graph in this context is made up of '' vertices'' (also called ''nodes'' or ''points'') which are conne ...
. The MSO theory of the complete infinite binary tree (
S2S) is decidable. By contrast, full second order logic over any infinite set (or MSO logic over for example (
,+)) can interpret the true
second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
A precur ...
.
Just as in first-order logic, second-order logic may include
non-logical symbol
In logic, the formal languages used to create expressions consist of symbols, which can be broadly divided into constants and variables. The constants of a language can further be divided into logical symbols and non-logical symbols (sometimes al ...
s in a particular second-order language. These are restricted, however, in that all terms that they form must be either first-order terms (which can be substituted for a first-order variable) or second-order terms (which can be substituted for a second-order variable of an appropriate sort).
A formula in second-order logic is said to be of first-order (and sometimes denoted
or
) if its quantifiers (which may be universal or existential) range only over variables of first order, although it may have free variables of second order. A
(existential second-order) formula is one additionally having some existential quantifiers over second order variables, i.e.
, where
is a first-order formula. The fragment of second-order logic consisting only of existential second-order formulas is called existential second-order logic and abbreviated as ESO, as
, or even as ∃SO. The fragment of
formulas is defined dually, it is called universal second-order logic. More expressive fragments are defined for any ''k'' > 0 by mutual recursion:
has the form
, where
is a
formula, and similar,
has the form
, where
is a
formula. (See
analytical hierarchy
In mathematical logic and descriptive set theory, the analytical hierarchy is an extension of the arithmetical hierarchy. The analytical hierarchy of formulas includes formulas in the language of second-order arithmetic, which can have quantifiers ...
for the analogous construction of
second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
A precur ...
.)
Semantics
The semantics of second-order logic establish the meaning of each sentence. Unlike first-order logic, which has only one standard semantics, there are two different semantics that are commonly used for second-order logic: standard semantics and Henkin semantics. In each of these semantics, the interpretations of the first-order quantifiers and the logical connectives are the same as in first-order logic. Only the ranges of quantifiers over second-order variables differ in the two types of semantics
(Väänänen 2001).
In standard semantics, also called full semantics, the quantifiers range over ''all'' sets or functions of the appropriate sort. Thus once the domain of the first-order variables is established, the meaning of the remaining quantifiers is fixed. It is these semantics that give second-order logic its expressive power, and they will be assumed for the remainder of this article.
Leon Henkin
Leon Albert Henkin (April 19, 1921, Brooklyn, New York - November 1, 2006, Oakland, California) was an American logician, whose works played a strong role in the development of logic, particularly in the theory of types. He was an active scholar ...
(1950) defined an alternative kind of semantics for second-order and higher-order theories, in which the meaning of the higher-order domains is partly determined by an explicit axiomatisation, drawing on
type theory
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundat ...
, of the properties of the sets or functions ranged over. Henkin semantics is a kind of many-sorted first-order semantics, where there are a class of models of the axioms, instead of the semantics being fixed to just the standard model as in the standard semantics. A model in Henkin semantics will provide a set of sets or set of functions as the interpretation of higher-order domains, which may be a proper subset of all sets or functions of that sort. For his axiomatisation, Henkin proved that
Gödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic.
The completeness theorem applies to any first-order theory: ...
and
compactness theorem
In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model. This theorem is an important tool in model theory, as it provides a useful (but generally no ...
, which hold for first-order logic, carry over to second-order logic with Henkin semantics. Since also the
Skolem–Löwenheim theorems hold for Henkin semantics,
Lindström's theorem In mathematical logic, Lindström's theorem (named after Swedish logician Per Lindström, who published it in 1969) states that first-order logic is the '' strongest logic'' (satisfying certain conditions, e.g. closure under classical negation) h ...
imports that Henkin models are just ''disguised first-order models''.
For theories such as second-order arithmetic, the existence of non-standard interpretations of higher-order domains isn't just a deficiency of the particular axiomatisation derived from type theory that Henkin used, but a necessary consequence of
Gödel's incompleteness theorem: Henkin's axioms can't be supplemented further to ensure the standard interpretation is the only possible model. Henkin semantics are commonly used in the study of
second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
A precur ...
.
Jouko Väänänen
Jouko Antero Väänänen (born September 3, 1950 in Rovaniemi, Lapland) is a Finnish mathematical logician known for his contributions to set theory,J. VäänänenSecond order logic or set theory? Bulletin of Symbolic Logic, 18(1), 91-121, 2012 ...
(
2001) argued that the choice between Henkin models and full models for second-order logic is analogous to the choice between
ZFC and ''
V'' as a basis for set theory: "As with second-order logic, we cannot really choose whether we axiomatize mathematics using ''V'' or ZFC. The result is the same in both cases, as ZFC ''is'' the best attempt so far to use ''V'' as an axiomatization of mathematics."
Expressive power
Second-order logic is more expressive than first-order logic. For example, if the domain is the set of all
real number
In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every real ...
s, one can assert in first-order logic the existence of an additive inverse of each real number by writing ∀''x'' ∃''y'' (''x'' + ''y'' = 0) but one needs second-order logic to assert the
least-upper-bound property for sets of real numbers, which states that every bounded, nonempty set of real numbers has a
supremum
In mathematics, the infimum (abbreviated inf; plural infima) of a subset S of a partially ordered set P is a greatest element in P that is less than or equal to each element of S, if such an element exists. Consequently, the term ''greatest l ...
. If the domain is the set of all real numbers, the following second-order sentence (split over two lines) expresses the least upper bound property:
:
:
This formula is a direct formalization of "every , set A ." It can be shown that any
ordered field
In mathematics, an ordered field is a field together with a total ordering of its elements that is compatible with the field operations. The basic example of an ordered field is the field of real numbers, and every Dedekind-complete ordered fiel ...
that satisfies this property is isomorphic to the real number field. On the other hand, the set of first-order sentences valid in the reals has arbitrarily large models due to the compactness theorem. Thus the least-upper-bound property cannot be expressed by any set of sentences in first-order logic. (In fact, every
real-closed field
In mathematics, a real closed field is a field ''F'' that has the same first-order properties as the field of real numbers. Some examples are the field of real numbers, the field of real algebraic numbers, and the field of hyperreal numbers.
De ...
satisfies the same first-order sentences in the signature
as the real numbers.)
In second-order logic, it is possible to write formal sentences that say "the domain is
finite
Finite is the opposite of infinite. It may refer to:
* Finite number (disambiguation)
* Finite set, a set whose cardinality (number of elements) is some natural number
* Finite verb, a verb form that has a subject, usually being inflected or marke ...
" or "the domain is of
countable
In mathematics, a set is countable if either it is finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function from it into the natural numbers ...
cardinality
In mathematics, the cardinality of a set is a measure of the number of elements of the set. For example, the set A = \ contains 3 elements, and therefore A has a cardinality of 3. Beginning in the late 19th century, this concept was generalized ...
." To say that the domain is finite, use the sentence that says that every
surjective
In mathematics, a surjective function (also known as surjection, or onto function) is a function that every element can be mapped from element so that . In other words, every element of the function's codomain is the image of one element of i ...
function from the domain to itself is
injective
In mathematics, an injective function (also known as injection, or one-to-one function) is a function that maps distinct elements of its domain to distinct elements; that is, implies . (Equivalently, implies in the equivalent contrapositiv ...
. To say that the domain has countable cardinality, use the sentence that says that there is a
bijection between every two infinite subsets of the domain. It follows from the
compactness theorem
In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model. This theorem is an important tool in model theory, as it provides a useful (but generally no ...
and the
upward Löwenheim–Skolem theorem that it is not possible to characterize finiteness or countability, respectively, in first-order logic.
Certain fragments of second-order logic like ESO are also more expressive than first-order logic even though they are strictly less expressive than the full second-order logic. ESO also enjoys translation equivalence with some extensions of first-order logic that allow non-linear ordering of quantifier dependencies, like first-order logic extended with
Henkin quantifier In logic a branching quantifier, also called a Henkin quantifier, finite partially ordered quantifier or even nonlinear quantifier, is a partial ordering
:\langle Qx_1\dots Qx_n\rangle
of quantifiers for ''Q'' ∈ . It is a special case ...
s,
Hintikka
Kaarlo Jaakko Juhani Hintikka (12 January 1929 – 12 August 2015) was a Finnish philosopher and logician.
Life and career
Hintikka was born in Helsingin maalaiskunta (now Vantaa).
In 1953, he received his doctorate from the University of Hels ...
and Sandu's
independence-friendly logic
Independence-friendly logic (IF logic; proposed by Jaakko Hintikka and in 1989) is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form (\exists v/V) and (\forall v/V), where V is a finite set of variables. ...
, and Väänänen's
dependence logic Dependence logic is a logical formalism, created by Jouko Väänänen, which adds ''dependence atoms'' to the language of first-order logic. A dependence atom is an expression of the form =\!\!(t_1 \ldots t_n), where t_1 \ldots t_n are terms, and c ...
.
Deductive systems
A
deductive system
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A for ...
for a logic is a set of
inference rules
In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of i ...
and logical axioms that determine which sequences of formulas constitute valid proofs. Several deductive systems can be used for second-order logic, although none can be complete for the standard semantics (see below). Each of these systems is
sound
In physics, sound is a vibration that propagates as an acoustic wave, through a transmission medium such as a gas, liquid or solid.
In human physiology and psychology, sound is the ''reception'' of such waves and their ''perception'' by the ...
, which means any sentence they can be used to prove is logically valid in the appropriate semantics.
The weakest deductive system that can be used consists of a standard deductive system for first-order logic (such as
natural deduction In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use ax ...
) augmented with substitution rules for second-order terms. This deductive system is commonly used in the study of
second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
A precur ...
.
The deductive systems considered by Shapiro (1991) and Henkin (1950) add to the augmented first-order deductive scheme both comprehension axioms and choice axioms. These axioms are sound for standard second-order semantics. They are sound for Henkin semantics restricted to Henkin models satisfying the comprehension and choice axioms.
Non-reducibility to first-order logic
One might attempt to reduce the second-order theory of the real numbers, with full second-order semantics, to the first-order theory in the following way. First expand the domain from the set of all real numbers to a two-sorted domain, with the second sort containing all ''sets of'' real numbers. Add a new binary predicate to the language: the membership relation. Then sentences that were second-order become first-order, with the formerly second-order quantifiers ranging over the second sort instead. This reduction can be attempted in a one-sorted theory by adding unary predicates that tell whether an element is a number or a set, and taking the domain to be the union of the set of real numbers and the
power set
In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is po ...
of the real numbers.
But notice that the domain was asserted to include ''all'' sets of real numbers. That requirement cannot be reduced to a first-order sentence, as the
Löwenheim–Skolem theorem
In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem.
The precise formulation is given below. It implies that if a countable first-order t ...
shows. That theorem implies that there is some
countably infinite
In mathematics, a set is countable if either it is finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function from it into the natural numbers; ...
subset of the real numbers, whose members we will call ''internal numbers'', and some countably infinite collection of sets of internal numbers, whose members we will call "internal sets", such that the domain consisting of internal numbers and internal sets satisfies exactly the same first-order sentences as are satisfied by the domain of real numbers and sets of real numbers. In particular, it satisfies a sort of least-upper-bound axiom that says, in effect:
Countability of the set of all internal numbers (in conjunction with the fact that those form a densely ordered set) implies that that set does not satisfy the full least-upper-bound axiom. Countability of the set of all ''internal'' sets implies that it is not the set of ''all'' subsets of the set of all ''internal'' numbers (since
Cantor's theorem
In mathematical set theory, Cantor's theorem is a fundamental result which states that, for any set A, the set of all subsets of A, the power set of A, has a strictly greater cardinality than A itself.
For finite sets, Cantor's theorem can be ...
implies that the set of all subsets of a countably infinite set is an uncountably infinite set). This construction is closely related to
Skolem's paradox
In mathematical logic and philosophy, Skolem's paradox is a seeming contradiction that arises from the downward Löwenheim–Skolem theorem. Thoralf Skolem (1922) was the first to discuss the seemingly contradictory aspects of the theorem, and to ...
.
Thus the first-order theory of real numbers and sets of real numbers has many models, some of which are countable. The second-order theory of the real numbers has only one model, however.
This follows from the classical theorem that there is only one
Archimedean complete ordered field
In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every r ...
, along with the fact that all the axioms of an Archimedean complete ordered field are expressible in second-order logic. This shows that the second-order theory of the real numbers cannot be reduced to a first-order theory, in the sense that the second-order theory of the real numbers has only one model but the corresponding first-order theory has many models.
There are more extreme examples showing that second-order logic with standard semantics is more expressive than first-order logic. There is a finite second-order theory whose only model is the real numbers if the
continuum hypothesis
In mathematics, the continuum hypothesis (abbreviated CH) is a hypothesis about the possible sizes of infinite sets. It states that
or equivalently, that
In Zermelo–Fraenkel set theory with the axiom of choice (ZFC), this is equivalent to ...
holds and that has no model if the continuum hypothesis does not hold (cf. Shapiro 2000, p. 105). This theory consists of a finite theory characterizing the real numbers as a complete Archimedean ordered field plus an axiom saying that the domain is of the first uncountable cardinality. This example illustrates that the question of whether a sentence in second-order logic is consistent is extremely subtle.
Additional limitations of second-order logic are described in the next section.
Metalogical results
It is a corollary of
Gödel's incompleteness theorem that there is no deductive system (that is, no notion of ''provability'') for second-order formulas that simultaneously satisfies these three desired attributes:
* (
Soundness
In logic or, more precisely, deductive reasoning, an argument is sound if it is both valid in form and its premises are true. Soundness also has a related meaning in mathematical logic, wherein logical systems are sound if and only if every formu ...
) Every provable second-order sentence is universally valid, i.e., true in all domains under standard semantics.
* (
Completeness) Every universally valid second-order formula, under standard semantics, is provable.
* (
Effectiveness
Effectiveness is the capability of producing a desired result or the ability to produce desired output. When something is deemed effective, it means it has an intended or expected outcome, or produces a deep, vivid impression.
Etymology
The ori ...
) There is a
proof-checking algorithm that can correctly decide whether a given sequence of symbols is a proof or not.
This corollary is sometimes expressed by saying that second-order logic does not admit a complete
proof theory
Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Jon Barwise, Barwise (1978) consists of four correspo ...
. In this respect second-order logic with standard semantics differs from first-order logic;
Quine (1970
pp. 90–91 pointed to the lack of a complete proof system as a reason for thinking of second-order logic as not ''logic'', properly speaking.
As mentioned above, Henkin proved that the standard deductive system for first-order logic is sound, complete, and effective for second-order logic with
Henkin semantics, and the deductive system with comprehension and choice principles is sound, complete, and effective for Henkin semantics using only models that satisfy these principles.
The
compactness theorem
In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model. This theorem is an important tool in model theory, as it provides a useful (but generally no ...
and the
Löwenheim–Skolem theorem
In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem.
The precise formulation is given below. It implies that if a countable first-order t ...
do not hold for full models of second-order logic. They do hold however for Henkin models.
[ Manzano, M., ''Model Theory'', trans. Ruy J. G. B. de Queiroz (]Oxford
Oxford () is a city in England. It is the county town and only city of Oxfordshire. In 2020, its population was estimated at 151,584. It is north-west of London, south-east of Birmingham and north-east of Bristol. The city is home to the ...
: Clarendon Press
Oxford University Press (OUP) is the university press of the University of Oxford. It is the largest university press in the world, and its printing history dates back to the 1480s. Having been officially granted the legal right to print books ...
, 1999)
p. xi
History and disputed value
Predicate logic was introduced to the mathematical community by
C. S. Peirce
Charles Sanders Peirce ( ; September 10, 1839 – April 19, 1914) was an American philosopher, logician, mathematician and scientist who is sometimes known as "the father of pragmatism".
Educated as a chemist and employed as a scientist for t ...
, who coined the term ''second-order logic'' and whose notation is most similar to the modern form (Putnam 1982). However, today most students of logic are more familiar with the works of
Frege
Friedrich Ludwig Gottlob Frege (; ; 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic ph ...
, who published his work several years prior to Peirce but whose works remained less known until
Bertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell, (18 May 1872 – 2 February 1970) was a British mathematician, philosopher, logician, and public intellectual. He had a considerable influence on mathematics, logic, set theory, linguistics, ...
and
Alfred North Whitehead
Alfred North Whitehead (15 February 1861 – 30 December 1947) was an English mathematician and philosopher. He is best known as the defining figure of the philosophical school known as process philosophy, which today has found applicat ...
made them famous. Frege used different variables to distinguish quantification over objects from quantification over properties and sets; but he did not see himself as doing two different kinds of logic. After the discovery of
Russell's paradox
In mathematical logic, Russell's paradox (also known as Russell's antinomy) is a set-theoretic paradox discovered by the British philosopher and mathematician Bertrand Russell in 1901. Russell's paradox shows that every set theory that contains ...
it was realized that something was wrong with his system. Eventually logicians found that restricting Frege's logic in various ways—to what is now called
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
—eliminated this problem: sets and properties cannot be quantified over in first-order logic alone. The now-standard hierarchy of orders of logics dates from this time.
It was found that
set theory
Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...
could be formulated as an axiomatized system within the apparatus of first-order logic (at the cost of several kinds of
completeness, but nothing so bad as Russell's paradox), and this was done (see
Zermelo–Fraenkel set theory
In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such ...
), as sets are vital for
mathematics
Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
.
Arithmetic
Arithmetic () is an elementary part of mathematics that consists of the study of the properties of the traditional operations on numbers— addition, subtraction, multiplication, division, exponentiation, and extraction of roots. In the 19th ...
,
mereology, and a variety of other powerful logical theories could be formulated axiomatically without appeal to any more logical apparatus than first-order quantification, and this, along with
Gödel and
Skolem
Thoralf Albert Skolem (; 23 May 1887 – 23 March 1963) was a Norwegian mathematician who worked in mathematical logic and set theory.
Life
Although Skolem's father was a primary school teacher, most of his extended family were farmers. Skolem ...
's adherence to first-order logic, led to a general decline in work in second (or any higher) order logic.
This rejection was actively advanced by some logicians, most notably
W. V. Quine
Willard Van Orman Quine (; known to his friends as "Van"; June 25, 1908 – December 25, 2000) was an American philosopher and logician in the analytic tradition, recognized as "one of the most influential philosophers of the twentieth century". ...
. Quine advanced the view that in predicate-language sentences like ''Fx'' the "''x''" is to be thought of as a variable or name denoting an object and hence can be quantified over, as in "For all things, it is the case that . . ." but the "''F''" is to be thought of as an ''abbreviation'' for an incomplete sentence, not the name of an object (not even of an
abstract object like a property). For example, it might mean " . . . is a dog." But it makes no sense to think we can quantify over something like this. (Such a position is quite consistent with Frege's own arguments on the
concept-object distinction). So to use a predicate as a variable is to have it occupy the place of a name, which only individual variables should occupy. This reasoning has been rejected by
George Boolos
George Stephen Boolos (; 4 September 1940 – 27 May 1996) was an American philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology.
Life
Boolos is of Greek-Jewish descent. He graduated with an A.B. i ...
.
In recent years second-order logic has made something of a recovery, buoyed by Boolos' interpretation of second-order quantification as
plural quantification
In 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 ...
over the same domain of objects as first-order quantification (Boolos 1984). Boolos furthermore points to the claimed
nonfirstorderizability In formal logic, nonfirstorderizability is the inability of a natural-language statement to be adequately captured by a formula of first-order logic. Specifically, a statement is nonfirstorderizable if there is no formula of first-order logic whic ...
of sentences such as "Some critics admire only each other" and "Some of Fianchetto's men went into the warehouse unaccompanied by anyone else", which he argues can only be expressed by the full force of second-order quantification. However,
generalized quantification and
partially ordered
In mathematics, especially order theory, a partially ordered set (also poset) formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary r ...
(or branching) quantification may suffice to express a certain class of purportedly nonfirstorderizable sentences as well and these do not appeal to second-order quantification.
Relation to computational complexity
The expressive power of various forms of second-order logic on finite structures is intimately tied to
computational complexity theory
In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and relating these classes to each other. A computational problem is a task solved by ...
. The field of
descriptive complexity
''Descriptive Complexity'' is a book in mathematical logic and computational complexity theory by Neil Immerman. It concerns descriptive complexity theory, an area in which the expressibility of mathematical properties using different types of lo ...
studies which computational
complexity class
In computational complexity theory, a complexity class is a set (mathematics), set of computational problems of related resource-based computational complexity, complexity. The two most commonly analyzed resources are time complexity, time and spa ...
es can be characterized by the power of the logic needed to express languages (sets of finite strings) in them. A string ''w'' = ''w''
1···''w
n'' in a finite alphabet ''A'' can be represented by a finite structure with domain ''D'' = , unary predicates ''P
a'' for each ''a'' ∈ ''A'', satisfied by those indices ''i'' such that ''w
i'' = ''a'', and additional predicates that serve to uniquely identify which index is which (typically, one takes the graph of the successor function on ''D'' or the order relation <, possibly with other arithmetic predicates). Conversely, the
Cayley table Named after the 19th century British mathematician Arthur Cayley, a Cayley table describes the structure of a finite group by arranging all the possible products of all the group's elements in a square table reminiscent of an addition or multiplic ...
s of any finite structure (over a finite
signature
A signature (; from la, signare, "to sign") is a handwritten (and often stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and intent. The writer of a ...
) can be encoded by a finite string.
This identification leads to the following characterizations of variants of second-order logic over finite structures:
* REG (the set of
regular language
In theoretical computer science and formal language theory, a regular language (also called a rational language) is a formal language that can be defined by a regular expression, in the strict sense in theoretical computer science (as opposed to ...
s) is definable by monadic, second-order formulas (Büchi's theorem, 1960)
*
NP is the set of languages definable by existential, second-order formulas (
Fagin's theorem
Fagin's theorem is the oldest result of descriptive complexity theory, a branch of computational complexity theory that characterizes complexity classes in terms of logic-based descriptions of their problems rather than by the behavior of algorithm ...
, 1974).
*
co-NP
In computational complexity theory, co-NP is a complexity class. A decision problem X is a member of co-NP if and only if its complement is in the complexity class NP. The class can be defined as follows: a decision problem is in co-NP precisely ...
is the set of languages definable by universal, second-order formulas.
*
PH is the set of languages definable by second-order formulas.
*
PSPACE
In computational complexity theory, PSPACE is the set of all decision problems that can be solved by a Turing machine using a polynomial amount of space.
Formal definition
If we denote by SPACE(''t''(''n'')), the set of all problems that can b ...
is the set of languages definable by second-order formulas with an added
transitive closure
In mathematics, the transitive closure of a binary relation on a set is the smallest relation on that contains and is transitive. For finite sets, "smallest" can be taken in its usual sense, of having the fewest related pairs; for infinite ...
operator.
*
EXPTIME is the set of languages definable by second-order formulas with an added
least fixed point
In order theory, a branch of mathematics, the least fixed point (lfp or LFP, sometimes also smallest fixed point) of a function from a partially ordered set to itself is the fixed point which is less than each other fixed point, according to the ...
operator.
Relationships among these classes directly impact the relative expressiveness of the logics over finite structures; for example, if PH = PSPACE, then adding a transitive closure operator to second-order logic would not make it any more expressive over finite structures.
See also
*
First-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
*
Higher-order logic
mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
*
Löwenheim number In mathematical logic the Löwenheim number of an abstract logic is the smallest cardinal number for which a weak downward Löwenheim–Skolem theorem holds.Zhang 2002 page 77 They are named after Leopold Löwenheim, who proved that these exist for ...
*
Omega language
In formal language theory within theoretical computer science, an infinite word is an infinite-length sequence (specifically, an ω-length sequence) of symbols, and an ω-language is a set of infinite words. Here, ω refers to the first ordinal nu ...
*
Second-order propositional logic
A second-order propositional logic is a propositional logic extended with quantification over propositions. A special case are the logics that allow second-order Boolean propositions, where quantifiers may range either just over the Boolean truth ...
*
Monadic second-order logic In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's ...
Notes
References
*
*. Reprinted in Boolos, ''Logic, Logic and Logic'', 1998.
*
*
* . Reprinted in Putnam, Hilary (1990), ''Realism with a Human Face'',
Harvard University Press
Harvard University Press (HUP) is a publishing house established on January 13, 1913, as a division of Harvard University, and focused on academic publishing. It is a member of the Association of American University Presses. After the retirem ...
pp. 252–260
*
*
*
*
Further reading
*
*
{{Mathematical logic
Systems of formal logic
fr:Logique d'ordre supérieur#Logique du second ordre