HIERARCHIES OF PROGRAM LOGICS UDC 517.11

M. A. Taitslin

INTRODUCTION The logic Lw1~, to which a vast literature is devoted, is the most "classical" among the logics that are more powerful than the first-order predicate logic. However, the fact that each countable system is described by a single formula of this logic up to isomorphism apparently demonstrates that this logic is too powerful. Trials have already been made long ago to study "reasonable" fragments of this logic. From these fragments Barwise isolated in [I] those fragments for which a certain compactness theorem holds and called them admissible. However, Magazov has recently established in [2] the interesting fact that "well-defined" fragments may not be admissible. Possibly, the most natural extension of the first-order predicate logic is the so-called weak logic of order w, obtained from the first-order predicate logic by the addition of hereditarily finite predicate variables of arbitrary finite steps and quantifiers with respect to these predicates. This logic is described in Sec. I of the survey [3]. Belyaev has found in [3] two more logics that are equivalent in expressive power to the weak logic of order on infinite systems. One of these logics is given in the form of a fragment of the logic L~l~, and we call it the Belyaev logic. It follows from the above-mentioned results of Magazov [2] that the Belyaev logic is not an admissible fragment. Our description of the Belyaev logic is given in Sec. I. In the well-knowo, books [4, 5] of Harel, a family of logics that can be easily represented in form of fragments of the logic L~L ~ is introduced. We would like to compare these logics with each other and with the Belyaev logic with respect to expressive power and also to obtain a description of the Belyaev logic in the form of a modal logic, similar to Harel's logics. Here, of course, there is no space to discuss as to why the Harel specifications are, in some sense, operational in comparison with those given in the form of fragments. The problems, to be considered by us, can also be of some practical interest, e.g., for the choice of the relational data base enquiry languages; however, in this article we restrict ourselves, on the contrary, to the model-theoretic aspects only. For this reason we have not extended the set of logics, considered by us, by means of all the constructions that occur in prograrmning, as we wish to preserve comprehensibility and simplicity of the definition of a class for those logicians who are presently not interested in the problems of programming theory. We introduce the set of logics, each of which is weaker than the Belyaev logic in expressive power, but the interrelations between the various logics of this class is not yet completely clear. We divide these logics into two classes, depending on whether the languages with an infinite number of free variables are admissible in the modalities or not. We observe that there is no logic in the second class that is equivalent to the Belyaev logic. The formulas of a logic of the first class may contain infinitely many free variables. Therefore, if we restrict ourselves to the Harel modalities, then for the elimination of such formulas it would be necessary to eliminate the modalities over languages with an infinite number of free variables and, therefore, to eliminate the logics of the first class. Therefore, it is necessary to introduce a new modality. Our modality <~, T> differs from the Harel modality in that new values are ascribed to the variables from T in an arbitrary manner such that all variables with sufficiently large numbers are given the same value. Of course, such understanding is natural for programming reasons also. This article is based on the lectures on the model theory which I delivered at the Kazakh State University during the academic session 1980-81. I thank the listeners of these lectures for useful discussions. Translated from Sibirskii Matematicheskii S. M. Kirov Kazakh State University, Alma-Ata. Zhurnal, Vol. 24, No. 3, pp. 184-192, May-June, 1983. Original article submitted October 28, 1981. 0037-4466/83/2403-0469507.50

9 1984 Plenum Publishing Corporation

469

I.

THE BELYAEV LOGIC

