View source for Beth definability theorem

<!--This article has been texified automatically. Since there was no Nroff source code for this article, 
the semi-automatic procedure described at https://encyclopediaofmath.org/wiki/User:Maximilian_Janisch/latexlist
was used.
If the TeX and formula formatting is correct, please remove this message and the {{TEX|semi-auto}} category.

Out of 69 formulas, 68 were replaced by TEX code.-->

{{TEX|semi-auto}}{{TEX|partial}}
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 $p ( x )$ be a [[Polynomial|polynomial]] over the real numbers having exactly one real root $\alpha$. Then the equation $p ( x ) = 0$ can be viewed as an implicit definition of $\alpha$, i.e. as a condition on a real number $x$ that involves $x$ and uniquely determines a number satisfying it, namely $\alpha$. The question whether there is an explicit definition of $\alpha$, i.e. a description of $\alpha$ not involving $\alpha$ itself, comes up to the question whether the implicit definition $p ( x ) = 0$ can be made explicit, say by representing the solution $\alpha$ by radicals. Of course, an explicit definition of $\alpha$, say $\alpha = \sqrt { 2 }$, 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 $f$ as an implicit definition of the [[Function|function]] $f$, whereas an explicit definition of $f$ 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

\begin{equation*} x \leq y \Leftrightarrow \exists z : x = y + z ^ { 2 }. \end{equation*}

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 $\mathcal{L}$ be a logic (cf. [[#References|[a3]]], Chap. II, and [[Logical calculus|Logical calculus]]), such as first-order logic, and let $T$ be an $\mathcal{L}$-theory, that is, a set of $\mathcal{L}$-sentences of some vocabulary $\tau$. An $n$-ary [[relation symbol]] $P$ of $\tau$ is explicitly definable in $T$ if there is some $\tau$-formula $\varphi ( x _ { 1 } , \dots , x _ { n } )$ of $\mathcal{L}$ not containing $P$ such that

\begin{equation*} \forall x _ { 1 } \dots \forall x _ { n } ( P  { x_1  \dots x _ { N }} \leftrightarrow \varphi ( x _ { 1 } , \ldots , x _ { n } ) ) \end{equation*}

is a theorem of $T$. Moreover, $T$ defines $P$ implicitly if

DI) For all $( \tau \backslash \{ P \} )$-structures $\mathcal{A}$ there is at most one $n$-ary relation $P ^ { \mathcal{A} }$ over the domain of $\mathcal{A}$ such that $( \mathcal{A} , P ^ { \mathcal{A} } )$ is a model of $T$.

$\mathcal{L}$ has the Beth property if for any finite $\mathcal{L}$-theory $T$, every relation symbol which is implicitly definable in $T$ is also explicitly definable in $T$. 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 $\mathcal{L}$ indicate a balance between the syntax and the semantics of $\mathcal{L}$.

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 $\mathcal{L}$ has the Craig interpolation property if for any $\mathcal{L}$-formulas $\varphi$ and $\psi$ of vocabulary $\sigma$ and $\tau$, respectively, such that $\varphi \rightarrow \psi$ is valid, there is a $\sigma \cap \tau$-formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/b/b120/b120180/b12018059.png"/> such that $\varphi \rightarrow \chi$ and $\chi \rightarrow \psi$ 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]]], $\mathcal{L} _ { \omega _ { 1 } \omega }$, 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]] $\kappa$ (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 $\mathcal{L}$ has a unique smallest extension satisfying the weak Beth property, the so-called weak Beth closure, $ \operatorname { WB} ( \mathcal{L} )$, of $\mathcal{L}$. Usually, the study of $ \operatorname { WB} ( \mathcal{L} )$ adds to the understanding of $\mathcal{L}$ 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 $n$-th order languages defined in $n$-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>