On the Decidability of Formulae Involving Continuous and Closed Functions

1 Introduction

Once a decision algorithm has been found for a formal­ ized mathematical theory T, it is rewarding to discover t~at the validity problem for some other theory T*, pos­ sibly related to a different branch of mathematics re­ duces to the validity problem ofT, which one is alr~ady able to solve.

Instances of this are common in the literature. We are therefore motivated in undertaking a quest for new problems whose solution is amenable to 'computable set theory', i.e. to the thick cluster of recently attained methods regarding various portions of classical set the­ ory (~ee [C_antone, 1988] for an extensive bibliography on this subJect). Some indications in this direction have been given in [Cantone et al. , 1987], where the satis­ fiability p~oblems of two theories dealing with mono­ tone functiOns on totally and partially ordered sets have been translated into M LS, or "multi-level syllogistic" ( cf. [Ferro et al., 1980]), a well-known decidable theory.

*Work supported by ENI and ENIDATA within the AXL project .

1 Subject area: B5. Automated deduction.

Eugenio G. Omodeo ENIDATA-Bologna Viale Aldo Moro, 38 40127 Bologna, Italy

Specifically, it was shown there how to reduce to MLS the satisfiability problem for propositional combinations of atoms of type

where f stands for a monotone function.

In the same paper a decision test was provided for the satisfiability problem of an unquantified 'extended Tarski' theory of reals with variables designating contin­ uous real-valued functions , based on Tarski's celebrated result on the real field (see [Tarski, 1951]) . Such theory allows real addition and subtraction, multiplication and division, and comparison between variables representing real numbe~s; also, ad~ition and subtraction of ( contin­ uous) functiOns, functiOn evaluation, positivity, mono­ tonicity and convexity predicates are allowed. More pre­ cisely, a decision test was provided for propositional com­ binations of atoms of the types

where x,y,z are real variables and J , g, h are function variables, and where convex(!, x, y) [resp. concave(!, x, y)] is true if and only if the function f is convex [resp. concave] in the real interval [x, y].

Additionally, an extension of Tarski 's theory with multi-variate continuous functions has been considered in t~e same paper (see [Bledsoe, 1977, Bledsoe, 1984, Rabm, 1969] for other approaches on related problems) .

In this note we give a further application of deci­ sion tests for set theory to theories involving elemen­ tary topological constructs. More specifically, we extend two-level syllogistic [Ferro and Omodeo, 1978] with the Kur~towski topological closure operation -, and with contmu<_>us or closed maps between topological spaces, alon? with the operations of point evaluation, set image, and mverse set image ( cf. [Kelley, 1961]).

We will assume that formulae satisfy a syntactic non­ circularity property (to be specified below).

The language £ 2 · 00 of our topological two-level syl­ logistic has countably infinitely many different sorts of variables, each sort corresponding to a different topo­ logical space. We will distinguish between individual, set, and map variables. Individual variables of a given sort n are supposed to range over the universe of sort n, whereas set variables range over the set of all subsets of the appropriate universe. Finally, each map variable ranges over the collection of continuous or closed maps between two appropriate topological universes.

As in [Ferro and Omodeo, 1978], the language £ 2 · 00 does not allow quantification (either universal or exis­ tential).

In the following section, we will give in detail the syn­ tax and semantics of £ 2 · 00 · Also, we will specify a sub­ class of formulae of £ 2 · 00 for which, in a subsequent sec­ tion, a decision procedure for the satisfiability problem will be produced.

2 Syntax and semantics of £ 2 · 00 · A cyclicity

£ 2 · 00 is a two-level multi-sorted language with func­ tions, containing for each natural number n two denu­ merable sequences of variables, called individual varibl ( (n) (n) (n) (n) ) d . bl a es x 0 ,x 1 , ... ,y 0 ,y 1 , ... , etc. an set varza es (x(n) x<n) y;(n) y(n) t ) th t t o<n) o , 1 , .. · , 0 , 1 , ... , e c. ; e cons an s and 1(n) (designating the empty set and a 'universe', i.e. the support of a topological space); the unary op­ erators '( n), -( n) (designating set complementation and topological closure) . The usual binary set operators U, n, \ (designating union, intersection, and set difference) are also available.

