Terms in second-order logic

Question

I am having a hard time in trying to find a formal and explicit definition for the syntax of the second-order logic. I understand there may be small differences in one formalization w.r.t. another (just like, in the formalization of a first-order language, the set of connectives is often different - just because you can build the missing ones from the others), but there are some gaps that I am unable to fill in myself.

In particular, I was wondering what should be considered the set of second-order terms and I would like to be pointed to some reference book which states this (sufficiently) explicitly.

Let me elaborate a bit more on what I found:

• in van Dalen's "Logic and Structure" (5 ed, ch. 5) the author first introduces the symbols of a second-order alphabet, and then defines the set of second-order formulas. However, there's no equality among the symbols, and it's not explicitly mentioned what are the terms he uses for building the formulas. If terms were just the first-order terms they would require a symbol which is not in the alphabet.

• in Libkin's "Elements of finite model theory" (https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf, ch. 7), a second-order language is explicitly described as an extension of a FO language. He describes what are first-order terms and then...he just forgets to say what the SO terms are, and few lines below just says that $t$ and $t'$ are "terms", without mentioning their order. Should I assume SO terms are exactly FO terms? I feel this would somehow be against the next reference I am mentioning.

• in Enderton's "A mathematical introduction to logic" (ch. 4) the author introduces two sorts of second order variables (one for predicate variables and one for function variables). It seems that the SO terms should be the FO terms plus the ones obtained by applying a function variable to the FO terms). This is a bit confusing though, as in other books I didn't find the possibility to quantify explicitly on two different sorts of second-order variables. I know you can always consider a function as a set (with certain properties), but formally this changes the set of what we should call "second-order terms".

I guess this may not be extremely relevant for the development of the theory, but honestly I feel that this is not a good reason for not having a formal definition to start with. I took a look a several other books I'm not mentioning here (for brevity), so please point to some reference only if you are certain that it solves my doubts.

Answer 1

One issue is that, although a first-order language has only one type of basic variables, for individuals, a general language for second order logic has an infinite collection of types of basic variables. Here is one of the more inclusive definitions for the set of types.

1. There is a type named "$0$" for "first order" variables ($x^0$, $y^0$, $\ldots$) which are meant to range over the individuals of a given model.

2. For each $n$, there is a type for variables that range over $n$-ary relations $R(x^0_1, \ldots, x^0_n)$ on individuals.

3. For each $n$, there us a type for variables that range over $n$-ary functions $f^0(x^0_1, \ldots, x^0_n)$ which take individuals and return an individual.

There are an infinite number of variable symbols for each of these types, and each variable symbol is of only one of the types.

The signature for a particular second-order theory can then have:

1. Constant symbols of any of the types of variables (e.g. a constant symbol $+$ for a binary function, a constant symbol $0$ for an individual, a constant symbol $<$ for a binary relation between individuals, etc). In particular, this includes all the kinds of symbols that could be in a first-order signature.

2. Third-order function symbols that take a finite number of terms (each of one of the types above) and return an object of one of the types above.

3. Third-order relation symbols that take a finite number of terms (each of one of the types above).

4. It is situation dependent whether to include an equality relation for each type. Equality symbols could be omitted entirely, included for only some types, or included for all types. If they are included, the appropriate logical axioms also need to be assumed in the deductive system.

Given all that, the terms of a second-order logic in a given signature are defined by analogy with first-order logic:

1. Individual variables are terms (in any type). Some of these are function variables and some may be function symbols from the signature

2. Constant symbols from the signature are terms.

3. The function symbols of the signature, with any variables substituted into them, are terms of the appropriate type

4. If $F^\rho(x^\sigma, x^\tau)$ is a function term that takes inputs of types $\sigma$ and $\tau$, and $t^\sigma$ and $t^\tau$ are terms of the appropriate types, then $F^\rho(t^\sigma, t^\tau)$ is a term of type $\rho$. The same holds for function terms of each arity. For example, if $f^0(x^0_1)$ is a function term and $t^0$ is a term of type $0$ then $f^0(t^0)$ is also term of type $0$.

In many settings, we can get by with only part of this general syntax, just as in first-order logic we can often simply the syntax to make a purely functional or purely relational language.

• As usual, we can replace $n$-ary function symbols with $(n+1)$-ary relation symbols, although we will need to add axioms or clauses saying that the relation symbols define functions.

• In theories of arithmetic we have a pairing function which is a bijection between the set of pairs of individuals and the set of individuals. In such settings, we can reduce our relation symbols to just unary relations. For this reason, second-order arithmetic is often axiomatized as having only two types: individuals of type $0$ and unary relations on individuals. In that case there are no function variables and no quantifiers for function variables.

• Alternatively, some authors axiomatize second-order arithmetic or higher-order arithmetic with only function symbols, so there are no relation variables and no quantifiers over relations. This convention is common, in particular, in constructive higher order arithmetic. For example, the intuitionistic theory of Heyting arithmetic in all finite types, $\text{HA}^\omega$, is often axiomatized with only function variables, as is its second-order variant $\text{HA}^2$.

Second-order logic can be generalized to higher-order logic in all finite types. The syntax I am sketching here is just a restriction of that syntax to the special case where all objects in a model are of appropriately low types.

Answer 2

In my neck of the logical woods, the canonical text on second-order logic is Stewart Shapiro's (slightly oddly titled) Foundations Without Foundationalism: A Case for Second Order Logic (OUP: Oxford Logic Guides 17).

Shapiro starts the formal exposition of various second order logics in his Chap 3. There's an account of the new formation rule for terms (added to the existing first order rules) on p. 62.