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 be a polynomial over the real numbers having exactly one real root . Then the equation can be viewed as an implicit definition of , i.e. as a condition on a real number that involves and uniquely determines a number satisfying it, namely . The question whether there is an explicit definition of , i.e. a description of not involving itself, comes up to the question whether the implicit definition can be made explicit, say by representing the solution by radicals. Of course, an explicit definition of , say , 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 as an implicit definition of the function , whereas an explicit definition of 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

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 be a logic (cf. [a3], Chap. II, and Logical calculus), such as first-order logic, and let be an -theory, that is, a set of -sentences of some vocabulary . An -ary relation symbol of is explicitly definable in if there is some -formula of not containing such that

is a theorem of . Moreover, defines implicitly if

DI) For all -structures there is at most one -ary relation over the domain of such that is a model of .

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

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 has the Craig interpolation property if for any -formulas and of vocabulary and , respectively, such that is valid, there is a -formula such that and 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], , 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 (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 has a unique smallest extension satisfying the weak Beth property, the so-called weak Beth closure, , of . Usually, the study of adds to the understanding of 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 -th order languages defined in -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