Inlogic andmathematics,second-order logic is an extension offirst-order logic, which itself is an extension ofpropositional logic.^[a] Second-order logic is in turn extended byhigher-order logic andtype theory.

First-order logicquantifies only variables that range over individuals (elements of thedomain of discourse); second-order logic, in addition, quantifies overrelations. For example, the second-ordersentence${\displaystyle \mathrm{\forall }P\mathrm{\forall }x(Px\vee \mathrm{\neg }Px)}$ says that for everyformulaP, and every individualx, eitherPx is true or not(Px) is true (this is thelaw of excluded middle). Second-order logic also includes quantification oversets,functions, and other variables (see sectionbelow). Both first-order and second-order logic use the idea of adomain of discourse (often called simply the "domain" or the "universe"). The domain is a set over which individual elements may be quantified.

First-order logic can quantify over individuals, but not over properties. That is, we can take anatomic sentence like Cube(b) and obtain a quantified sentence by replacing the name with a variable and attaching a quantifier:^[1]

$${\displaystyle \mathrm{\exists }x\mathrm{C}\mathrm{u}\mathrm{b}\mathrm{e}(x)}$$

However, we cannot do the same with the predicate. That is, the following expression:

$${\displaystyle \mathrm{\exists }\mathrm{P}\mathrm{P}(b)}$$

is not a sentence of first-order logic, but this is a legitimate sentence of second-order logic. Here,P is apredicate variable and is semantically aset of individuals.^[1]

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:

$${\displaystyle \mathrm{\exists }\mathrm{P}\mathrm{\forall }x(\mathrm{P}x\leftrightarrow (\mathrm{C}\mathrm{u}\mathrm{b}\mathrm{e}(x)\vee \mathrm{T}\mathrm{e}\mathrm{t}(x))).}$$

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:

$${\displaystyle \mathrm{\forall }\mathrm{P}(\mathrm{\forall }x(\mathrm{P}x\leftrightarrow (\mathrm{C}\mathrm{u}\mathrm{b}\mathrm{e}(x)\vee \mathrm{T}\mathrm{e}\mathrm{t}(x)))\to \mathrm{\neg }\mathrm{\exists }x(\mathrm{P}x\wedge \mathrm{D}\mathrm{o}\mathrm{d}\mathrm{e}\mathrm{c}(x))).}$$

Second-order quantification is especially useful because it gives the ability to expressreachability properties. For example, if Parent(x,y) denotes thatx is a parent ofy, then first-order logic cannot express the property thatx is anancestor ofy. In second-order logic we can express this by saying that every set of people containingy and closed under the Parent relation containsx:

$${\displaystyle \mathrm{\forall }\mathrm{P}((\mathrm{P}y\wedge \mathrm{\forall }a\mathrm{\forall }b((\mathrm{P}b\wedge \mathrm{P}\mathrm{a}\mathrm{r}\mathrm{e}\mathrm{n}\mathrm{t}(a,b))\to \mathrm{P}a))\to \mathrm{P}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 cannot say, for example, that there is a property Shape(P) that is true for the predicatesP Cube, Tet, and Dodec. This would requirethird-order logic.^[2]

The syntax of second-order logic prescribes which expressions are well formedformulas. In addition to thesyntax of first-order logic, second-order logic includes many newsorts (sometimes calledtypes) of variables. These are:

• A sort of variables that range over sets of individuals. IfS is a variable of this sort andt is a first-order term then the expressiont ∈S (also writtenS(t), orSt to save parentheses) is anatomic formula. Sets of individuals can also be viewed asunary relations on the domain.
• For each natural numberk there is a sort of variables that ranges over allk-ary relations on the individuals. IfR is such ak-ary relation variable andt₁,...,t_k are first-order terms then the expressionR(t₁,...,t_k) is an atomic formula.
• For each natural numberk there is a sort of variables that ranges over all functions takingk elements of the domain and returning a single element of the domain. Iff is such ak-ary function variable andt₁,...,t_k are first-order terms then the expressionf(t₁,...,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. Asentence 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 ann-ary function variable can be represented by a relation variable of arityn+1 and an appropriate formula for the uniqueness of the "result" in then+1 argument of the relation. (Shapiro 2000, p. 63)

Monadic second-order logic (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 calledfull second-order logic to distinguish it from the monadic version. Monadic second-order logic is particularly used in the context ofCourcelle's theorem, an algorithmic meta-theorem ingraph theory. The MSO theory of the complete infinite binary tree (S2S) isdecidable. By contrast, full second-order logic over any infinite set (or MSO logic over for example (${\displaystyle \mathbb{N}}$,+)) can interpret the truesecond-order arithmetic.

Just as in first-order logic, second-order logic may includenon-logical symbols 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${\displaystyle {\mathrm{\Sigma }}_0^1}$ or${\displaystyle {\mathrm{\Pi }}_0^1}$) 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${\displaystyle {\mathrm{\Sigma }}_1^1}$ (existential second-order) formula is one additionally having some existential quantifiers over second-order variables, i.e.${\displaystyle \mathrm{\exists }{R}_0\dots \mathrm{\exists }{R}_m\varphi }$, where${\displaystyle \varphi }$ is a first-order formula. The fragment of second-order logic consisting only of existential second-order formulas is calledexistential second-order logic and abbreviated as ESO, as${\displaystyle {\mathrm{\Sigma }}_1^1}$, or even as ∃SO. The fragment of${\displaystyle {\mathrm{\Pi }}_1^1}$ formulas is defined dually, it is called universal second-order logic. More expressive fragments are defined for anyk > 0 by mutual recursion:${\displaystyle {\mathrm{\Sigma }}_{k+1}^1}$ has the form${\displaystyle \mathrm{\exists }{R}_0\dots \mathrm{\exists }{R}_m\varphi }$, where${\displaystyle \varphi }$ is a${\displaystyle {\mathrm{\Pi }}_k^1}$ formula, and similar,${\displaystyle {\mathrm{\Pi }}_{k+1}^1}$ has the form${\displaystyle \mathrm{\forall }{R}_0\dots \mathrm{\forall }{R}_m\varphi }$, where${\displaystyle \varphi }$ is a${\displaystyle {\mathrm{\Sigma }}_k^1}$ formula. (Seeanalytical hierarchy for the analogous construction ofsecond-order arithmetic.)

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 andHenkin 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.^[3]

In standard semantics, also called full semantics, the quantifiers range overall sets or functions of the appropriate sort. A model with this condition is called a full model, and these are the same as models in which the range of the second-order quantifiers is the powerset of the model's first-order part.^[3] 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 (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 ontype theory, 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 thatGödel's completeness theorem andcompactness theorem, which hold for first-order logic, carry over to second-order logic with Henkin semantics. Since also theLöwenheim–Skolem theorems hold for Henkin semantics,Lindström's theorem imports that Henkin models are justdisguised first-order models.^[4]

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 ofGö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 ofsecond-order arithmetic.

Jouko Väänänen argued that the distinction between Henkin semantics and full semantics for second-order logic is analogous to the distinction between provability inZFC and truth inV, in that the former obeys model-theoretic properties like the Löwenheim–Skolem theorem and compactness, and the latter has categoricity phenomena.^[3] For example, "we cannot meaningfully ask whether the${\displaystyle V}$ as defined in${\displaystyle \mathrm{Z}\mathrm{F}\mathrm{C}}$ is the real${\displaystyle V}$. But if we reformalize${\displaystyle \mathrm{Z}\mathrm{F}\mathrm{C}}$ inside${\displaystyle \mathrm{Z}\mathrm{F}\mathrm{C}}$, then we can note that the reformalized${\displaystyle \mathrm{Z}\mathrm{F}\mathrm{C}}$ ... has countable models and hence cannot be categorical."^{[citation needed]}

Second-order logic is more expressive than first-order logic. For example, if the domain is the set of allreal numbers, one can assert in first-order logic the existence of an additive inverse of each real number by writing${\displaystyle \mathrm{\forall }x\mathrm{\exists }y(x+y=0)}$ but one needs second-order logic to assert theleast-upper-bound property for sets of real numbers, which states that every bounded, nonempty set of real numbers has asupremum. 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:Here, the part of the first line involving${\displaystyle w}$ represents the assumption that${\displaystyle A}$ is nonempty (it has an element,${\displaystyle w}$). The rest of the first line represents the assumption that${\displaystyle A}$ is bounded from above (there exists a number${\displaystyle z}$ that is greater than or equal to all elements${\displaystyle u}$ of${\displaystyle A}$). The second line expresses the existence of a least upper bound${\displaystyle x}$. It asserts that${\displaystyle x}$ is an upper bound (it is greater than or equal to any element${\displaystyle u}$ in${\displaystyle A}$) and that, if any number${\displaystyle y}$ is also an upper bound, then${\displaystyle x\le y}$. Anyordered field 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, everyreal-closed field satisfies the same first-order sentences in the signature${\displaystyle ⟨+,\cdot ,\le ⟩}$ as the real numbers.)

In second-order logic, it is possible to write formal sentences that say “the domain isfinite” or “the domain is ofcountablecardinality.” To say that the domain is finite, use the sentence that says that everysurjective function from the domain to itself isinjective. To say that the domain has countable cardinality, use the sentence that says that there is abijection between every two infinite subsets of the domain. It follows from thecompactness theorem and theupward 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 withHenkin quantifiers,Hintikka and Sandu’sindependence-friendly logic, and Väänänen’sdependence logic.

Adeductive system for a logic is a set ofinference rules 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 issound, 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 asnatural deduction) augmented with substitution rules for second-order terms.^[b] This deductive system is commonly used in the study ofsecond-order arithmetic.

The deductive systems considered byShapiro (2000) andHenkin (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.^[c]

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 allsets 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 one whether an element is a number or a set, and taking the domain to be the union of the set of real numbers and thepower set of the real numbers.

But notice that the domain was asserted to includeall sets of real numbers. That requirement cannot be reduced to a first-order sentence, or even afirst-order theory, as theLöwenheim–Skolem theorem shows. That theorem implies that there is somecountably infinite subset of the real numbers, whose members we will callinternal 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 allinternal sets implies that it is not the set ofall subsets of the set of allinternal numbers (sinceCantor's theorem implies that the set of all subsets of a countably infinite set is an uncountably infinite set). This construction is closely related toSkolem's paradox.

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 oneArchimedeancomplete ordered field, 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 thecontinuum hypothesis holds and that has no model if the continuum hypothesis does not hold.^[5] 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.

It is a corollary ofGödel's incompleteness theorem that there is no deductive system (that is, no notion ofprovability) for second-order formulas that simultaneously satisfies these three desired attributes:^[d]

• (Soundness) 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) There is aproof-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 completeproof theory. In this respect second-order logic with standard semantics differs from first-order logic;Quine pointed to the lack of a complete proof system as a reason for thinking of second-order logic as notlogic, properly speaking.^[6]

As mentioned above, Henkin proved that the standard deductive system for first-order logic is sound, complete, and effective for second-order logic withHenkin 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.

Thecompactness theorem and theLöwenheim–Skolem theorem do not hold for full models of second-order logic. They do hold however for Henkin models.^[7]

Predicate logic was introduced to the mathematical community byC. S. Peirce, who coined the termsecond-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 ofFrege, who published his work several years prior to Peirce but whose works remained less known untilBertrand Russell andAlfred 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 ofRussell'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 calledfirst-order logic—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 thatset theory could be formulated as an axiomatized system within the apparatus of first-order logic (at the cost of several kinds ofcompleteness, but nothing so bad as Russell's paradox), and this was done (seeZermelo–Fraenkel set theory), as sets are vital formathematics.Arithmetic,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 withGödel andSkolem's adherence to first-order logic, led to a general decline in work in second (or any higher) order logic.^{[citation needed]}

This rejection was actively advanced by some logicians, most notablyW. V. Quine. Quine advanced the view^{[citation needed]} that in predicate-language sentences likeFx 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 anabbreviation for an incomplete sentence, not the name of an object (not even of anabstract 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 theconcept-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 byGeorge Boolos.^{[citation needed]}

In recent years^[when?] second-order logic has made something of a recovery, buoyed by Boolos’ interpretation of second-order quantification asplural quantification over the same domain of objects as first-order quantification (Boolos 1984). Boolos furthermore points to the claimednonfirstorderizability 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 andpartially ordered (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.

The expressive power of various forms of second-order logic on finite structures is intimately tied tocomputational complexity theory. The field ofdescriptive complexity studies which computationalcomplexity classes can be characterized by the power of the logic needed to express languages (sets of finite strings) in them. A stringw = w₁···w_n in a finite alphabetA can be represented by a finite structure with domainD = {1,...,n}, unary predicatesP_a for eacha ∈ A, satisfied by those indicesi such thatw_i = a, and additional predicates that serve to uniquely identify which index is which (typically, one takes the graph of the successor function onD or the order relation <, possibly with other arithmetic predicates). Conversely, theCayley tables of any finite structure (over a finitesignature) can be encoded by a finite string.

This identification leads to the following characterizations of variants of second-order logic over finite structures:

• REG (theregular languages) is the set of languages definable by monadic, second-order formulas (Büchi-Elgot-Trakhtenbrot theorem, 1960).
• NP is the set of languages definable by existential, second-order formulas (Fagin's theorem, 1974).
• co-NP is the set of languages definable by universal, second-order formulas.
• PH is the set of languages definable by second-order formulas.
• PSPACE is the set of languages definable by second-order formulas with an addedtransitive closure operator.
• EXPTIME is the set of languages definable by second-order formulas with an addedleast fixed point operator.

Relationships among these classes directly impact the relative expressiveness of the logics over finite structures; for example, ifPH = PSPACE, then adding a transitive closure operator to second-order logic would not make it any more expressive over finite structures.

• First-order logic
• Higher-order logic
• Löwenheim number
• Omega language
• Second-order propositional logic
• Monadic second-order logic

• Henkin, L. (1950). "Completeness in the theory of types".Journal of Symbolic Logic.15 (2):81–91.doi:10.2307/2266967.JSTOR 2266967.S2CID 36309665.
• Hinman, P. (2005).Fundamentals of Mathematical Logic. A K Peters.ISBN 1-56881-262-0.
• Shapiro, S. (2000) [1991].Foundations without Foundationalism: A Case for Second-Order Logic. Oxford: Clarendon Press.ISBN 0-19-825029-0.
• Väänänen, J. (2001)."Second-Order Logic and Foundations of Mathematics"(PDF).Bulletin of Symbolic Logic.7 (4):504–520.CiteSeerX 10.1.1.25.5579.doi:10.2307/2687796.JSTOR 2687796.S2CID 7465054. Archived fromthe original(PDF) on 8 October 2023.
• Quine, W. V. (1970).Philosophy of Logic.Prentice Hall.ISBN 9780674665637.

• 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.doi:10.2307/2026308.JSTOR 2026308.. Reprinted in Boolos,Logic, Logic and Logic, 1998.
• Grädel, Erich; Kolaitis, Phokion G.;Libkin, Leonid; Maarten, Marx;Spencer, Joel;Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007).Finite model theory and its applications. Texts in Theoretical Computer Science. An EATCS Series. Berlin:Springer-Verlag.ISBN 978-3-540-00428-8.Zbl 1133.03001.
• Putnam, Hilary (1982)."Peirce the Logician".Historia Mathematica.9 (3):290–301.doi:10.1016/0315-0860(82)90123-9.. Reprinted in Putnam, Hilary (1990),Realism with a Human Face,Harvard University Press,pp. 252–260.
• Rossberg, M. (2004)."First-Order Logic, Second-Order Logic, and Completeness"(PDF). In V. Hendricks; et al. (eds.).First-order logic revisited. Berlin: Logos-Verlag.

• Systems of formal logic
• Charles Sanders Peirce

• Articles with short description
• Short description is different from Wikidata
• All articles with unsourced statements
• Articles with unsourced statements from December 2024
• Articles with unsourced statements from January 2010
• Articles with unsourced statements from April 2020
• All articles with vague or ambiguous time
• Vague or ambiguous time from October 2017