View source for Beth definability theorem

Definability theorems provide answers to the question to what extent implicit definitions can be made explicit. Questions of this kind are a traditional issue in mathematics, as is illustrated by the following examples.

1) Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b1201801.png" /> be a [[Polynomial|polynomial]] over the real numbers having exactly one real root <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b1201802.png" />. Then the equation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b1201803.png" /> can be viewed as an implicit definition of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b1201804.png" />, i.e. as a condition on a real number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b1201805.png" /> that involves <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b1201806.png" /> and uniquely determines a number satisfying it, namely <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b1201807.png" />. The question whether there is an explicit definition of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b1201808.png" />, i.e. a description of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b1201809.png" /> not involving <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018010.png" /> itself, comes up to the question whether the implicit definition <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018011.png" /> can be made explicit, say by representing the solution <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018012.png" /> by radicals. Of course, an explicit definition of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018013.png" />, say <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018014.png" />, can also be viewed as an implicit definition. In fact, this example mirrors the general experience that explicit definitions are special cases of implicit definitions.

2) Similarly to the above, one may consider a differential equation (cf. also [[Differential equation, ordinary|Differential equation, ordinary]]; [[Differential equation, partial|Differential equation, partial]]) with exactly one real solution <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018015.png" /> as an implicit definition of the [[Function|function]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018016.png" />, whereas an explicit definition of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018017.png" /> would come up to solving the given equation explicitly.

3) Since in real closed fields the ordering is uniquely determined (cf. also [[Real closed field|Real closed field]]), the axioms of real closed fields, based on the notions of addition, multiplication and order, can be viewed as an implicit definition of the latter. This definition can be made explicit with respect to addition and multiplication, namely by

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018018.png" /></td> </tr></table>

The precise notions given below reflect typical features of the preceding examples, the relationship with example 3) being obvious already at a first glance. The restriction to definitions of relations is inessential.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018019.png" /> be a logic (cf. [[#References|[a3]]], Chap. II, and [[Logical calculus|Logical calculus]]), such as first-order logic, and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018020.png" /> be an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018022.png" />-theory, that is, a set of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018023.png" />-sentences of some vocabulary <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018024.png" />. An <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018025.png" />-ary relation symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018026.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018027.png" /> is explicitly definable in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018028.png" /> if there is some <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018029.png" />-formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018030.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018031.png" /> not containing <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018032.png" /> such that

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018033.png" /></td> </tr></table>

is a theorem of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018034.png" />. Moreover, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018035.png" /> defines <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018036.png" /> implicitly if

DI) For all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018037.png" />-structures <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018038.png" /> there is at most one <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018039.png" />-ary relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018040.png" /> over the domain of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018041.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018042.png" /> is a model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018043.png" />.

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018044.png" /> has the Beth property if for any finite <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018045.png" />-theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018046.png" />, every relation symbol which is implicitly definable in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018047.png" /> is also explicitly definable in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018048.png" />. If in DI)  "at most one"  is strengthened to  "exactly one" , the resulting analogue is called the weak Beth property.

Intuitively, implicit definitions are of a semantical nature, whereas explicit definitions are of a more syntactical character. Hence, the Beth property (and its variants) for a logic <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018049.png" /> indicate a balance between the syntax and the semantics of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018050.png" />.

