On the completeness and the decidability of strictly monadic second-order logic

Regarding strictly monadic second-order logic (SMSOL), which is the fragment of monadic second-order logic in which all predicate constants are unary and there are no function symbols, we show that a standard deductive system with full comprehension is sound and complete with respect to standard semantics. This result is achieved by showing that in the case of SMSOL, the truth value of any formula in a faithful identity-standard Henkin structure is preserved when the structure is "standardized"; that is, the predicate domain is expanded into the set of all unary relations. In addition, we obtain a simpler proof of the decidability of SMSOL. (c) 2021 Wiley-VCH GmbH