5
$\begingroup$

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.)

$\endgroup$
9
$\begingroup$

No, it can't be extended above second order.

At as soon as you hit third order fully monadic logic, you have enough types to quantify over Kuratowski pairs of individuals (and posit a predicate constant that encodes a set of such pairs), which allows you to simulate first-order logic with a binary predicate, and thus general set theory.

$\endgroup$
1
$\begingroup$

For a proof of the above statement, see Tharp, Leslie H. The Characterization of Monadic Logic. J. Symbolic Logic 38 (1973), no. 3, 481--488

$\endgroup$

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.