Are the implicitly definable sets of a second-order theory the sets the second-order quantifiers range over? I know that in a second-order setting, due to the failure of the Beth definability theorem, implicit and explicit definition come apart (i.e., there are predicates which can be implicitly, but not explicitly, defined). I'm trying to better understand implicit definition in this context.
The definition I've typically seen runs as follows [taken from this handout]:

A predicate π is implicitly definable in a theory $T$ from non-logical symbols $\beta_1\dots \beta_m$ if for all models $\mathcal{M, N}$ of $T$:
$\beta_i^{\mathcal{M}} = \beta_i^{\mathcal{N}}$ for all $i=1,\dots,m$ implies $\pi^{\mathcal{M}} = \pi^{\mathcal{N}}$

Unlike explicit definition, there is no mention of the requirement that there be a formula in the language that uniquely identifies the set being defined. Given that, it seems possible (unless the restriction enters from somewhere else) that there could be more than countably many implicitly definable sets in a given theory (i.e., more definable sets than formulas of the language).
If that's right, then are the (second-order) implicitly definable sets of a theory $T$ just the sets in the powerset of the domain (i.e., the sets that the second order quantifiers range over)?
 A: The answer depends on your definition of nonlogical symbols. In the more reasonable case where you require a symbol to be expressible, or in other words countable (so you might have a language with finitely many nonlogical symbols, or nonlogical symbols that can be defined in a formal language, etc), then there are only countably many finite sets of $\mathcal{B}_i$'s. Then there are only countably many formulas that can be produced using one of these sets of nonlogical symbols. Then the equivalence classes of distinct predicates defined from these countably many formulas is itself countable.
On the other hand, it is not impossible to think about a language with an uncountable collection of nonlogical symbols. I'd consider this an unreasonable foundation for anything, and if you are doing this in a class I'd guess this is not the approach you are taking. However, if there are uncountably many nonlogical symbols, then you typically have an uncountable number of implicitly definable predicates. Take for example a language where each real number corresponds to a nonlogical symbol and a theory which associates each of these symbols with the associated constant representing the corresponding real number. Then every real singleton is an implicitly definable set, and so in this case the implicitly definable predicates are not countable.
