MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Call a higher-order logic fully monadic if and only if all of its predicate constants (at any order) and higher-order variables (at any order) are monadic (and it has no function symbols). In /Solvable cases of the decision problem/, Ackermann proves that fully monadic second-order logic is decidable, and so complete. My question: has this result been, or can it be, extended to fully monadic logics of even higher order?

(My gut tells me it should be so extensible; failures of decidability stem, even in FOL, from having relational predicates, and so you'd expect so long as you keep away from them as you go up the hierarchy you'd be in the clear. But I'd like something more solid than my gut on this one.)

share|cite|improve this question
It is customary not to crosspost unless it has been at MSE for a long enough period of time to be clear it is not getting an answer there. And if cross-posted you should let people know. This is basically to avoid repetition. – Benjamin Steinberg Sep 18 '12 at 12:59

It seems to me that, by allowing predicates of higher order, you've essentially counteracted the monadicity assumption at lower orders and therefore shouldn't expect decidability. Specifically, for elements $x,y$ of the ground domain, monadic second-order admits predicates (sets) like $\{x,y\}$ and $\{x\}$, monadic 3rd-order admits the Kuratowski ordered pair $\{\{x\},\{x,y\}\}$, and monadic 4th-order allows sets of such ordered pairs. So you can code binary predicates on the ground domain, and that destroys decidability.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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