In logic and mathematics secondorder logic is an extension of firstorder logic, which itself is an extension of propositional logic.^{[1]} Secondorder logic is in turn extended by higherorder logic and type theory.
Firstorder logic quantifies only variables that range over individuals (elements of the domain of discourse); secondorder logic, in addition, also quantifies over relations. For example, the secondorder sentence \forall P\,\forall x (x \in P \lor x \notin P) says that for every unary relation (or set) P of individuals and every individual x, either x is in P or it is not (this is the principle of bivalence). Secondorder logic also includes quantification over functions, and other variables as explained in the section Syntax and fragments below. Both firstorder and secondorder logic use the idea of a domain of discourse (often called simply the "domain" or the "universe"). The domain is a set of individual elements which can be quantified over.
Syntax and fragments
The syntax of secondorder logic tells which expressions are well formed formulas. In addition to the syntax of firstorder logic, secondorder 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 firstorder term then the expression t ∈ S (also written S(t), or St to save parentheses) is an atomic formula. Sets of individuals can also be viewed as unary relations on the domain.

For each natural number k there is a sort of variables that ranges over all kary relations on the individuals. If R is such a kary relation variable and t_{1},..., t_{k} are firstorder 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 kary function variable and t_{1},...,t_{k} are firstorder terms then the expression f(t_{1},...,t_{k}) is a firstorder 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 secondorder logic, as in firstorder logic, is a wellformed 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 nary 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 secondorder logic (MSOL) is a restriction of secondorder logic in which only quantification over unary relations (i.e.: sets) are allowed. Quantification over functions, owing to the equivalence to relations as described above, is thus also not allowed. The secondorder logic without these restrictions is sometimes called full secondorder logic to distinguish it from the monadic version.
Just as in firstorder logic, secondorder logic may include nonlogical symbols in a particular secondorder language. These are restricted, however, in that all terms that they form must be either firstorder terms (which can be substituted for a firstorder variable) or secondorder terms (which can be substituted for a secondorder variable of an appropriate sort).
A formula in secondorder logic is said to be of firstorder (and sometimes denoted \Sigma^1_0 or \Pi^1_0) if its quantifiers (which may be of either type) range only over variables of first order, although it may have free variables of second order. A \Sigma^1_1 (existential secondorder) formula is one additionally having some existential quantifiers over second order variables, i.e. \exists R_0\ldots\exists R_m \phi, where \phi is a firstorder formula. The fragment of second order logic consisting only of existential secondorder formulas is called existential secondorder logic and abbreviated as ESO, as \Sigma^1_1, or even as ∃SO. The fragment of \Pi^1_1 formulas is defined dually, it is called universal secondorder logic. More expressive fragments are defined for any k > 0 by mutual recursion: \Sigma^1_{k+1} has the form \exists R_0\ldots\exists R_m \phi, where \phi is a \Pi^1_k formula, and similar, \Pi^1_{k+1} has the form \forall R_0\ldots\forall R_m \phi, where \phi is a \Sigma^1_k formula. (See analytical hierarchy for the analogous construction of secondorder arithmetic.)
Semantics
The semantics of secondorder logic establish the meaning of each sentence. Unlike firstorder logic, which has only one standard semantics, there are two different semantics that are commonly used for secondorder logic: standard semantics and Henkin semantics. In each of these semantics, the interpretations of the firstorder quantifiers and the logical connectives are the same as in firstorder logic. Only the ranges of quantifiers over secondorder 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 firstorder variables is established, the meaning of the remaining quantifiers is fixed. It is these semantics that give secondorder logic its expressive power, and they will be assumed for the remainder of this article.
In Henkin semantics, each sort of secondorder variable has a particular domain of its own to range over, which may be a proper subset of all sets or functions of that sort. Leon Henkin (1950) defined these semantics and proved that Gödel's completeness theorem and compactness theorem, which hold for firstorder logic, carry over to secondorder logic with Henkin semantics. This is because Henkin semantics are almost identical to manysorted firstorder semantics, where additional sorts of variables are added to simulate the new variables of secondorder logic. Secondorder logic with Henkin semantics is not more expressive than firstorder logic. Henkin semantics are commonly used in the study of secondorder arithmetic.
Väänänen (2001) argued that the choice between Henkin models and full models for secondorder logic is analogous to the choice between ZFC and V as a basis for set theory: "As with secondorder 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
Secondorder logic is more expressive than firstorder logic. For example, if the domain is the set of all real numbers, one can assert in firstorder logic the existence of an additive inverse of each real number by writing ∀x ∃y (x + y = 0) but one needs secondorder logic to assert the leastupperbound property for sets of real numbers, which states that every bounded, nonempty set of real numbers has a supremum. If the domain is the set of all real numbers, the following secondorder sentence (split over two lines) expresses the least upper bound property:

