I've come across a some notation that I have not seen before and since it's all symbols, I couldn't really find anything on Google about it. I don't think it's necessary/relevant to explain the entire context here, but the formula read like this:
where COINF if the index set of all coinfinite recursively enumerable sets.
It's probably not all that complicated, but I've never seen the quantifier notation before. What does it mean? The variable is supposed to range over the natural numbers.