Namespaces
Variants
Actions

Difference between revisions of "Beth definability theorem"

From Encyclopedia of Mathematics
Jump to: navigation, search
m (link)
m (finish TeX)
 
(2 intermediate revisions by one other user not shown)
Line 1: Line 1:
 +
<!--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 and if all png images have been replaced by TeX code, please remove this message and the {{TEX|semi-auto}} category.
 +
 +
Out of 69 formulas, 68 were replaced by TEX code.-->
 +
 +
{{TEX|done}}
 
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.
 
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.
+
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 <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.
+
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
 
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>
+
\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.
 
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
+
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
  
<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>
+
\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 <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
+
is a theorem of $T$. Moreover, $T$ defines $P$ 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" />.
+
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$.
  
<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.
+
$\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 <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" />.
+
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 <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.
+
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 $\chi$ 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.
 
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]]].
+
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:
 
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).
+
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]]]).
 
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]]]).
Line 39: Line 47:
 
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 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]]]).
+
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====
 
====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>
+
<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>

Latest revision as of 19:09, 18 July 2020

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 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, partial) with exactly one real solution $f$ as an implicit definition of the 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), 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. [a3], Chap. II, and 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. [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 $\chi$ 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 [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 [a11], $\mathcal{L} _ { \omega _ { 1 } \omega }$, i.e. first order-logic with countably infinite conjunctions and disjunctions, [a9], together with countable admissible fragments [a2]. The Beth property for these fragments allows interesting applications to Borel sets [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 $\kappa$ (cf. [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 [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. [a3], Chaps. II; XVIII, or [a7]).

c) Logics with their semantics restricted to finite structures, including first-order logic (cf. [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. [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. [a3], Ch. XVII). In the finite case, the weak Beth closure of first-order logic is related to fixed-point logics (cf. [a8]).

References

[a1] J. Barwise, "Infinitary logic and admissible sets" Doctoral Diss. Stanford (1967)
[a2] J. Barwise, "Infinitary logic and admissible sets" J. Symbolic Logic , 34 (1969) pp. 226–252
[a3] "Model-theoretic logics" J. Barwise (ed.) S. Feferman (ed.) , Springer (1985)
[a4] E.W. Beth, "On Padoa's method in the theory of definition" Indag. Math. , 15 (1953) pp. 330–339
[a5] W. Craig, "Satisfaction for $n$-th order languages defined in $n$-th order languages" J. Symbolic Logic , 30 (1965) pp. 13–25
[a6] H.-D. Ebbinghaus, J. Flum, "Finite model theory" , Springer (1995)
[a7] R. Gostanian, K. Hrbacek, "On the failure of the weak Beth property" Proc. Amer. Math. Soc. , 58 (1976) pp. 245–249
[a8] P. Kolaitis, "Implicit definability on finite structures and unambiguous computations" , Proc. 5th IEEE Symp. on Logic in Computer Science (1990) pp. 168–180
[a9] E.G.K. Lopez-Escobar, "An interpolation theorem for denumerably long sentences" Fund. Math. , 57 (1965) pp. 253–272
[a10] A.H. Mekler, S. Shelah, "Stationary logic and its friends I" Notre Dame J. Formal Logic , 26 (1985) pp. 129–138
[a11] K. Schütte, "Der Interpolationssatz der intuitionistischen Prädikatenlogik" Math. Ann. , 148 (1962) pp. 192–200
How to Cite This Entry:
Beth definability theorem. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Beth_definability_theorem&oldid=39430
This article was adapted from an original article by H.-D. Ebbinghaus (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article