In addition, for each pair (n, m) of natural numbers, there are two denumerable sequences, one consisting of continuous map variables uin,m), f~n,m), .. . ) and one of I d . bl ( (n,m) (n,m) ) c ose map varza es g1 , g2 , . · · ·

Finally, the language £ 2 · 00 contains the usual relators =, E, ~. the propositional connectives ...,, &, V, --+, +-+, and parentheses.

Individual terms and set terms of sort n, for each n, are defined as follows. If t(n) is an individual term of sort n, r}n), Tin) are set terms of sort n, f(m,n), g(n ,m) are a continuous and a closed map variable of type ( m, n) and (n, m) respectively, and h(n,m) stands for a continuous or closed map variable of type (n, m), then Tin) U Tin) , Tfn)nTin), Tfn\Tin), (Tin))', Tin) are set terms of sort n, and h(n ,m)(t(n)), (f(m,n))- 1[Tin)], g(n,m)[Tin)] are set terms of sort m. Each individual variable of sort n is an individual term of sort n. Each set variable of sort n and the constants o<n>, 1 (n) are set terms of sort n .

Formulae of £ 2 · 00 are propositional combination of atoms of the forms

where t~n), t~n) are individual terms of sort n and Tin), Tin) are set terms of sort n, for some natural num­ ber n.

The semantics of the language £ 2 · 00 is defined in the most natural way. So, a topological assignment M is any interpretation of the variables and constants of £ 2 · 00 such that M1(n) is a non-empty set endowed with a topology T(n); MO(n) is the empty set; M :z:(n) is an ele­ ment of M1(n), for each individual variable z(n); M x<n) is a (possibly empty) subset of M1 (n); U, n, \ are interpreted as binary set union, set intersection, and set difference in the space M1(n); t(n) is interpreted as set complementation in M1 (n); -(n) is interpreted as the closure operation within the topological space (M1 (n), T(n)) ; M f(n,m) is a continuous map from the topological space (M1 (n), T(n)) into the topological space (M1(m), T(m)), for each continuous map variable f(n,m) in £ 2· 00 ; Mg(n ,m) is a closed map from (M1(n),T(n)) into (M1 (m), T(m)), for each closed map variable g(n ,m) in £_2,oo .

A formula p of £ 2 · 00 is said to be topologically satisfi­ able if there is a topological assignment M such that pM is true.

p is said to be topologically valid if pM is true for all topological assignments M .

For ease of presentation, we require that all spaces are pairwise disjoint.

To each formula p of £ 2 · 00 , we associate a graph Gp = (Np, Ep), where Np = {io·, i1, ... , iA:} is the set of all sorts of individual and set variables present in the formula p. The edge it '=> ih is in Ep if and only if either p contains some occurrence of a continuous map variable of sort (ih, it), or p contains some occurrence of a closed map variable of sort (it, ih). Then we say that a formula p of £ 2 · 00 is acyclic if its associated graph Gp is acyclic.

Notice that an acyclic formula cannot contain any oc­ currence of map variables of sort (n, n).

In the next section we will give some evidence that the language £ 2 · 00 is quite expressive. In fact , most of the elementary concepts and properties that can be typically found in the first chapters of introductory textbooks on general topology are expressible in £ 2 · 00 (and therefore, as will be shown in the following, automatically verifi­ able).

In the subsequent section, we will sketch a decision procedure tQ solve the satisfiability problem for the sub­ class of acyclic formulae of £ 2 · 00 . By virtue of the acyclicity assumption we will be able to eliminate map constructs quite smoothly. This fact coupled with a tech­ nique for eliminating also the closure operator - will al­ low us to r~duce the satisfiability problem for acyclic £ 2 · 00 -formulae to the problem of testing ordinary satis­ fiability of two-level syllogistic formulae. Therefore our decidability result will follow from [Ferro and Omodeo, 1978].

3 Some examples

Several basic notions of general topology can be formu­ lated in the language £ 2 · 00 . Some operators immediately expressible are:

• Int(A) =oer (A')' (the interior of A);
• Ext(A) =oer Int(A') (the exterior of A);
• a( A) =:oer A\ Int(A) (the boundary of A).

Also, the following topological predicates are expressible in the language £ 2 · 00 :

• open(A) =oef A= Int(A) (A is an open set);
• closed(A) =oef A= A (A is a closed set);
• open_domain(A) =oef A = Int(A) (A is an open domain; see [Kuratowski, 1922]);
• neighborhood( A, a) =oef a E Int(A) (A is a neigh­ borhood of a);
• dense(A) :=oef A= 1 (A is dense in the space 1);
• co_dense(A) =oef dense(A') (A is co_dense in the space 1);
• nowhere_dense(A) =Def co-dense(A) (A is nowhere-dense in the space 1).

Observe that, in general, for each formula <f>(xt, ... , xn) with free variables x 1 , . . . , Xn, the following are equivalent

• ¢(x1, ... , xn) is satisfiable;
• (3x1) ... (3xn)<f>(x1, ... , Xn) is valid;
• -{v'x1) ... (Vxn)-,<f>(xt, ... , Xn) is valid.

Therefore, any satisfiability test for an unquantified the­ ory T closed with respect to negation provides a validity test for the universal and the existential closures of the formulae in T.

Since the class of acyclic formulae of £ 2 · 00 is closed under negation, it follows that the validity of the follow­ ing statements can be recognized by a satisfiability test for acyclic formulae of £ 2 · 00 :

• (a) the intersection of two open domains is an open do­ mam;
• (b) the union of two open domains need not be an open domain;
• (c) if A and Bare open domains, then

• (d) 0 0 , and for all A and B

( K uratowski 's closure axioms);

• (e) if A is co-dense and B is nowhere dense, then AU B is co-dense;
• (f) the union of two co-dense sets is not necessarily a co-dense set;
• (g) for all subsets A of a topological space U,

• (h) for each continuous map f and each set B,

• (i) for all A,

• (j) every continuous map is locally continuous, i.e., for all x, if B is a neighborhood off( x), then J- 1 [ B] is a neighborhood of x.

It will turn out that the decision test to be described in the next section is "constructive", in the sense that whenever a formula is recognized satisfiable, a model for it can be effectively constructed. In other words, our test can provide counter-examples for unvalid universal formulae. So, for instance, in the case of statement (b) above, our procedure besides proving its validity, can actually exhibit a topological space with two open do­ mains whose union is not an open domain. Analogously for statement (f).

4 The decision method

Given any acyclic formula p, we can assume without loss of generality that (a) the set Np = {i1 , i2 , ... , ik} of all sorts of individual and set variables occurring in p coincides with {1,2, . . . ,k}; (b) if the edge i:::} j is in Gp, then i < j.

In addition, by using a simple normalization proce­ dure, it is easy to see that the problem of topological satisfiability for acyclic formulae of £ 2 · 00 can be reduced to the problem of testing for topological satisfiability acyclic conjunctions of literals of type

where x, y stand for individual variables, f and g for a continuous and a closed map variable respectively, and X, Y for set variables. In fact, for example, terms of type T' and T1 nT2 can be replaced by 1\ T and T1 \ (T1 \T2), respectively.

Any acyclic conjunction of literals of type (1) satisfy­ ing properties (a) and (b) above is called a normalized acyclic formula.

We describe an effective procedure that given a nor­ malized acyClic formula p of £ 2 · 00 produces a formula p** in the multi-sorted sublanguage .C** of £ 2 · 00 in which nei­ ther map terms of type h(t), f- 1 [11, g[T], nor topological terms of type T can occur and such that pis topologically satisfiable if and only if p** is (topologically) satisfiable.

Let p be a normalized acyclic formula of £ 2 · 00 and let k be the largest sort of any variable in p (i.e., Np = {1,2, ... ,k}).

Below is the procedure for eliminating map and topo­ logical terms from p. (Throughout the following proce­ dure, calligraphic capital letters are used to denote sets of variables or sets of sets of variables.)

ELIMINATION PROCEDURE

1. Initialize q to the empty conjunction.
2. Initialize CLOSED(i) to the empty set, for each i = 1, ... ' k.
3. FOR i = 1 TO k DO
4. LetiV(i) be the collection of set variables of sort i present in p and in the auxiliary conjunction q.

1. For each S(i) ~ Pow(V(i)), introduce a brand new set variable C~) (of sort i); also, for each X(i) in v<i) introduce the shorthand notation

(K~) is intended to denote the closure of X(i), whereas the c~) 's will be the closed sets of the topology over 1 (i).)

1. For each S(i) ~ Pow(V(i)) add to q the formula

where, if Q = 0, UxeQ K~) stands for the con­ stant Q(i) and, if S(i) = 0, the right-hand side stands for the constant 1 (i).

1. For each X(i) in V(i) add to q the formula

1. For each X(i) in V(i) and S(i) ~ Pow(V(i)) add to q the formula

1. Put

and

1. For each Q(i) C W(i) introduce a brand new set variable pg) ~ sort i (Pg) is intended to rep­ resent a region of the Venn diagram associated with W(i), as expressed by the following three formulae) .
2. For all Qii) , Q~i) ~ W(i), Qii) f. Q~i), add to q the formula

