Definition in satisfiability problem While I was reading the PhD thesis of Balder ten Cate (2005). Model theory for extended modal languages. I found a theorem that says: **2.6.4Theorem.** The frame satisfiability problem for modal formulas is highly undecidable, in fact not analytical. My question is: What that mean highly undecidable and not analytical?

By "undecidable", the author means the problem has a nonzero Turing degree - there is no algorithm that decides the problem correctly.

By "not analytical", the author means that the problem is not classifiable in the analytical hierarchy. This is equivalent to saying that it is not definable by a formula of second-order arithmetic.

Appendix B of the thesis appears to have a summary of this.