An example that comes to mind is the set of recursive dilators; this is a $\Pi^1_2$-complete set (Theorem 4.1 in Girard 1985, Introduction to $\Pi^1_2$-logic). Dilators have some use outside of logic (e.g.: Some uses of dilators in combinatorial problems I, II, III).

An example that comes to mind is the set of recursive dilators; this is a $\Pi^1_2$-complete set (Theorem 4.1 in Girard 1985, Introduction to $\Pi^1_2$-logic). Dilators have some use outside of logic (e.g.: Some uses of dilators in combinatorial problems I, II, III).

Added October 27:

Definition: A dilator is functor from ON to ON (the large poset of ordinals and strictly increasing functions) preserving filtered colimits and pullbacks. A dilator is weakly finite if it maps finite ordinals to finite ordinals. A dilator is recursive if it is weakly finite and the morphism part is a recursive function from N to N under a standard coding of finite sequences as numbers.

Thus, weakly finite dilators are coded by reals, while recursive dilators are coded by numbers, and in the latter case forming a $\Pi^1_2$-complete set, just as the usual set of codes of recursive ordinals forms a $\Pi^1_1$-complete set.