Second-order Logic - Syntax and Fragments

Syntax and Fragments

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:

• 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) 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 variable 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 variable that ranges over functions that take k elements of the domain and return a single element of the domain. If f is such a k-ary function symbol and t₁,...,t_k are first-order terms then the expression f(t₁,...,t_k) is a first-order term.

For each of the sorts of variable just defined, it is permissible to build up formulas by using universal and/or existential quantifiers. Thus there are many sorts of quantifiers, two for each sort of variable. 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 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)

In monadic second-order logic (MSOL), only variables for subsets of the domain are added. The second-order logic with all the sorts of variables just described is sometimes called full second-order logic to distinguish it from the monadic version.

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 or ) 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 (existential second-order) formula is one additionally having some existential quantifiers over second order variables, i.e., where 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 ESO, or even ∃SO. formulas are defined dually, the their fragment is called universal second-order logic. More expressive fragments are defined recursively for any k > 0, has the form, where is a formula. (See analytical hierarchy for the analogous construction of second-order arithmetic.)