We fix a finite signature ~. Let F be the set of symbols of the operations of the signature ~, R be the set of the predicate symbols of the signature ~, VF be the denumerable set of symbols of the variables, and ~(f) and ~(P) be the numbers of the argument places of the symbol of the operation f and of the symbol of the predicate P of the signature ~, respectively. Finiteness of ~ means that R U F is finite. We suppose that the elements of the sets R, F, VF, and { V , A , ~, ~, v, =} are not sets (do not contain elements), but are praelements (see [I]). Moreover, we suppose that these four sets are pairwise disjoint. Each sequence of the form Pvl ... v m, =fwl ... WsWs+l or =zlz2, where P E R , f~(P)=m, f E F , ~(f) = s, and Vl,...,Vm, Wl .... ,ws+l, zl, z2 are variables, is called an atomic formula. An atomic formula contains freely precisely those variables which are its elements. Atomic formulas, and also the sequences A (~, ~/~b, ~ i , Na~i, Va~p,, where a is a finite set of variables, @ is a denumerable set of formulas, and ~ t is a formula, are called the for-

mulas

of the logic LmI ~ of the signature ~.

A mapping of the set VF into the supporting set of the system D is called a state of the The validity of a formula ~ on a state o, in symbols O~qD , is defined in the following manner:

algebraic system D of the signature ~. e~Pz,...z~ o~----zlz2

is equivalent is equivalent

~=~z,...z,z~+, o~V(D

o~-]cp

to O(Zl)

is equivalent

is equivalent

o~A(~

to pD(o(Zl),...,O(Zm)); = o(z2);

to fD(o(Zl),...,O(Zs))

to the existence of a

is equivalent

to

o~

for each

if and only if it is false that

~E(~

= O(Zs+1); such that

o~0;

~E(D;

o~;

o~Na~p is equivalent to the existence of a state ~' of the system D such that o'(x) o(x) for x ~ a and o'S(p, o~Va~

is equivalent

to

=

o~a-]q0.

Exactly those variables occur freely in the formulas /~ (D and V~) which occur freely in one of the formulas of the set @. Precisely those variables occur freely in the formulas ~acp~ and V a ~ which occur freely in the formula (p,, but are not elements of the set a. Exactly those variables occur freely in -]qh which occur freely in the formula ~,. The natural number

~ (n~, n~) = ~/~ (n~ + n~) (n~ + n~ + I) + n~ is called the Cantor n~mber of the ordered pair n~n2 of natural numbers. Let

~,+,(n, . . . . , n,, n , + , ) = ~,(~,(ni, ..., n,), n,+~). For

each

natural

number

m, l e t

~,,~(m), . . . , ~ , . , ( m ) •

denote

natural

numbers

such

that

J m ) , . . . , ?,. ~(m)) = m.

In place of Y2,1 and ~2,2 w e will write yl and u

respectively.

The system of the signature <+, ., O, I>, representing the set of natural numbers with the usual operations of addition and multiplication and with the distinguished elements zero and one, is called the arithmetic. A formula of the predicate logic of first order with an equation of signature <+, ", O, I, ~, ?~, ?~>. The expression ~(vl,...,v n) means that the arithmetical formula does not contain any free variable distinct from v~,...,v n. A set X of natural numbers is said to be arithmetical if there exists an arithmetical formula ~(x) such that ~(n) is valid in the arithmetic for a natural number n if and only if n E X . We say that ~(x) defines X. Let us consider an arithmetical formula 0(y, x) such that for each natural number m the formula 0(m, x) is equivalent in the arithmetic to a quantifier-free formula and for each 470

quantifier-free formula ~(x) there can be effectively G(m, x) is equivalent in the arithmetic to ~(x). We call

the smallest number m such that ~(x)

found a natural

is equivalent

number m such that

in the arithmetic

to 0(m, x)

the number of the quantifier-free arithmetical formula ~(x). We call the number of the formula ~(Xs,z(x),...,Ys,s(X)) the number of the quantifier-free arithmetical formula ~(xl ..... Ks) .

We select formulas with the least possible number of quantifiers from among the arithmetical formulas that define the arithmetical set X and are prenex and begin from the quantifier of universality or are quantifier-free. Let the number of the quantifiers in the selected formulas be equal to s. After redesignation of the connected variables, we can reduce each selected formula to the form

(vzt)(~z2) . . . (Qz~)~(z,,

(1)

..., a , x),

w h e r e Q i s v i f s i s odd a n d Q i s ~ i f s i s e v e n a n d ~O i s a q u a n t i f i e r - f r e e formula. From t h e f o r m u l a s ( 1 ) , w h i c h d e f i n e X, we s e l e c t a f o r m u l a f o r w h i c h ~ h a s t h e l e a s t n u m b e r . Let this number be m. Then we call ~2(s, m) the number of the arithmetical .set X. Let us now consider a one-to-one mapping of the set R O F U { A , V, q, 2, v, =} onto an initial segment of the natural number set and a one-to-one mapping of the set VF onto the set of the natural numbers greater than k0. Thus, we obtain a one-to-one mapping ~ of the set

M=RUFU onto

the set of natural

numbers.

VFU { A , V, -3; ~I, v, = }

Let xj denote an element

of VF such that ~(xj)

= j + ko.

Let us set A0 = M. We call the natural number w(a)=• 0, ~(a)) the number of the elea~Ao. Let A i and the mapping w of the set A i into the set of natural numbers be already constructed. We say that X is an object of genus i + 1 if X is a subset of Ai, X~Ai, the set {v(x)Ix~X} is arithmetical, and the set {?3,2(~(x))Ix~X} is bounded. If X is an object of genus i + I, then we set