1. For all w<i) in W(i) add to q the formula

1. For each S(i) ~ Pow(V(i)) add to q the formula

where, if there is no Q ~ W(i) such that (VQ1 E S)(3X E Ql)(Kx E Q), the right-hand side stands for the constant Q(i). (In view of 3.8 and 3.9, this formula is equivalent to 3.3.)

1. For each X(i) in CLOSED(i), add to q the for­ mula

(See comment to step 3.2; see also steps 3.16, 3.19 below.)

1. For each Q(i) ~ W(i) and each continuous map variable f(j,i) of sort (j, i) in p (with j > i) introduce a brand new set variable Pg.~ of sort j and add to q the formula

(Pg,~ will stand for the set term (/(j ,i))(- 1 )[pg)], as expressed by the following three formulae).

1. For each Qii), Q~i) ~ W(i), Qii) f. Q~i), and each continuous map variable f(j,i) of sort (j, i) add to q the formula

1. For each w<i) in W(i) and each continuous map variable f(j ,i) of sort (j, i) in p introduce a brand new set variable wjj) of sort j and add to q the formula

(Wjj) will stand for the set term uu ,i))< -1 )[w<i)]).

1. For each continuous map variable f(i ,i) of sort (j, i) in p add to q the formula

1. For each S(i) ~ Pow(V(i)) and each continuous map variable f(j ,i) of sort (j, i) in p introduce a brand new set variable cCJ,j of sort j and add to q the formula

where, if there is no Q ~ W(i) such that ('v'Q1 E S)(3X E Q1)(Kx E Q), the right-hand side stands for the constant oU). Also, add cCJ,j to CLOSED(j).

rc<j) will stand for the set term S,J uu ,i))< -1)[ c~i)l.J

1. For each Q(i) ~ W(i) and each closed map vari­ able g(i,j) of sort (i,j) in p (with j > i) introduce a brand new set variable Pg,~ of sort j and add to q the formula

(Pg,~ will stand for the set term g(i.i)[pg)]).

1. For each W(i) in W(i) and each closed map vari­ able g(i ,j) of sort ( i, j) in p introduce a brand

new set variable wJn of sort j and add to q the formula

(WJi) will stand for the set term g(i,i)[WCi)]).

1. For each S(i) ~ Pow(V(i)) and each closed map variable g(i,j) of sort ( i, j) in p introduce a brand new set variable c.¥.~ of sort j and add to q the formula

where, if there is no Q ~ W(i) such that (VQ1 E S)(3X E Q1)(Kx E Q), the right-hand side stands for the constant O(j). Also, add c.¥_~ to CLOSED(j).

(c_¥,~ will stand for the set term (gCi,i))[C~)].J

1. END FOR.
2. For each literal yU) = g(i,i)(xCi)) in p and each Q ~ W(i), 1 ~ i < j ~ k, add to q the formula

1. For each literal y(i) = f(i,i)(xCi)) in p and each Q ~ W(i), 1 ~ i < j ~ k, add to q the formula

1. For each pair of literals y~i) = h(i,j)(xii)), y~i) = h(i,i)(x~i)) in p, with h(i,j) a continuous or closed map variable, 1 ~ i, j ~ k, add to q the formula

1. Let p* be obtained from p by substituting

and by dropping from pall literals of type y = h(x), with x, y individual variables and h a map variable.

