Second-order logic

In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. 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 logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations. For example, the second-order sentence ∀ P ∀ x ( x ∈ P ∨ x ∉ P ) {displaystyle forall P,forall x(xin Plor x otin 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). Second-order logic also includes quantification over sets, functions, and other variables as explained in the section Syntax and fragments. 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. The syntax of second-order logic tells which expressions are well formed formulas. In addition to the syntax of first-order logic, second-order logic includes many new sorts (sometimes called types) of variables. These are: Each of the variables just defined may be universally and/or existentially quantified over, to build up formulas. Thus there are many kinds of quantifiers, two for each sort of variables. A sentence in second-order logic, as in first-order logic, is a well-formed formula with no free variables (of any sort). It's possible to forgo the introduction of function variables in the definition given above (and some authors do this) because an n-ary function variable can be represented by a relation variable of arity n+1 and an appropriate formula for the uniqueness of the 'result' in the n+1 argument of the relation. (Shapiro 2000, p. 63) Monadic second-order logic (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. Just as in first-order logic, second-order logic may include non-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 Σ 0 1 {displaystyle Sigma _{0}^{1}} or Π 0 1 {displaystyle Pi _{0}^{1}} ) 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 Σ 1 1 {displaystyle Sigma _{1}^{1}} (existential second-order) formula is one additionally having some existential quantifiers over second order variables, i.e. ∃ R 0 … ∃ R m ϕ {displaystyle exists R_{0}ldots exists R_{m}phi } , where ϕ {displaystyle phi } 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 Σ 1 1 {displaystyle Sigma _{1}^{1}} , or even as ∃SO. The fragment of Π 1 1 {displaystyle Pi _{1}^{1}} formulas is defined dually, it is called universal second-order logic. More expressive fragments are defined for any k > 0 by mutual recursion: Σ k + 1 1 {displaystyle Sigma _{k+1}^{1}} has the form ∃ R 0 … ∃ R m ϕ {displaystyle exists R_{0}ldots exists R_{m}phi } , where ϕ {displaystyle phi } is a Π k 1 {displaystyle Pi _{k}^{1}} formula, and similar, Π k + 1 1 {displaystyle Pi _{k+1}^{1}} has the form ∀ R 0 … ∀ R m ϕ {displaystyle forall R_{0}ldots forall R_{m}phi } , where ϕ {displaystyle phi } is a Σ k 1 {displaystyle Sigma _{k}^{1}} formula. (See analytical hierarchy for the analogous construction of second-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 and Henkin semantics. In each of these semantics, the interpretations of the first-order quantifiers and the logical connectives are the same as in first-order logic. Only the ranges of quantifiers over second-order variables differ in the two types of semantics (Väänänen 2001).