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.

  • $\begingroup$ Libkin, in particular, is really only interested in monadic second order logic, a fragment in which there are no second-order function symbols. This may be why he omits function variables and quantifiers from his definition of second-order logic. $\endgroup$ – Carl Mummert Mar 17 '18 at 19:56
  • $\begingroup$ Similarly, van Dalen explicitly comments that his description has only set (relation) variables. $\endgroup$ – Carl Mummert Mar 17 '18 at 20:04

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.

  • $\begingroup$ As for a reference - I am afraid that a lot of this is folklore or spread throughout various books on proof theory. But Shapiro's text, recommended by Peter Smith, is excellent. The other place I would turn is Troelstra's Metamathematical Investigation of Intuitionistic Arithmetic and Analysis which is on par with Kleene's Introduction to Metamathematics as a source for rigorous definitions. $\endgroup$ – Carl Mummert Mar 17 '18 at 20:22
  • $\begingroup$ Thank you very much for your detailed answer! That's the kind of definition I was hoping to find somewhere. On the one hand it is a relief that you say that "a lot of this is folklore" (it means that maybe it's not that I'm just too dumb to understand), but on the other I still find it surprising. I knew of Shapiro's book (see the comment in Peter Smith's answer) and of Kleene's IM (but he seems to focus mainly on FOL). I admit I did not go carefully through all the book though (I simply cannot read carefully hundreds of pages from 6/7 books before being able to come up with a definition). $\endgroup$ – Manlio Mar 18 '18 at 13:07
  • $\begingroup$ Sorry, let me ask you an additional question: you used the word "type" to distinguish between individual/function/relation variables. What is the difference (if there is one) between the concepts of "type" and "sort"? Is there a reason why we should call them one way or the other? $\endgroup$ – Manlio Mar 20 '18 at 9:22
  • $\begingroup$ In this situation, there is not much difference. If we move up to full higher order logic, then the types really do start to look like "types", because we have type forming rules that tell us how to make new types form old ones, and the entire set of types is inductively defined using these rules. That system is a very primitive form of type theory. On the other hand, if we look at second order arithmetic with a language restricted to elements and sets of elements, we might just call those "two sorts", since this theory doesn't look much like type theory. $\endgroup$ – Carl Mummert Mar 20 '18 at 12:03

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.

  • $\begingroup$ Thank you for the pointer. I already knew about Shapiro's book. The problem I found with that is that he gives a formation rule for new terms, but it seems he doesn't specify what are the terms we should start with. I know (or at least I expect) they should be variables and constant symbols, but that's something I would like to read, not guess. I admit I didn't carefully go through all the pages up to ch.3, so it may just be that this is written (more or less explicitly) somewhere else in the book. $\endgroup$ – Manlio Mar 18 '18 at 12:42
  • $\begingroup$ That's also why I'm asking for a pointer...I don't want to (and I cannot) read hundreds of pages from several books before being able to get a proper definition :) $\endgroup$ – Manlio Mar 18 '18 at 12:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.