is decidable. By contrast, full second-order logic over any infinite set (or MSO logic over for example (,+)) can interpret the true second-order arithmetic and is thus undecidable.

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