(∀ A) ([(∃ w) (w ∈ A) ∧ (∃ z)(∀ u)(u ∈ A → u ≤ z)]

→ (∃ x)(∀ y)[(∀ w)(w ∈ A → w ≤ y) ↔ (x ≤ y)])
This formula is a direct formalization of "every nonempty, bounded set A has a least upper bound." The leastupperbound property cannot be expressed by any set of sentences in firstorder logic, because the real numbers are up to isomorphism the unique ordered field that satisfies this property, whereas the set of firstorder sentences valid in the reals has arbitrarily large models due to the compactness theorem. (In fact, every realclosed field satisfies the same firstorder sentences in the signature \langle +,\cdot,\le\rangle as the real numbers.)
In secondorder logic, it is possible to write formal sentences which say "the domain is finite" or "the domain is of countable cardinality." To say that the domain is finite, use the sentence that says that every surjective function from the domain to itself is injective. 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 and the upward Löwenheim–Skolem theorem that it is not possible to characterize finiteness or countability, respectively, in firstorder logic.
Certain fragments of second order logic like ESO are also more expressive than firstorder logic even though they are strictly less expressive than the full secondorder logic. ESO also enjoys translation equivalence with some extensions of firstorder logic which allow nonlinear ordering of quantifier dependencies, like firstorder logic extended with Henkin quantifiers, Hintikka and Sandu's independencefriendly logic, and Väänänen's dependence logic.
Deductive systems
A deductive system for a logic is a set of inference rules and logical axioms that determine which sequences of formulas constitute valid proofs. Several deductive systems can be used for secondorder logic, although none can be complete for the standard semantics (see below). Each of these systems is sound, 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 firstorder logic (such as natural deduction) augmented with substitution rules for secondorder terms.^{[2]} This deductive system is commonly used in the study of secondorder arithmetic.
The deductive systems considered by Shapiro (1991) and Henkin (1950) add to the augmented firstorder deductive scheme both comprehension axioms and choice axioms. These axioms are sound for standard secondorder semantics. They are sound for Henkin semantics if only Henkin models that satisfy the comprehension and choice axioms are considered.^{[3]}
Nonreducibility to firstorder logic
One might attempt to reduce the secondorder theory of the real numbers, with full secondorder semantics, to the firstorder theory in the following way. First expand the domain from the set of all real numbers to a twosorted 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 secondorder become firstorder, with the formerly secondorder quantifiers ranging over the second sort instead. This reduction can be attempted in a onesorted 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 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 firstorder sentence, as the Löwenheim–Skolem theorem shows. That theorem implies that there is some countably infinite 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 firstorder sentences as are satisfied by the domain of real numbers and sets of real numbers. In particular, it satisfies a sort of leastupperbound axiom that says, in effect:

Every nonempty internal set that has an internal upper bound has a least internal upper bound.
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 leastupperbound 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 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.
Thus the firstorder theory of real numbers and sets of real numbers has many models, some of which are countable. The secondorder 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, along with the fact that all the axioms of an Archimedean complete ordered field are expressible in secondorder logic. This shows that the secondorder theory of the real numbers cannot be reduced to a firstorder theory, in the sense that the secondorder theory of the real numbers has only one model but the corresponding firstorder theory has many models.
There are more extreme examples showing that secondorder logic with standard semantics is more expressive than firstorder logic. There is a finite secondorder theory whose only model is the real numbers if the continuum hypothesis holds and which 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 secondorder 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 secondorder formulas that simultaneously satisfies these three desired attributes:^{[4]}

(Soundness) Every provable secondorder sentence is universally valid, i.e., true in all domains under standard semantics.

(Completeness) Every universally valid secondorder formula, under standard semantics, is provable.