ment

m = m a x {?~. 2(v(x))lx ~ X}. the natural number • m~i m2), w h e r e m2 i s t h e n u m b e r o f t h e a r i t h m e t i c a l set a n d m~ ---- max {m, ~t(m2)} , the number v(X) of the element X. L e t Ai+ z be t h e u n i o n of the set A i and the set of all objects of genus i + I. Let A be the union of all Ai, where i runs over the set of all natural numbers.

We c a l l

{v(X)tx~X}

is call

Let us recall that the sequence ab is the set {{a}, {a, b}} and the sequence {{a~...a~}, {a~...a~,a~+~}}. Therefore, certain formulas of the logic L ~ belong the formulas

variables

of the logic L~l ~ that belong

at...a~a~+~ to A.

to A and c o n t a i n only a finite number

We of free

the formulas of the Belyaev logic.

We will lent to o ~ $

say that two formulas ~ and ~ are equivalent on a system D if for each state o of the system D .

We say that a formula ~t of the Belyaev quence of formulas q~+~, ~, ..., % such that

o~cp

is equiva-

logic has special form if there exists a se%+~ is a quantifier-free formula of signature


H~>

of the first-order predicate logic with equality, where H~,...,H k are the symbols of twoplace predicates that do not occur in ~ and ~p~ , i = 1,...,k, are either 2a~p~+~ or Va(p~+~, where a is (xj} for j < s, or

V {~a[ (q~+~)~ l 1 = 0, t, 2 . . . . }, or

A {Va~ (~i+l)z I1 = 0, 1, 2 . . . . ]. Here

t ai={xn, xn+,!n~-s~. 2i+2jk;

]=0,

i .....

/},

Where s is a natural number such that xi, i >/ s, do not occur in ~k+~, and (~+~)z is obtained from qc~§ by replacing each subformula of the form Hiulu2 by the formula V{ A{=u~x~, = u 2 x ~ + ~ } l n =

s + 2i+ 27k; ] = 0 ,

t~ . . . , l}.

471

Here it is assumed that the symbols H~,...,H k do not already occur in the formula

~

THEOREM I. With each formula ~ of the Belyaev logic or of the weak logic of order there can be associated a formula of special form of the Belyaev logic that is equivalent q~ on infinite systems.

to

Proof. Repeating the arguments given in Sec. I of the survey [3], we get analogs of Lemmas 7 and 9 of Sec. I of the survey [3]. The theorem is proved. 2.

PROGRAM LOGICS

