We’ll set this up in the most general way and later see how Hellman’s account in terms of and applies.
Letting be a language with a -ary relation symbol not appearing in the relation-symbol set of , is the language that extends and which includes . is a theory in .
We say that is explicitly definable if, and only if, there is an formula with free variables such that . And we say that is implicitly definable if, and only if, for any - structure and any (i.e., the universe of the structure), if both , and are models of , then .
Beth’s definability theorem says that if a language with a -ary relation symbol not appearing in the relation-symbol set of , is the language that extends and which includes and is a theory in , then is explicitly definable if, and only if, is implicitly definable.
To prove that explicit definability implies implicit definability is straightforward. Assume . Show for , if . Since we’re assuming , is definable over (i.e., for -ary , , for with free variables. Let . So ; but and models . So .
To prove that implicit definability implies explicit definability takes just a bit longer, but it’s simple; using the Compactness Theorem and the Craig Interpolation Theorem.
Next time I’ll turn to how Hellman deals with the problems posed by this theorem.