1. Let p** be the conjunction p* & q.
2. Return p**.

Our satisfiability result is an immediate consequence of the following lemmas.

LEMMA 4.1 p is topologically satisfiable if and only if p** is satisfiable.

Proof. Clearly, any topological model M for p can be naturally extended to an ordinary model M** for p**, by putting, for instance,

etc ..

At this point, it is an easy matter to thow that M** is indeed a model for p**.

Conversely, given a model M** for p**, we can assume that

for all Q ~ W(i) and for all closed map variables g(i,i) of sort ( i, j) occurring in p, 1 ~ i < j ~ k (otherwise a suitable "enlargement" procedure could be used to force (2)).

By (2), one can then define M**g(i,i) as any map G from M**1 (i) into M**1 (i) such that

for all Q(i) C W(i).

Likewise, M** f(i,j) can be defined as any map F from M**1 (i) into M**1 (j) such that

for all Q(i) ~ w<n.

In addition, it can easily be verified that

is a topology over M**1 (i), for 1 ~ i ~ k.

By inspecting the Elimination Procedure, it is easy to see that the assignment M** so extended is a topological model for p. For instance, if X(i) = Y(i) is a literal in p, then by step 8 of the Elimination Procedure, p* contains the literal X(i) = K~). Hence, Af** xCi) = M** K(i) and since M** J((i) - M**C(i) is closed y ' y - {{Y}} ' one only needs to show that if M**Y(i) ~ M**C~) then M** X(i) ~ M**C~i), for all S(i) ~ Pow(V(i)) . But this follows at once from clauses added to q at step 3.5 of the Elimination Procedure.

This concludes the proof of the lemma.

·

So far, the topological satisfiability problem for the class of acyclic formulae of £ 2 · 00 has been reduced to the ordinary satisfiability problem for the class of for­ mulae in the sublanguage £**. To further reduce this latter problem to the satisfiability of the two-level syllo­ gistic language (2LS in short) considered in [Ferro and Omodeo, 1978], the following simple procedure can be used 1 .

Let p** be a formula of £** and assume that p** in­ volves individual and set variables of sorts in { 1, 2, ... , k} only. Let 1 and 0 be the constants of 2LS language (de­ noting the universe and the empty set, respectively) .

• 1'. For each 1 ~ i ~ k, introduce a brand new 2LS set variable U; (which will denote the constant 1 (i)) .
• 2'. For each set variable X(i) [resp. individual variable x(i)] of sort i in p**, introduce a brand new 2LS set [resp. individual] variable X; [resp. x;] of 2LS.

1 see also [Cantone et al., 1989] for a reduction of the satis­ fiability problem for 2LS to the same problem for the multi­ level syllogistic language MLS.

• 3'. Let p be the 2LS-formula resulting by substituting in p··

each occurrence of 1 < i) by Ui, for 1 $ i $ k,

each occurrence of O(i) by 0, for 1 $ i $ k, each occurrence of x<i) by xi, for 1 $ i $ k, each occurrence of z(i) by Zi, for 1 $ i $ k,

and by adding the conjunctions

(which expresses that the universes Ui's are non­ empty and pairwise disjoint) and

(which expresses that the variables Xi and Zi are of sort i, 1 $ i $ k ).

Then we have

LEMMA 4.2 p** is satisfiable if and only if p is satis­ fiable . 0

Thus, by [Ferro and Omodeo, 1978], we obtain

THEOREM 4.3 The class of acyclic formulae in the language .C 2 · 00 has a solvable satisfiability problem. 0

Slight modifications of the Elimination Procedure al­ low one to add the map predicates injective and surjec­ tive, without disrupting the decidability of the satisfia­ bility problem for acyclic formulae.

Facing slightly harder technicalities, one could also al­ low in the language .C 2 · 00 the predicate

"z is an accumulation point of X"

and the operator Der(X) (where Der(X) stands for the set of all accumulation points of X, i.e. the derived set of X) without undermining decidability.

An interesting open problem is if one could relax the requirement of acyclicity, without losing decidability.

Acknowledgements

We are indebted with M. Breban (Yeshiva University), who first treated, in 1980, two-level syllogistic with the Kuratowski topological closure operator. Also, we wish to thank an anonymous referee for his/h~r comments.