(Effectiveness) There is a proofchecking algorithm that can correctly decide whether a given sequence of symbols is a proof or not.
This corollary is sometimes expressed by saying that secondorder logic does not admit a complete proof theory. In this respect secondorder logic with standard semantics differs from firstorder logic; Quine (1970, pp. 90–91) pointed to the lack of a complete proof system as a reason for thinking of secondorder logic as not logic, properly speaking.
As mentioned above, Henkin proved that the standard deductive system for firstorder logic is sound, complete, and effective for secondorder 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 and the LöwenheimSkolem theorem do not hold for full models of secondorder logic. They do hold however for Henkin models. (Väänänen 2001)
History and disputed value
Predicate logic was primarily introduced to the mathematical community by C. S. Peirce, who coined the term secondorder 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, who actually published his work several years prior to Peirce but whose works remained in obscurity until Bertrand Russell and Alfred North Whitehead 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 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 firstorder logic—eliminated this problem: sets and properties cannot be quantified over in firstorderlogic alone. The nowstandard hierarchy of orders of logics dates from this time.
It was found that set theory could be formulated as an axiomatized system within the apparatus of firstorder logic (at the cost of several kinds of completeness, but nothing so bad as Russell's paradox), and this was done (see ZermeloFraenkel set theory), as sets are vital for mathematics. Arithmetic, mereology, and a variety of other powerful logical theories could be formulated axiomatically without appeal to any more logical apparatus than firstorder quantification, and this, along with Gödel and Skolem's adherence to firstorder 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. Quine advanced the view that in predicatelanguage 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 conceptobject 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 Boolos.
In recent years secondorder logic has made something of a recovery, buoyed by plural quantification over the same domain of objects as firstorder quantification (Boolos 1984). Boolos furthermore points to the claimed nonfirstorderizability 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 secondorder quantification. However, generalized quantification and partially ordered, or branching, quantification may suffice to express a certain class of purportedly nonfirstorderizable sentences as well and it does not appeal to secondorder quantification.
Relation to computational complexity

The expressive power of various forms of secondorder logic on finite structures is intimately tied to computational complexity theory. The field of descriptive complexity studies which computational complexity classes 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 = {1,...,n}, unary predicates P_{a} for each a ∈ A, satisfied by those indices i such that w_{i} = a, and additional predicates which 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 table of any finite structure can be encoded by a finite string.
With this identification, we have the following characterizations of variants of secondorder logic over finite structures:

REG (the set of regular languages) is definable by monadic, secondorder formulas (Büchi's theorem, 1960)

NP is the set of languages definable by existential, secondorder formulas (Fagin's theorem, 1974).

coNP is the set of languages definable by universal, secondorder formulas.

PH is the set of languages definable by secondorder formulas.

PSPACE is the set of languages definable by secondorder formulas with an added transitive closure operator.

EXPTIME is the set of languages definable by secondorder formulas with an added least fixed point 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 secondorder logic would not make it any more expressive over finite structures.
See also
Notes

^ Shapiro (1991) and Hinman (2005) give complete introductions to the subject, with full definitions.

^ Such a system is used without comment by Hinman (2005).

^ These are the models originally studied by Henkin (1950).

^ The proof of this corollary is that a sound, complete, and effective deduction system for standard semantics could be used to produce a recursively enumerable completion of Peano arithmetic, which Gödel's theorem shows cannot exist.
References

Andrews, Peter (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (2nd ed.). Kluwer Academic Publishers.

Boolos, George (1984). "To Be Is To Be a Value of a Variable (or to Be Some Values of Some Variables)". Journal of Philosophy 81 (8): 430–50. . Reprinted in Boolos, Logic, Logic and Logic, 1998.

Henkin, L. (1950). "Completeness in the theory of types". Journal of Symbolic Logic 15 (2): 81–91.

Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters.

Putnam, Hilary (1982). "Peirce the Logician". Historia Mathematica 9 (3): 290–301. . Reprinted in Putnam, Hilary (1990), Realism with a Human Face, Harvard University Press, pp. 252–260.

W.V. Quine (1970). Philosophy of Logic. PrenticeHall.

Rossberg, M. (2004). V. Hendricks et al., eds., ed. "Firstorder logic revisited". Berlin: LogosVerlag.

Shapiro, S. (2000). Foundations without Foundationalism: A Case for Secondorder Logic. Oxford University Press.

Väänänen, J. (2001). "SecondOrder Logic and Foundations of Mathematics". Bulletin of Symbolic Logic 7 (4): 504–520.
Further reading
This article was sourced from Creative Commons AttributionShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, EGovernment Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a nonprofit organization.