Second Order Logic
SECOND ORDER LOGIC
Second-order logic is the extension of first-order logic obtained by introducing quantification of predicate and function variables. A first-order formula, say Fxy, may be converted to a second-order formula by replacing F with a dyadic relation variable X, obtaining Xxy. Existential quantification yields ∃X Xxy, which may be read "there is a relation that x bears to y." In general relation variables of all adicities are admissible. Similarly, quantifiable function variables may be introduced.
Semantics for the Second-Order Logic
A structure, with non-empty domain D, for a second-order language includes relation domains Reln (D ) and function domains Funcn (D ). In general Reln (D ) C P (Dn ), where P (Dn ) is the power set of Dn. Similarly, the function domains Funcn(D ) are subsets of the collection of n -place total functions on D. Such second-order structures are called Henkin or general structures. If X is an n -place relation variable, a formula ∃X φ(X ) is true in a Henkin structure M if there is an n -place relation R ∈ Reln (D ) such that φ(X ) is true in M when X has the value R. There is a similar definition for formulas of the form ∀X φ(X ) and for formulas with quantified function variables. A formula φ is a Henkin semantic consequence of a set Δ of formulas if φ is true in all Henkin models of Δ.
The relation domain Reln(D ) need not contain all subsets of Dn. If Reln(D ) = P (Dn ) for each n, we say that each relation domain is full (similarly for function domains) and that the structure is full, standard or principal. Second-order logic restricted to full structures is called full or standard second-order logic. A formula φ is a full semantic consequence of a set Δ if φ is true in all full models of Δ. A formula is valid if it is true in all full structures.
In Henkin semantics, the Completeness, Compactness and Löwenheim-Skolem Theorems hold because Henkin structures can be reinterpreted as many-sorted first-order structures. This yields Henkin's Completeness Theorem: There exists a deductive system DS such that if φ is a Henkin consequence of axioms Δ then there is a deduction of φ from Δ using the rules of DS. For further details, see Shapiro 1991, Shapiro 2001, or van Dalen 1994.
Expressive Power
Following Gottfried Leibniz, we may define "x = y " as "any property of x is a property of y." The corresponding second-order definition ∀x ∀y (x = y ↔ ∀X (Xx → Xy )) is valid. In contrast with first-order logic, there are categorical second-order theories with infinite models: All full models are isomorphic. For example, let Δ be the theory with axioms ∀x (s (x ) ≠ 0), ∀x ∀y (s (x ) = s (y ) → x = y ) and ∀X [(X 0 ∧ ∀x (Xx → Xs (x ))) → ∀xXx ]. Any full model of Δ is isomorphic to the structure (N , 0, S ), where N is the set of natural numbers and S the successor operation. So, the Löwenheim-Skolem Theorems fail in full second-order logic. Consider the theory Δ ∪ {c ≠ 0, c ≠ s 0, c ≠ ss 0, …}, with c a constant. This theory has no full model, but any finite subset of it has a full model. So the Compactness Theorem fails, too.
Extending Δ with the recursion axioms for addition and multiplication, we obtain the theory PA2 whose unique full model up to isomorphism is the natural number structure (N, 0, S, +, x). Similarly there is an axiom system whose unique full model up to isomorphism is the ordered field of real numbers, (R , 0, 1, +, x, <). More generally there exist second-order formulas expressing cardinality claims inexpressible in first-order logic. The most striking example concerns the Continuum Hypothesis (CH), which says that there is no cardinal number between ℵ0 and 2ℵ0. Results due to Kurt Gödel and Paul Cohen imply that the Continuum Hypothesis is independent of standard axiomatic set theory (ZFC). But there is a second-order formula CH* which is valid just in case CH is true.
If we augment PA2 with inference rules for the second-order quantifiers and the monadic comprehension scheme ∃X ∀x (Xx ↔ φ), we obtain axiomatic second-order arithmetic, Z2. (See Simpson 1998 for a detailed investigation of Z2 and its subsystems.) One may construct a Gödel sentence G, true just in case G is not a theorem of Z2. Now, all full models of Z2 are isomorphic to (N, 0, S, +, x). So an arithmetic sentence φ is true just in case φ is a full semantic consequence of Z2. G is thus a full semantic consequence of Z2 but not a theorem of Z2. The Completeness Theorem therefore fails; there is no sound and complete, recursively axiomatized, deductive system for full second-order logic. Indeed the set of second-order validities is not recursively enumerable. For further details see Shapiro 1991, Shapiro 2001, or Enderton 2001.
Is Second-Order Logic Logic?
Second-order comprehension has the form ∃X ∀x 1 … ∀x n(Xx 1…x n ↔ φ). Should such existential axioms count as logical? Does this violate the topic-neutrality of logic? W. V. Quine argued that second-order logic is "set theory in sheep's clothing" because "set theory's staggering existential assumptions are cunningly hidden … in the tacit shift from schematic predicate letter to quantifiable variable" (Quine 1970, p. 68). Another reason for not counting second-order logic as logic is that the full semantic consequence relation does not allow a complete proof procedure.
In reply George Boolos pointed out that the obvious translation from second-order formulas to first-order set-theoretic formulas does not map valid formulas to set-theoretic theorems. For example ∃X ∀yXy is valid, while ∃x ∀y (y ∈ x ) is refutable in axiomatic set theory. Furthermore ∃X ∃x ∃y (Xx ∧ Xy ∧ x ≠ y ) is not valid, and so "second-order logic is not committed to the existence of even a two-membered set" (Boolos 1975 [1998], pp. 40–41). Furthermore first-order logic does have a complete proof procedure, but the set of first-order validities is undecidable (Church's Theorem), while the monadic fragment is decidable. So why is completeness used to draw the line between logic and mathematics rather than decidability?
The Interpretation of Second-Order Variables
George Boolos (1984, 1985) has provided monadic second-order logic with a novel interpretation: the plural interpretation. Certain natural language locutions that receive monadic second-order formalizations are perhaps better analysed as instances of plural quantification. For example the Geach-Kaplan sentence, "Some critics admire only one another," may be formalized as ∃X (∃xXx ∧ ∀x ∀y (Xx ∧ Axy → x ≠ y ∧ Xy )). This formula is non-first-orderizable (not equivalent to a first-order formula containing just the predicates A and =). According to the usual interpretation, its truth implies the existence of a collection. The plural interpretation reads "There are some [critics] such that, for any x and y, if x is one of them and admires y, then y is not x and y is one of them." Rather than asserting the existence of a collection, this is a plural means of referring to individuals. Second-order logic can also be applied to set theory. In this context we can interpret monadic second-order quantification over sets as plural quantification.
See also Computability Theory; First-Order Logic; Gödel, Kurt; Leibniz, Gottfried Wilhelm; Logic, History of: Modern Logic: From Frege to Gödel; Mathematics, Foundations of; Proof Theory; Quine, Willard Van Orman.
Bibliography
Boolos, George. Logic, Logic and Logic. Cambridge, MA: Harvard University Press, 1998.
Boolos, George. "Nominalist Platonism." Philosophical Review 94 (1985): 327–344. Reprinted in Boolos 1998.
Boolos, George. "On Second-Order Logic." Journal of Philosophy 72 (1975): 509–527. Reprinted in Boolos 1998.
Boolos, George. "To Be Is to Be a Value of a Variable (or to Be Some Values of Some Variables)." Journal of Philosophy 81 (1984): 430–449. Reprinted in Boolos 1998.
Enderton, Herbert. A Mathematical Introduction to Logic. San Diego, CA: Harcourt/Academic Press, 2001.
Shapiro, Stewart. Foundations Without Foundationalism: A Case for Second-Order Logic. Oxford: Oxford University Press, 1991.
Shapiro, Stewart. "Second-Order Logic." In Blackwell Guide to Philosophical Logic, edited by Lou Goble. Oxford: Blackwell, 2001.
Simpson, Stephen G. Subsystems of Second-Order Arithmetic. Berlin: Springer, 1998.
Quine, W. V. O. Philosophy of Logic. Cambridge, MA: Harvard University Press, 1970.
van Dalen, Dirk. Logic and Structure. Berlin: Springer-Verlag, 1994.
Jeffrey Ketland (2005)