There is a tight relationship between definability properties and so-called  "interpolation"  properties (cf. [[#References|[a3]]], Chaps. II; XVIII), the most important relation of the latter kind being the Craig interpolation property: A logic <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018051.png" /> has the Craig interpolation property if for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018052.png" />-formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018053.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018054.png" /> of vocabulary <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018055.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018056.png" />, respectively, such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018057.png" /> is valid, there is a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018058.png" />-formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018059.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018060.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018061.png" /> are valid. In particular, the Craig interpolation property implies the Beth property (but not vice versa). Proofs of definability properties can often be given directly, but mostly proceed by proving interpolation properties. The methods used may be either proof theoretic or model theoretic in nature.

The earliest definability result, going back to E.W. Beth, the Beth definability theorem [[#References|[a4]]], states that first-order logic has the Beth property. There are numerous results concerning the validity of definability properties for a wide range of logics.

First, logics with the Beth property are rare. Besides first-order logic the most important examples include intuitionistic predicate logic [[#References|[a11]]], <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018062.png" />, i.e. first order-logic with countably infinite conjunctions and disjunctions, [[#References|[a9]]], together with countable admissible fragments [[#References|[a2]]]. The Beth property for these fragments allows interesting applications to Borel sets [[#References|[a1]]].

There are various negative results. Three such groups are as follows:

a) Logics where, intuitively, syntax and semantics are clearly out of balance, such as first-order logic extended by a cardinality quantifier of the form  "there are k many x such that …"  for some uncountable [[Cardinal number|cardinal number]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018063.png" /> (cf. [[#References|[a3]]], Chap. IV).

b) Logics that can describe their syntax and semantics. Namely, if a logic has a recursive syntax and admits an axiomatization of, say, arithmetic, then it often allows one to implicitly define arithmetical truth which, by a theorem of A. Tarski, is not explicitly definable. The method goes back to W. Craig [[#References|[a5]]] in the framework of higher-order logic and includes, for example, weak second-order logic and first-order logic extended by the quantifier  "there are infinitely many x such that …"  (cf. [[#References|[a3]]], Chaps. II; XVIII, or [[#References|[a7]]]).

c) Logics with their semantics restricted to finite structures, including first-order logic (cf. [[#References|[a6]]]).

The negative results under b) and c) are valid for the weak Beth property too, whereas the question whether the logics under a) have the weak Beth property is widely open (1998) and the answer may, partly, depend on the underlying set theory (cf. [[#References|[a8]]]).

The uniqueness condition in the weak Beth property guarantees that, in contrast to the Beth property, any logic <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018064.png" /> has a unique smallest extension satisfying the weak Beth property, the so-called weak Beth closure, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018065.png" />, of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018066.png" />. Usually, the study of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018067.png" /> adds to the understanding of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018068.png" /> with respect to definability (cf. [[#References|[a3]]], Ch. XVII). In the finite case, the weak Beth closure of first-order logic is related to fixed-point logics (cf. [[#References|[a8]]]).

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  J. Barwise,   "Infinitary logic and admissible sets"  ''Doctoral Diss. Stanford''  (1967)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  J. Barwise,   "Infinitary logic and admissible sets"  ''J. Symbolic Logic'' , '''34'''  (1969)  pp. 226–252</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  "Model-theoretic logics"  J. Barwise (ed.)  S. Feferman (ed.) , Springer  (1985)</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  E.W. Beth,   "On Padoa's method in the theory of definition"  ''Indag. Math.'' , '''15'''  (1953)  pp. 330–339</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  W. Craig,   "Satisfaction for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018069.png" />-th order languages defined in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018070.png" />-th order languages"  ''J. Symbolic Logic'' , '''30'''  (1965)  pp. 13–25</TD></TR><TR><TD valign="top">[a6]</TD> <TD valign="top">  H.-D. Ebbinghaus,   J. Flum,   "Finite model theory" , Springer  (1995)</TD></TR><TR><TD valign="top">[a7]</TD> <TD valign="top">  R. Gostanian,   K. Hrbacek,   "On the failure of the weak Beth property"  ''Proc. Amer. Math. Soc.'' , '''58'''  (1976)  pp. 245–249</TD></TR><TR><TD valign="top">[a8]</TD> <TD valign="top">  P. Kolaitis,   "Implicit definability on finite structures and unambiguous computations" , ''Proc. 5th IEEE Symp. on Logic in Computer Science''  (1990)  pp. 168–180</TD></TR><TR><TD valign="top">[a9]</TD> <TD valign="top">  E.G.K. Lopez-Escobar,   "An interpolation theorem for denumerably long sentences"  ''Fund. Math.'' , '''57'''  (1965)  pp. 253–272</TD></TR><TR><TD valign="top">[a10]</TD> <TD valign="top">  A.H. Mekler,   S. Shelah,   "Stationary logic and its friends I"  ''Notre Dame J. Formal Logic'' , '''26'''  (1985)  pp. 129–138</TD></TR><TR><TD valign="top">[a11]</TD> <TD valign="top">  K. Schütte,   "Der Interpolationssatz der intuitionistischen Prädikatenlogik"  ''Math. Ann.'' , '''148'''  (1962)  pp. 192–200</TD></TR></table>