Second-order logic: Difference between revisions

Revision as of 07:27, 2 June 2020

Latest revision as of 11:07, 16 August 2025

(92 intermediate revisions by 52 users not shown)

Line 1:

{{Short description|Form of logic that allows quantification over predicates}}

In [[logic]] and [[mathematics]] '''second-order logic''' is an extension of [[first-order logic]], which itself is an extension of [[propositional logic]].<ref>Shapiro (1991) and Hinman (2005) give complete introductions to the subject, with full definitions.</ref> Second-order logic is in turn extended by [[higher-order logic]] and [[type theory]].

In [[logic]] and [[mathematics]], '''second-order logic''' is an extension of [[first-order logic]], which itself is an extension of [[Propositional calculus|propositional logic]].{{efn|{{harvtxt|Shapiro|2000}} and {{harvtxt|Hinman|2005}} give complete introductions to the subject, with full definitions.}} Second-order logic is in turn extended by [[higher-order logic]] and [[type theory]].

First-order logic [[QuantificationQuantifier (logic)|quantifies]] only variables that range over individuals (elements of the [[___domain of discourse]]); second-order logic, in addition, also quantifies over [[Finitary relation|relations]]. For example, the second-order [[Sentence (mathematical logic)|sentence]] <math>\forall P\,\forall x (x \in PPx \lor x \notinneg PPx)</math> says that for every unary relation (or [[Setwell-formed (mathematics)formula|setformula]]) ''P'' of individuals, and every individual ''x'', either ''xPx'' is intrue or not(''PPx'' or it) is nottrue (this is the [[principlelaw of bivalenceexcluded middle]]). Second-order logic also includes quantification over sets[[set (mathematics)|set]]s, functions[[function (mathematics)|function]]s, and other variables as explained in the(see section ''[[#Syntax and fragments|Syntax and fragmentsbelow]]''). 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==

[[File:Kindl-Treppe Aug2021d.jpg|thumb|[[Graffiti]] in [[Neukölln]] (Berlin) showing the simplest second-order sentence admitting nontrivial models, “{{math|∃''φ'' ''φ''}}”.]]

In first-order logic, one can quantify over individuals, but not over properties. That is, in FOL 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<ref>Professor Marc Cohen lecture notes https://faculty.washington.edu/smcohen/120/SecondOrder.pdf</ref>:

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:<ref name="mcohen">{{cite web|title=Second Order Logic |last=Marc Cohen |first=S. |url=https://faculty.washington.edu/smcohen/120/SecondOrder.pdf |website=Philosophy 120A - Introduction to Logic |date=2007}}</ref>

∃x Cube(x)

<math display="block">\exists x\,\mathrm{Cube}(x)</math>

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

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

∃P P(b)

<math display="block">\exists\mathrm{P}\,\mathrm{P}(b)</math>

is not a sentence of FOL. But this is a legitimate sentence of second-order logic<ref>Professor Marc Cohen lecture notes https://faculty.washington.edu/smcohen/120/SecondOrder.pdf</ref>.

is not a sentence of first-order logic, but this is a legitimate sentence of second-order logic. Here, ''P'' is a [[predicate variable]] and is semantically a [[Set (mathematics)|set]] of individuals.<ref name="mcohen"/>

As a result, second-order logic has much more “expressive power” than FOL does. For example, there is no way in FOL to say that a and b have some property in common; but in second-order logic this would be expressed as

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:

∃P (P(a) ∧ P(b)).

<math display="block">\exists\mathrm{P}\,\forall x\,(\mathrm{P}x\leftrightarrow(\mathrm{Cube}(x)\vee\mathrm{Tet}(x))).</math>

Suppose we would like to say that a and b have the same shape. The best we could do in FOL is something like this:

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:

(Cube(a) ∧ Cube(b)) ∨ (Tet(a) ∧ Tet(b)) ∨ (Dodec(a) ∧ Dodec(b))

<math display="block">\forall\mathrm{P}\,(\forall x\,(\mathrm{P}x\leftrightarrow(\mathrm{Cube}(x)\vee\mathrm{Tet}(x)))\rightarrow\lnot\exists x\,(\mathrm{P}x\wedge\mathrm{Dodec}(x))).</math>

If the only shapes are cube, tetrahedron, and dodecahedron, for a and b to have the same shape is for them either to be both cubes, both tetrahedra, or both dodecahedra. But this FOL sentence doesn’t seem to mean quite the same thing as the English sentence it is translating — for example, it doesn’t say anything about the fact that it is shape that a and b have in common<ref>Professor Marc Cohen lecture notes https://faculty.washington.edu/smcohen/120/SecondOrder.pdf</ref>.

Second-order quantification is especially useful because it gives the ability to express [[reachability]] properties. For example, if Parent(''x'', ''y'') denotes that ''x'' is a parent of ''y'', then first-order logic cannot express the property that ''x'' is an [[ancestor]] 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'':

In second-order logic, by contrast, we could add a predicate Shape that is true of precisely the properties corresponding to the predicates Cube, Tet, and Dodec. That is,

<math display="block">\forall\mathrm{P}\,((\mathrm{P}y\wedge\forall a\,\forall b\,((\mathrm{P}b\wedge\mathrm{Parent}(a,b))\rightarrow\mathrm{P}a))\rightarrow\mathrm{P}x).</math>

Shape(Cube) ∧ Shape(Tet) ∧ Shape(Dodec)

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 predicates ''P'' Cube, Tet, and Dodec. This would require [[Higher-order logic|third-order logic]].<ref>{{Citation |last=Väänänen |first=Jouko |title=Second-order and Higher-order Logic |date=2021 |url=https://plato.stanford.edu/archives/fall2021/entries/logic-higher-order/ |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |edition=Fall 2021 |publisher=Metaphysics Research Lab, Stanford University |access-date=2022-05-03}}</ref>

So we could write:

<!-- Is this reference (for the old wrong example) still useful?

In first-order logic, such a property has to be written out explicitly for each case. For example, we can say that no object is both a cube and a tetrahedron:<ref>Stapleton, G., Howse, J., & [[John M. Lee|Lee, J. M.]], eds., ''Diagrammatic Representation and Inference: 5th International Conference, Diagrams 2008'' ([[Berlin]]/[[Heidelberg]]: [[Springer Science+Business Media|Springer]], 2008), [https://books.google.com/books?id=EuNtCQAAQBAJ&pg=PA258 p. 258].</ref>{{rp|258}} -->

∃P (Shape(P) ∧ P(a) ∧ P(b))

And this will come out true in exactly when a and b are either both cubes, both tetrahedra, or both dodecahedra. So in second-order logic we can express the idea of ''same shape'' using identity and the second-order predicate Shape; we can do without the special predicate SameShape<ref>Professor Marc Cohen lecture notes https://faculty.washington.edu/smcohen/120/SecondOrder.pdf</ref>.

Similarly, we can express the claim that no object has every shape in a way that brings out the quantifier in ''every shape'':

¬∃x ∀P(Shape(P) → P(x))

In FOL, the best we can do is to say that no block is both a cube, a tetrahedron, and a dodecahedron<ref>Professor Marc Cohen lecture notes https://faculty.washington.edu/smcohen/120/SecondOrder.pdf</ref>:

¬∃x (Cube(x) ∧ Tet(x) ∧ Dodec(x))

==Syntax and fragments==

{{anchor|fragments}}

The syntax of second-order logic tells which expressions are well formed [[formula (mathematical logic)|formulas]]. In addition to the [[First-order logic#Formation rules|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]]. Sets of individuals can also be viewed as [[Finitary relation|unary relation]]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''₁,...,''t''_''k'' are first-order terms then the expression ''R''(''t''₁,...,''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''₁,...,''t''_''k'' are first-order terms then the expression ''f''(''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. 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.&nbsp;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 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]], an algorithmic meta-theorem in [[graph theory]]. The MSO theory of the complete infinite binary tree ([[S2S (mathematics)|S2S]]) is decidable. By contrast, full second order logic over any infinite set (or MSO logic over for example (<math>\mathbb{N}</math>,+)) can interpret the true [[second-order arithmetic]].

Just as in first-order logic, second-order logic may include [[non-logical symbolssymbol]]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 <math>\Sigma^1_0</math> or <math>\Pi^1_0</math>) if its quantifiers (which may be ofuniversal eitheror typeexistential) range only over variables of first order, although it may have free variables of second order. A <math>\Sigma^1_1</math> (existential second-order) formula is one additionally having some existential quantifiers over second order variables, i.e. <math>\exists R_0\ldots\exists R_m \phi</math>, where <math>\phi</math> 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 <math>\Sigma^1_1</math>, or even as ∃SO. The fragment of <math>\Pi^1_1</math> formulas is defined dually, it is called universal second-order logic. More expressive fragments are defined for any ''k'' > 0 by mutual recursion: <math>\Sigma^1_{k+1}</math> has the form <math>\exists R_0\ldots\exists R_m \phi</math>, where <math>\phi</math> is a <math>\Pi^1_k</math> formula, and similar, <math>\Pi^1_{k+1}</math> has the form <math>\forall R_0\ldots\forall R_m \phi</math>, where <math>\phi</math> is a <math>\Sigma^1_k</math> formula. (See [[analytical hierarchy]] for the analogous construction of [[second-order arithmetic]].)

==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 [[#Vaananen2001.{{sfn|(Väänänen |2001)]].}}

In standard semantics, also called full semantics, the quantifiers range over ''all'' 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.{{sfn|Väänänen|2001}} 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 on [[type 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 that [[Gödel's completeness theorem]] and [[compactness theorem]], which hold for first-order logic, carry over to second-order logic with Henkin semantics. Since also the [[Skolem–Löwenheim theorem]]s hold for Henkin semantics, [[Lindström's theorem]] imports that Henkin models are just ''disguised first-order models''.<ref>*{{cite book |author=Mendelson, Elliot

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.

|title=Introduction to Mathematical Logic

|edition=5th

|series=Discrete Mathematics and Its Applications

|type=hardcover

|year=2009 |publisher=Chapman and Hall/CRC |___location=Boca Raton

|isbn=978-1-58488-876-5

|page=387}}

</ref>

InFor Henkintheories semantics,such each sort ofas second-order variablearithmetic, hasthe a particular ___domainexistence of itsnon-standard owninterpretations toof rangehigher-order over,domains whichisn't may bejust a proper subsetdeficiency of allthe setsparticular oraxiomatisation functionsderived offrom thattype sort.theory [[Leonthat Henkin]] (1950)used, definedbut thesea semanticsnecessary andconsequence proved thatof [[Gödel's completenessincompleteness theorem]] and [[compactness theorem]], which hold for first-order logic, carry over to second-order logic with: Henkin's semantics.axioms Thiscan't is because Henkin semantics arebe almostsupplemented identicalfurther to many-sorted first-order semantics, where additional sorts of variables are added to simulateensure the newstandard variables of second-order logic. Second-order logic with Henkin semanticsinterpretation is notthe moreonly expressive than first-orderpossible logicmodel. Henkin semantics are commonly used in the study of [[second-order arithmetic]].

Väänänen [[#Vaananen2001|(2001)Jouko Väänänen]] argued that the choicedistinction between Henkin modelssemantics and full modelssemantics for second-order logic is analogous to the choicedistinction between provability in [[ZFC]] and truth in ''[[Von Neumann universe|V]]'', asin athat basisthe forformer setobeys theory:model-theoretic "Asproperties withlike secondthe Lowenheim-orderSkolem logictheorem and compactness, weand cannotthe reallylatter choosehas whethercategoricity phenomena.{{sfn|Väänänen|2001}} For example, "we axiomatizecannot mathematicsmeaningfully usingask ''whether the <math>V''</math> oras ZFC.defined Thein result<math>\mathrm{ZFC}</math> is the samereal in<math>V</math> both. cases,But asif we reformalize <math>\mathrm{ZFC}</math> ''is''inside the<math>\mathrm{ZFC}</math>, bestthen attemptwe socan farnote tothat usethe ''V''reformalized as<math>\mathrm{ZFC}</math> an... axiomatizationhas ofcountable mathematicsmodels and hence cannot be categorical."{{Citation needed|date=December 2024}}

==Expressive power==

Second-order logic is more expressive than first-order logic. For example, if the ___domain is the set of all [[real number]]s, one can assert in first-order logic the existence of an additive inverse of each real number by writing ∀''<math>\forall x''\exists ∃''y'' (''x'' + ''y'' = 0)</math> but one needs second-order logic to assert the [[Supremum|least-upper-bound]] 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 second-order sentence (split over two lines) expresses the least upper bound property:

<math display=block>

: (&forall; A) ([{{color|#800000|(&exist; ''w'') (''w'' &isin; A)}} &and; {{color|#008000|(&exist; ''z'')(&forall; ''u'')(''u'' &isin; A &rarr; ''u'' &le; ''z'')}}]

\begin{align}

::&rarr; {{color|#0000BB|(&exist; ''x'')(&forall; ''y'')([(&forall; ''w'')(''w'' &isin; A &rarr; ''w'' &le; ''x'') &and; (&forall; ''u'')(''u'' &isin; A &rarr; ''u'' &le; ''y'')] &rarr; ''x'' &le; ''y'')}})

\forall A\biggl(&\bigl(\exists w(w\in A)\wedge

This formula is a direct formalization of "every {{color|#800000|nonempty}}, {{color|#008000|bounded}} set A {{color|#0000BB|has a least upper bound}}." It can be shown that any [[ordered 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, every [[real-closed field]] satisfies the same first-order sentences in the signature <math>\langle +,\cdot,\le\rangle</math> as the real numbers.)

\exists z\forall u(u\in A\rightarrow u\le z)\bigr)\rightarrow\\

&\exists x\Bigl(\forall u(u\in A\rightarrow u\le x)\wedge

\forall y\forall u\bigl( (u\in A\rightarrow u\le y)\rightarrow x\le y\bigr)\Bigr)\biggr)\\

\end{align}

</math>

Here, the part of the first line involving <math>w</math> represents the assumption that <math>A</math> is nonempty (it has an element, <math>w</math>). The rest of the first line represents the assumption that <math>A</math> is bounded (there exists a number <math>z</math> that is greater than equal to all elements <math>u</math> of <math>A</math>). The second line expresses the existence of a least upper bound <math>x</math>. It asserts that <math>x</math> is an upper bound (it is greater than equal to any element <math>u</math> in <math>A</math>) and that, if any number <math>y</math> is also an upper bound, then <math>x\le y</math>. Any [[ordered 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, every [[real-closed field]] satisfies the same first-order sentences in the signature <math>\langle +,\cdot,\le\rangle</math> as the real numbers.)

In second-order logic, it is possible to write formal sentences whichthat say "the ___domain is [[finite set|finite]]" or "the ___domain is of [[countable set|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 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 whichthat allow non-linear ordering of quantifier dependencies, like first-order logic extended with [[Henkin quantifier]]s, [[Hintikka]] and Sandu's [[independence-friendly logic]], and Väänänen's [[dependence logic]].

==Deductive systems==

Line 81 ⟶ 89:

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 second-order logic, although none can be complete for the standard semantics (see below). Each of these systems is [[soundness|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 first-order logic (such as [[natural deduction]]) augmented with substitution rules for second-order terms.<ref>{{efn|Such a system is used without comment by {{harvtxt|Hinman (|2005)}}.</ref>}} This deductive system is commonly used in the study of [[second-order arithmetic]].

The deductive systems considered by {{harvtxt|Shapiro (1991)|2000}} and {{harvtxt|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.<ref>{{efn|These are the models originally studied by {{harvtxt|Henkin (|1950)}}.</ref>}}

==Non-reducibility to first-order logic==

Line 89 ⟶ 97:

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]] 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]] 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 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:

:{{block indent|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 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]] 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]].

Line 98 ⟶ 106:

This follows from the classical theorem that there is only one [[Archimedean property|Archimedean]] [[real number|complete 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 the [[continuum hypothesis]] holds and whichthat has no model if the continuum hypothesis does not hold (cf. {{sfn|Shapiro |2000, |p.&nbsp;=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:<ref>{{efn|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.</ref>}}

* ([[Soundness]]) Every provable second-order sentence is universally valid, i.e., true in all domains under standard semantics.

Line 109 ⟶ 117:

* ([[Decidability (logic)|Effectiveness]]) There is a [[automated proof checking|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]]. In this respect second-order logic with standard semantics differs from first-order logic; [[W.Willard V.Van Orman Quine|Quine]] (1970, [https://books.google.com/books?id=S_NhnP0izA4C&lpg=PP3&hl=de&pg=PA90 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.{{sfn|Quine|1970|p=[https://books.google.com/books?id=S_NhnP0izA4C&pg=PA90 90–91]}}

As mentioned above, Henkin proved that the standard deductive system for first-order logic is sound, complete, and effective for second-order logic with [[Higher-order logic|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öwenheim–Skolem theorem]] do not hold for full models of second-order logic. They do hold however for Henkin models.<ref>[[María Manzano|Manzano, M.]], ''Model Theory'', trans. Ruy J. G. B. de Queiroz ([[Oxford]]: [[Oxford University Press#Vaananen2001Clarendon Press|(VäänänenClarendon 2001)Press]], 1999), [https://books.google.com/books?id=Nc5uXx057JwC&pg=PR11 p. xi].</ref>

==History and disputed value==

Predicate logic was introduced to the mathematical community by [[Charles Sanders Peirce|C. S. Peirce]], 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 [[Gottlob Frege|Frege]], who published his work several years prior to Peirce but whose works remained less known 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 [[First-order predicate calculus|first-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 that [[set theory]] could be formulated as an axiomatized system within the apparatus of first-order logic (at the cost of several kinds of [[completeness (logic)|completeness]], but nothing so bad as Russell's paradox), and this was done (see [[Zermelo–Fraenkel 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 first-order quantification, and this, along with [[Kurt Gödel|Gödel]] and [[Thoralf Skolem|Skolem]]'s adherence to first-order logic, led to a general decline in work in second (or any higher) order logic.{{Citation needed|date=January 2010}}

This rejection was actively advanced by some logicians, most notably [[W. V. Quine]]. Quine advanced the view{{Citation needed|date=January 2010}} 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 and object|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]].{{citation needed|date=April 2020}}

In recent years{{when|date=October 2017}} second-order logic has made something of a recovery, buoyed by Boolos' interpretation of second-order quantification as [[plural quantification]] over the same ___domain of objects as first-order 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 second-order quantification. However, [[generalized quantifier|generalized quantification]] and [[branching quantification|partially ordered,]] (or branching,) quantification may suffice to express a certain class of purportedly nonfirstorderizable sentences as well and itthese doesdo not appeal to second-order quantification.

== Relation to computational complexity==

{{anchor|Applications to complexity|relation to computational complexity}}

The expressive power of various forms of second-order logic on finite structures is intimately tied to [[computational complexity theory]]. The field of [[descriptive complexity]] studies which computational [[complexity class]]es can be characterized by the power of the logic needed to express languages (sets of finite strings) in them. A string ''w''&nbsp;=&nbsp;''w''₁···''w_n'' in a finite alphabet ''A'' can be represented by a finite structure with ___domain ''D''&nbsp;=&nbsp;{1,...,''n''}, unary predicates ''P_a'' for each ''a''&nbsp;∈&nbsp;''A'', satisfied by those indices ''i'' such that ''w_i''&nbsp;=&nbsp;''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]]s of any finite structure (over a finite [[signature (logic)|signature]]) can be encoded by a finite string.

{{main|SO (complexity)}}

The expressive power of various forms of second-order logic on finite structures is intimately tied to [[computational complexity theory]]. The field of [[descriptive complexity]] studies which computational [[complexity class]]es can be characterized by the power of the logic needed to express languages (sets of finite strings) in them. A string ''w''&nbsp;=&nbsp;''w''₁···''w_n'' in a finite alphabet ''A'' can be represented by a finite structure with ___domain ''D''&nbsp;=&nbsp;{1,...,''n''}, unary predicates ''P_a'' for each ''a''&nbsp;∈&nbsp;''A'', satisfied by those indices ''i'' such that ''w_i''&nbsp;=&nbsp;''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.

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

* REG (the set of [[regular language]]s) is the set of languages definable by monadic, second-order formulas ([[Büchi's-Elgot-Trakhtenbrot theorem]], 1960).

* [[NP (complexity)|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.

Line 146 ⟶ 153:

* [[Omega language]]

* [[Second-order propositional logic]]

* [[Monadic second-order logic]]

==Notes==

{{notelist}}

<references/>

==References==

{{Reflist}}

===Works cited===

* {{cite journal

| last = Henkin

| first = L.

| title = Completeness in the theory of types

| journal = Journal of Symbolic Logic

| volume = 15

| year = 1950

| pages = 81–91

| issue = 2

| doi = 10.2307/2266967

| jstor=2266967| s2cid = 36309665

}}

* {{cite book

| last = Hinman

| first = P.

| title = Fundamentals of Mathematical Logic

| publisher = A K Peters

| year = 2005

| isbn = 1-56881-262-0}}

* {{cite book

| last = Shapiro

| first= S.

| author-link = Stewart Shapiro

| title = ''Foundations without Foundationalism: A Case for Second-Order Logic''

| publisher = Clarendon Press

| ___location = Oxford

| year = 2000

| orig-year = 1991

| isbn = 0-19-825029-0}}

* {{cite journal

| last = Väänänen

|first = J.

| url = http://www.math.helsinki.fi/logic/people/jouko.vaananen/VaaSec.pdf

| title = Second-Order Logic and Foundations of Mathematics

| journal = Bulletin of Symbolic Logic

| volume = 7

| issue = 4

| year = 2001

| pages = 504–520

| doi = 10.2307/2687796

| jstor = 2687796

| citeseerx = 10.1.1.25.5579

|s2cid = 7465054

|archive-url = https://web.archive.org/web/20231008112652/http://www.math.helsinki.fi/logic/people/jouko.vaananen/VaaSec.pdf

|archive-date = 8 October 2023

}}

*{{cite book

| first = W. V.

| last = Quine

| title = Philosophy of Logic

| url = https://books.google.com/books?id=S_NhnP0izA4C

| year = 1970

| publisher = [[Prentice Hall]]

| isbn = 9780674665637

}}

==Further reading==

* {{cite book

| author=Andrews, Peter

Line 167 ⟶ 235:

|pages=430&ndash;50

|jstor = 2026308}}. Reprinted in Boolos, ''Logic, Logic and Logic'', 1998.

* {{cite book | last1=Grädel | first1=Erich | last2=Kolaitis | first2=Phokion G. | last3=Libkin | first3=Leonid | author3-link=Leonid Libkin | last4=Maarten | first4=Marx | last5=Spencer | first5=Joel | author5-link=Joel Spencer | last6=Vardi | first6=Moshe Y. | author6-link=Moshe Y. Vardi | last7=Venema | first7=Yde | last8=Weinstein | first8=Scott | title=Finite model theory and its applications | zbl=1133.03001 | series=Texts in Theoretical Computer Science. An EATCS Series | ___location=Berlin | publisher=[[Springer-Verlag]] | isbn=978-3-540-00428-8 | year=2007 }}

* {{cite journal

| author = Henkin, L.

| title = Completeness in the theory of types

| journal = Journal of Symbolic Logic

| volume = 15

| year = 1950

| pages = 81–91

| issue = 2

| doi = 10.2307/2266967

| jstor=2266967}}

* {{cite book

| author = Hinman, P.

| title = Fundamentals of Mathematical Logic

| publisher = A K Peters

| year = 2005

| isbn = 1-56881-262-0}}

* {{cite journal

| doi= 10.1016/0315-0860(82)90123-9

| author= Putnam, Hilary

|authorlinkauthor-link=Hilary Putnam

| year=1982

| title=Peirce the Logician

Line 194 ⟶ 247:

| issue= 3| doi-access=free

}}. Reprinted in Putnam, Hilary (1990), ''Realism with a Human Face'', [[Harvard University Press]], [https://books.google.com/books?id=7JFTo-ZXROMC&pg=PT252 pp.&nbsp;252&ndash;260].

*{{cite book

| author = W. V. Quine

| title = Philosophy of Logic

| url = https://books.google.com/books?id=S_NhnP0izA4C&printsec=frontcover

| year = 1970

| publisher = [[Prentice Hall]]

}}

* {{cite conference

| author = Rossberg, M.

| url = http://logic.amu.edu.pl/images/4/46/Completenessrossberg.pdf

| title = First-Order Logic, Second-Order Logic, and Completeness

| booktitlebook-title = First-order logic revisited

| editor = V. Hendricks |display-editors=et al

| publisher = Logos-Verlag

Line 211 ⟶ 257:

| year = 2004

}}

* {{cite book

| author = [[Stewart Shapiro|Shapiro, S.]]

| title = ''Foundations without Foundationalism: A Case for Second-Order Logic''

| publisher = [[Oxford University Press|Clarendon Press]]

| ___location = [[Oxford]]

| year = 2000

| orig-year = 1991

| isbn = 0-19-825029-0}}

* {{cite journal

| last = Väänänen

|first = J.

| url = https://www.math.ucla.edu/~asl/bsl/0704/0704-003.ps

| title = Second-Order Logic and Foundations of Mathematics

| journal = Bulletin of Symbolic Logic

| volume = 7

| issue = 4

| year = 2001

| pages = 504–520

| doi = 10.2307/2687796

| jstor = 2687796

| ref=Vaananen2001

| citeseerx = 10.1.1.25.5579

}}

==Further reading==

* {{cite book | last1=Grädel | first1=Erich | last2=Kolaitis | first2=Phokion G. | last3=Libkin | first3=Leonid | author3-link=Leonid Libkin | last4=Maarten | first4=Marx | last5=Spencer | first5=Joel | author5-link=Joel Spencer | last6=Vardi | first6=Moshe Y. | author6-link=Moshe Y. Vardi | last7=Venema | first7=Yde | last8=Weinstein | first8=Scott | title=Finite model theory and its applications | zbl=1133.03001 | series=Texts in Theoretical Computer Science. An EATCS Series | ___location=Berlin | publisher=[[Springer-Verlag]] | isbn=978-3-540-00428-8 | year=2007 }}

{{Mathematical logic}}

[[Category:Systems of formal logic]]

[[Category:Charles Sanders Peirce]]

[[fr:Logique d'ordre supérieur#Logique du second ordre]]