Each expression of the form (x i § t), where t is a term, is called an appropriation. Each expression of the form (~?), where ~ is a formula of the Belyaev logic, is called a test. This test is said to be quantifier-free or elementary if cp is, respectively, a quantifier-free or an arbitrary formula of the first-order predicate logic with equality. Each sequence of tests and appropriations, in which all tests are quantifier-free (elementary), is said to be q~ntifier-free (elementary). Each set of finite sequences of tests and appropriatiOns is called a language. A language is said to be quantifier-free (elementary) if all its elements are quantifier-free (elementary). We say that a variable x i occurs freely in the appropriation (xj § t) if it occurs in t, and it is said to occur freely in a test ((p?) if it occurs freely in cp ; it is said to occur freely in a sequence al,...,a s of tests and appropriations if it occurs freely in al or there exists a j such that I < j ~< s, x i does not occur freely in al,...,aj-l, none of al,...,~j-1 is an appropriation of the form (x i § t), and x i occurs freely in ej; it is said to occur freely in a language if it occurs freely in an element of this language. Let K be a fixed set of languages. For i0 = 0, I and j0 = I, 2, let us define the notion of a formula of the logic L(K, i0, J0). We call a set T of variables recursive if the set {~(x)Ix~T} is recursive. The atomic formulas are formulas of the logic L(K, i0, j0). Let cp be a formula of the logic L(K, i0, J0). If H ~ K , i0=0, ]o----2, T is a recursive set of variables, and H is a quantifier-free languate, then ~ and <}~>~ are formulas of the logic L(K, i0, J0). If H ~ K ~ io=0, ] 0 = I , and H is a quantifier-free language with finite set of free variables, then ~0 is a formula of the logic L(K, i0, j0). If ~K, i0=i, ]0= 2, T is a recursive set of variables, and H is an elementary language, then <~, T>~ and <~[>~ are formulas of the logic L(K, i0, j0). If H ~ K , i0----I, ] 0 = I and H is an elementary language with finite set of free variables, then <~l>~p is a formula of the logic L(K, i0, j0). A variable occurs freely in ~p if either it occurs freely in H or it occurs freely in q0, and there exists a sequence in H, no element of which is an appropriation of the form (xi § t), where x i is the considered variable. A variable occurs freely in <}I, T>q0 if it is not an element of T and occurs freely in cp. If r and ~2 are formulas of the logic L(K, Nz~ are also formulas of the logic L(K, i0, j0). a variable in these formulas is the usual one.

i0, j0), then /k ~,q%, Vcp~q02, 7~j, Vx~q0, ,and The definition of the free occurrence of

The relation o~r of validity of a formula q~ of the logic L(K, i0, j0) on a state o of an algebraic system D for atomic formulas and for formulas of the preceding Paragraph is defined in the usual manner. Let us pass to the definition of o~r and o ~ < H , T>r Let D be an algebraic say that

system of signature ~ and o and ~' be states of the system D. s(x~ +- t ) s '

if o'(x i) = z(x i) for i ~ j and o'(xj) that

is the value of the term t on the state o.

if o' = o and o ~ . Let al ... a s be a finite sequence of tests and appropriations.

if there exist states o~,...,Os- ~ of the system D such that

472

We say that

We say

We

Finally, let d be a state of the system D, H be a set of finite sequences of tests and appropriations, T be a recursive set of variables, and qc be a formula of the logic Lml m. To say that geo ~ and

d ~ q0 if there exist a sequence a ~ and a state o' of the system D such that d~. We say that o ~ < ~ , T>~ if there exists a state ol of the system D such that

r

=

o(x)

