Hanf Numbers and Decidability Currently reading J.L. Bell's Models and Ultraproducts and at the end of Chapter 4 section 4 the authors comment that "In spite of the fact that most languages can easily be shown to possess Hanf numbers, the problem of computing (or even estimating) the Hanf number of a given language is in general very difficult. However, for first order predicate languages the calculation is simple." 
Can someone tell me whether the problem of computing the Hanf number for a given first-order language is a decidable problem? A given second order language? And can someone give me a source on this? I grant I haven't been able to get a hold of Hanf's paper. 
Thanks!
 A: It's not clear how to phrase "compute the Hanf number" as a problem for which decidability makes sense. The Hanf number problem takes in a logic, and outputs a cardinal; decidability, or computability, makes sense in the context of natural numbers.
In certain cases, the Hanf number is completely understood. For example, for a first-order language $L$, the Hanf number is $\aleph_0$.
In other cases, basic properties of the Hanf number can be independent of ZFC. For instance, ZFC proves that the Hanf number of second-order logic - more generally, any set-sized logic at all - exists; however, it also proves that if a measurable cardinal exists, then the Hanf number of second-order logic is at least the least measurable cardinal. Since the existence of measurables is independent of ZFC, this means the question "Is the Hanf number of second-order logic $\ge$ a measurable cardinal?" is independent of ZFC.
This approach - via questions about Hanf numbers, rather than Hanf numbers themselves - is one for which (un)decidability makes sense. We could ask, "How complicated is the set of theorems about the Hanf number?" However, by virtue of the complexity of ZFC alone this would be bumped up to halting problem, regardless of the logic in question. So this isn't the way to go.
Although Hanf numbers are a topic for which independence makes sense, I don't think computability-theoretic issues fit; one could try looking at higher recursion theory, e.g. $E$-recursion, but even that doesn't seem promising.