for xj~T, o~<~I)(p , and there exists a natural number i such that oy(x k) for arbitrary natural numbers j and k greater than i.

xj, xh~T

for o1(xj)

=

To call an elementary language prenex language if all tests of all its elements have the form ((p?), where @ is a prenex formula. We call a prenex language restricted if there exists a natural number n such that all tests of all its elements have the form (~?), where (~ has at most n changes of quantifiers. In the sequel we will assume that K is a class of recursively enumerable restricted languages, i0 = 0 or i0 = I, j0 = I or j0 = 2. THEOREM 2. For each formula ~ of the logic L(K, i0, j0) with a finite set T~ of free variables there can be constructed a formula ~ of the Belyaev logic such that Tr is the set of free variables of ~ and o ~ is equivalent to o~(~ for each algebraic system D and each state d of the system D. Proof.

Let ~ be a formula of the logic L~I~ that belongs

to A.

It is sufficient

to

construct formulas ~ and ~2 of the logic Lmz~ that belong to A and are such that ~ < ~ [ , T>~ is equivalent to d ~ and o ~ < H > ~ is equivalent to o ~ z for each algebraic system D and each state o of the system D. Here ~I is a fixed language from K and T is a fixed recursive set of variables. In addition, ~ and (H>~, and also ~ and < H , T > $ , must have t h e same free variables. a~H,

Since ~I is restricted, it follows that for each test (p?) that occurs in a sequence we can construct a formula p* of the following form that is equivalent to p:

aa,Va~.., aa~V {A {rl,/] ~ {I . . . . . t,}}le~ {1, ..., t}},

(2)

where q is a fixed odd number, az,...,aq are finite sets of variables, and ~ij is an atomic formula or the negation of an atomic formula. Since ~ is finite, it follows that for a certain fixed r all the so-obtained formulas p' belong to A r for all the tests that occur in the elements of the language H . Let 9.=a~..~(=) and o be a state of the system D. By induction over i we can easily construct a sequence of terms tz,...,tp such that for a i of the form (p?) and for a state o' of the system D, for which oel ... gi_lo', the relations o < ~ p and o~p~ are equivalent, where z~,...,Zp are all the variables that occur freely in p' and pl is obtained from p' by the simultaneous replacement of each free occurrence of zj by the occurrence of tj for j = 1,...,p. It is clear that p~ is equivalent to a formula ~(~, i) of the form (2). If ei is not a test, then as w(a, i) we take an identically valid formula of the form (2), fixed in advance. In the same manner, there exists a sequence of terms that depends only on a such that for a state o' of the system D, for which oao', the relations o ' ~ : and d ~ ( = ) are equivalent, where uz(a) is obtained from ~ by the simultaneous replacement of each free occurrence of a variable by the occurrence of the term of the sequence corresponding to this variable. Therefore, d~<{~}>~ is equivalent to

(~ I::: A (u,(~), a(c,, ~;)l~= i . . . . .

s(a)}.

If T is finite, then we let ~2(a, T, j) be ~l(a), and if T is infinite, then we let be the least of those k > j for which x k occurs in T, and ~2(~, T, j) is obtained from ~l(a) by replacing each free occurrence of x ~ T for k > I by the occurrence of Xl, and a(~, j) is the finite set of the variables that occur freely in T and in case of the formulas

~..(cz, T, j), a(cz, 1) . . . . , g((z, s(o~)). It is clear that

s~V where r(e) k>/.

is H e

o~<~[,

T>~:,

is equivalent

to

(~a((z, j) A{n~(a, T , j ) , a ( ~ , i ) I i = t , . , . , s ( c c ) } l ~ H ; least l such that x k does not occur in ~(a,

j = r ( a ) , r(~)+] . . . . }, i) for any i = 1,...,s(a)

(3)

for

473

It is also clear that

o~~

is equivalent to

oI=V{A{~Jr

~(a, i ) l i , = t . . . . . s(a)}la~}.

(4)

Since H is recursively enumerable, ~l(~) is effectively computed with respect to a and 4, and ~(a, i) has the form (2), it follows that the formulas on the right-hand side of the sign of validity in (3) and (4) can be taken as 41 and ~2. The theorem is proved. We say that a logic L' is weaker than a logic L" if for each formula ~ with a finite number of free variables of the logic L' there exists a formula 4 with the same number of free variables of the logic L" such that for each infinite algebraic system D and each state o of this system, the relation o~cp is equivalent to o ~ . If L' is weaker than L" and L" is weaker than L', then we say that L' and L" are equivalent. Let us denote the Belyaev logic by BL. COROLLARY.

Every logic L(K, i0, j0) is weaker than the logic BL.

There arise the problems of interrelationship of the logics L(K, i0, j0) and BL for various K, i0, and j0. We call these problems the ffarel problems. To formulate certain Harel problems, we agree about some additional notation. By RE we will denote the class of all recursively enumerable restricted languages. If each language H from K is a set of sequences of tests and appropriations, taken from a certain finite list of tests and appropriations, fixed for a given language, then L(K, i0, I) coincides with L(K, i0, 2) for i0 = 0 and i0 = I. In these cases we will wrile L(K, i0) in place of L(K, i0, j0). The classes RG of the regular languages, RD of regular deterministic languages, and CF of context-free languages are examples of these classes K. Let us recall definitions. A language is said to be regular if there exists a finite list E of tests and appropriations such that the considered language is a regular set in the alphabet E. A regular language is said to be deterministic if it has one element and is either concatenation of two regular deterministic languages or is the union of two regular deterministic languages and, in addition, all sequences of the first languages begin with the test (~?) and those of the second languages with the test (-]~?), or is the iteration of a language, all sequences of which begin with the test (~?) and is concatenated with the one-element language that consists of the test (-]~?).. A language H is said to be context-free if there exist a context-free grammar G, the set of whose terminals is a finite set of tests and appropriations such that G generates Harel has asked whether L(RG, i0) and L(PD, i0)? are equivalent. A negative answer to both these questions is contained in [6]. The natural question whether L(PD, i0, I) and L(KC, i0) are equivalent got a negative answer in [7]. However, at present my information about the interrelation of the logics L(K, i0, j0) is almost confined to this. For example, the questions whether L(KC, i 0 ) a n d L(RG, i0) are equivalent is open. In conclusion, let us observe that we can extend the hierarchy of the logics L(K, i, j0) to i = 2, 3,..., assuming that <~>~ is a formula of the logic L(K, i + ~, j0) if ~ is a formula of this logic, H ~ K , and H contains only a finite number of free variables for j0 = I and all tests in the elements of ~I have the form (~?), where ~ is a formula of the logic L(K, i, j0). We can also introduce a restriction on the tests in the elements of such that L(K, i, j0) is weaker than BL. We obtain another hierarchy if we begin with i = I. If the logics of this new hierarchy are denoted by L'(K, i, j0), then it is clear that L(K, i, j0) is weaker than L'(K, i, j0). The problem about the interrelation of the logics of these two hierarches arises, e.g., for what K are these hierarchies stabilized? 3.

FUNDAMENTAL THEOREMS

As usual, in place of =xy we will write x = y, in place of ~ = z U and in place of A ~ 2 and V~I~2 we will write (~iA~2) and (~iV~), THEOREM 3.

we will write x ~ y, respectively.

L(RG, i0, 2) is equivalent to BL for io = 0, I.

Proof. By the corollary of Theorem 2, it is sufficient to prove that BL is weaker than L(RG, i0, 2). Since L(RG, O, 2) is weaker than L(RG, I, 2), it is sufficient to prove that BL is weaker than L(RG, 0, 2). Let q01 be a formula of special form of BL. By Theorem I, it is sufficient to construct for ~ a formula 41 from L(RG, 0, 2) such that for each infinite algebraic system D and each state o of the system D the relations o~cp~ and o ~ i are equivalent. To avoid repetition,

474

we will use the notation logic. Let T i be

from the definition

of a formula of special form of the Be!yaev

{x,~, x,~+~, x ~ _ ~ l m = s + 4i + 41k; n = s + 2i + 2Ik; l = 1 , 2

Let

~I(~,~, u~)

denote

{(((a,=x.,A

. . . . }.

the language

a~=xm+,)A

]=t,...,1}))?)lm=s+4i+4lk;

(A{x~-x=+~ln=s+2i;

1=t,

2 . . . . }.

Let us replace in qo~+i each subformula of the form Hiulu2 by <~I(i,ul, ~)>xi=x~ for i = I,..., k. We get the formula q0h+~. Let r be already constructed. If q0{ is N{xj}q~{+i or u • %+~ , then (p* is ~{xjq0i*+1or Vxj%0*+1, respectively. If % is V { E a ~ (qvi+1)z]/----0,i.... ] or

A {Va ((P~+1)zif:

0,1 .... }, then

q0~

is

<}{i,Ti>(pi+1 or

7<~li, T~> ~ T~+I, respectively,

where

~I~

is {((x~+~ # x~+~+~ A x~+~ = x.+~+m)?)17 = 2, 3 . . . . }.

If xl occurs freely in (p~, then as ~l w e take TI and, in the contrary case, as ~l we take ~xlq0I. It is obvious that this }i works. The theorem is proved. Theorem 3 cannot be strengthened THEOREM 4.

L(RG,

by replacing L(RG,

I, I) is not equivalent

i, 2) by L(RG, i, i).

to BL.

Proof. We consider the class IO of complete torsion-free Abelian groups as systems of the signature <+, 0>. We can consider each such group as a vector space over the field of rational numbers. Let us consider a denumerable group G from IO that is an infinitedimensional space and also the class IOf of all those groups from IO, which are finitedimensional spaces. The formula of the Belyaev logic that asserts the existence of a finite number of elements such that each element is a linear combination of them is valid in all groups from }OF, but is false in G. Now, we show that each formula from L(RG, I, I) that is valid in each group from IOF is valid in G also. Since each elementary formula is equivalent in the theory of the Class lO to a quantifier-free formula, each elementary test can be replaced by a quantifier-free test, and for each formula of the logic L(RG, I, I) we can construct a formula of the logic L(P~, 0, I) that is equivalent to it on each system from 10. Now let qP be a formula of the logic L(PH, 0, I) that does not contain free variables, but contains n quantifiers. Let q~ be valid in G. We show that (p is valid in each system from IOf, whose dimension exceeds n. The proof, given here, follows a well-known scheme and this fact is well known even in a more general situation. By induction over the number of quantifiers in a formula ~; we will prove that if ~ contains n quantifiers and ~:~ § ~ is a local isomorphism of G into a system G~IOF, and the dimension of GI exceeds the dimension of the subspace generated by b by more than n, then the validity of 9($) in G is equivalent to the validity ~(b) in G~. Here 9 is a formula of the logic_L(RG, 0, I), all free variables of which are contained among vl,...,Vm, ~ = < ~ , . . . , ~m >, and b = . If ~b does not contain any quantifier, then the assertion is obvious. The induction step is reduced to the case where ~ has the form (~u,~+,)~. Selecting an element ~m+~ in G such that the formula ~ is valid on the set < ~ , ' ' - , ~ m , ~m +~> in G, we find an element bm+ ~ in G such that the mapping that transforms ~m+~ into bm+~ and is an extension of @ is a local isomorphism of G into G~. By the induction hypothesis, ~(b~,...,bm, bm+~) is valid in Gz. In the same manner, it can be proved that the validity of 9(b) in G1 implies the validity of ~(~) in G. The theorem is proved. LITERATURE I .

2.

3.

4.

CITED

J. Barwise, Admissible Sets and Structures. An Approach to Definability Theory, Springer-Verlag, Berlin--New York (1975). S. S. Magazov, "On fragments of finite rank," in" Matematika: Abstracts of the Reports of =the Seventh Kazakh Interc:ollege Scier~tific Conference on Mathematics and Mechanics [in Russian], Karaganda Univ. (1981), p. 136. V. Ya. Pelyaev and M. A. Taitslin, "On elementary properties of existentially closed systems," Usp. Mat. Nauk, 34, No. 2, 39-94 (1979). D. Harel, Logics of Programs: Axiomatics and Descriptive Power, MIT. Lab. Comput. Sci. Tech. Report, No. 200, 1978. 475

5. 6.

7.

D. Harel, First-Order Dynamic Logic, Springer-Verlag, Berlin--New York (1979). E . A . Boyarskaya, N. N. Repin, and M. A. Taitslin, "A determinate dynamic logic that is weaker than the dynamic logic," in: Questions of the Theory of Algebraic Systems [in Russian], Karaganda Univ. (1981), pp. 20-31. M . M . Erimbetov, "On the expressive power of program logics," in: Investigations in Theoretical Programming [in Russian], Kazakhsk. Univ., Alma-Ata (1981), pp. 49-68.

MAPPINGS THAT QUASIPRESERVE

CONES

D. A. Trotsenko

UDC 513.75+517.54

I.

INTRODUCTION

The theorems on affineness of a mapping that transforms a family of cones into another family of cones play a fundamental role in chronogeometry. The initial theorem without the condition of continuity of the mapping was proved by Aleksandrov and Ovchinnikov [I]; in the sequel the requirements on the families of cones were much reduced (e.g., [2-4]). The main idea of the proofs, due to Aleksandrov, consists in obtaining a sufficiently "rich" family of straight lines, obtained as the intersection of cones in the domain and in the range. This idea does not enable us to "loosen," weaken, the conditions on the mappings in order to obtain a contensive class of mappings that are similar, in some sense, to affine mappings. Let A and A' denote affine spaces of same finite dimension n. In all previous works, some of the following conditions were essential for the mapping f:A § A': I) f is an injective mapping 2) the cones of the family

of A onto A',

in the domain and the range are strictly convex,

3) the dimension of spaces n ~ 3. The following simple example shows that these conditions are essential: f(xl,...,x n) = (fl(xl),...,fn(xn)), where the functions fi are monotone. If fi are strictly monotonically increasing continuous functions that map a straight line onto a straight line, then for all Y = (Yl,...,Yn) the cones {x f x i ~ Yi, i = 1,...,n} are mapped onto the cones {x'Fx~ ~ fi • (Yi)}In the case n ~ 3, these cones are not strictly convex. In the present article we drop the conditions I)-3) entirely. Instead of them, we introduce two families of cones in the domain and in the range. These cones must satisfy quite weak conditions (2.1)-(2.4), allowing the cones to consist of, e,g., a finite number of rays. The conditions (2.5)-(2.6) on the mapping are also substantially weaker than the previous conditions and require neither injectivity nor surjectivity of the mapping. In this article we will study classes of mappings that satisfy (2.5)-(2.6). The main result (Theorem I) is the proof of the quasiconformality of these mappings under the introduction of Euclidean norms in A and A' (and, consequently, of homeomorphicity and of differentiability almost everywhere). Theorem 2 gives a necessary and sufficient condition on cones for affineness and Theorem 3 gives a simple sufficient condition. Their proof is based on the following well-known result: Each conformal mapping of R n into Rn is a similarity. The terms "mappings that quasipreserve cones" and "(~, ~)-QPC" are introduced in Sec. 4 and are used in the case of a mapping of Euclidean spaces with families of right-circular cones. This case describes to a significant degree the case of mappings with arbitrary families of cones and at the same time it is more visual and better amenable to analysis. Theorem 4 gives estimates of the coefficient of conformality of an (~, The stability in the Liouville theorem on conformal mappings of a space [5] prove that the mapping is uniformly approximated on each ball by orthogonal Er, where r is the radius of the ball and ~ = e(~, ~) is small for proximate will not consider this problem here.

B)-QPC mapping. enables us to mappings [up to ~ and ~]. We

Novosibirsk Institute of the National Economy, Novosibirsk. Translated from Sibirskii Matematicheskii Zhurnal, Vol. 24, No. 3, pp. 193-203, May-June, 1983. Original article submitted February 4, 1981.

476

0037-4466/83/2403- 0476507.50

9 ].984 Plenum Publishing

Corporation