v

Meseguer's general logics try to give an answer to the question of what is a logic? using ideas from abstract model theory and category theory [3]. This is achieved by extending further Dana Scott's definition of entailment system and combining it with institutions of Goguen and Burstall [1]. All the fundamental components of a logic like those of syntax, entailment system, models, proof calculus and satisfaction are properly treated in general logics. Our approach analyses general logic’s proof calculi using trees and is based on the result that any graph is the homeomorphic image of a tree. The only well known proof of this result makes use of topology and universal covering spaces [4]. This leads to the main result of the paper in which we prove the existence of universal coverings in the category of Meseguer general logic.

We follow J. Lambek and P. Scott [2] in their treatment of logical deduction. According to this, sentences are objects and deductions are arrows in a category. This approach is rather syntactical than semantical, is independent from logical valuations and is compatible with Meseguer's general logics.

Deduction can be treated in terms of graphs and categories according to Lambek and Scott. The objects of any graph can be considered as formulas while the arrows can be considered as deductions or proofs. The associative law in categories can be considered as a rule of inference.

A deductive system is a graph in which to each object A is associated an arrow 1_a: A ® A, the identity arrow, and to each pair of arrows f: A ® B and g: B ® C is associated an arrow gf: A ® C, the composition of f with g. A category then , is a deductive system in which the following equations hold, for all f: A ® B, g: B ® C and h: C ® D:

General logics try to provide a very general framework for defining already developed logics including many sorted equational, first and second order logic, modal logics etc.

Meseguer's general logics try to give an answer to the question of «what is a logic?» ,using ideas from abstract model theory and category theory [3]. This is achieved by extending further Dana Scott's definition of entailment system and combining it with institutions of Goguen and Burstall [1]. All the fundamental components of a logic like those of syntax, entailment system, models, proof calculus and satisfaction are included in the definition of a (general) logic. General logics try to provide a very general framework for defining already developed logics including many sorted equational, first and second order logic, modal logics etc.

Entailment systems is a categorical formalization of the broad concept of (syntactical) Logical context for theories . It relevance with the Information science is that it can be used to formulate various requirement and specification systems for the development of software of many different information systems . The entailment system approach is invariant of the choice of initial concepts (called signatures ) and of the way the propositions are composed ( category of sentences ) .

Definition An entailment system is a triple E = (Sign, sen, ÃÄ ) such that

sen: Sign ®Set is a functor associating to each signature S a corresponding set of S - sentences, and

ÃÄ is a function associating to each S Î |Sign| a binary relation ÃÄ _S Í P (sen(S)) ´sen(S) called S - entailment such that the following properties are satisfied:

3. transitivity: if G ÃÄ _S f_i for all i Î I, and G È { f_i | i ÎI} ÃÄ _S y, then

.The category deductive system of an entailment system and an entailment system of a Deductive system

(and by R_ÃÄ(D(E)) the entailement relation defined by a deduction system: We put

AÃÄ a iff there is an arrow for some xÎA .The A is a set of sentences of the deductive system D(E) .

Institutions is somehow a complementary approach relative to the entailement systems in the sense that it formulates categorically the concept of semantical (model theoretic ) Logical context for theories .

Definition An institution is a 4-tuple I = (Sign, sen, Mod, ÆÍ) such that

sen: Sign ® Set is a functor associating to each signature S a set of S-sentences,

Mod: Sign ®Cat^op is a functor that gives for each signature S a category whose objects are called S-models, and

Putting together both the categorical formulation of syntactical and semantical (model theoretic ) Logical context ,namely entailement systems and institutions we get the categorical formulation of Logical context or general Logic :

Definition A logic is a 5-tuple L = (Sign, sen, Mod, ÃÄ ,ÆÍ ) such that:

and the following soundness condition is satisfied: for any S Î|Sign|, G Í sen(S), and f Îsen(S),

where, by definition, the relation G ÆÍ_Sf holds if and only if M ÆÍ_Sfholds for any model M that satisfies all the sentences in G.

Definition Given two entailment systems E = (Sign, sen, ÃÄ ) and E' = (Sign', sen', ÃÄ' ), a map of entailment systems (F, a) : E ® E' consists of a natural tranformation a: sen Þ sen' o F and an a - sensible functor F: Th₀® Th₀'satifying the following property:

Every category C determines a graph UC that has the same objects and arrows as the category. Every functor F: C ® C' is also a morphism UF: UC ® UC' between the corresponding graphs. Using the above we can define the forgetful functor U: Cat ® Grph, from small categories to small graphs.

Let O be a fixed set. An O - graph G is a graph with O as its set of objects. Any O-graph G may be used to generate a category C on O. The arrows of this category will be the strings of composable arrows of G, so that an arrow of C from b to a may be pictured as a path from b to a consisting of succesive edges of G. This category C will be written C = C(G) and is called the free category generated by the graph G.

In the previous definition the concept of graph is actually that of the oriented graph.If we want the concepts of non-oriented praph then we defined it as following :

Definition A non-oriented graph H consists of a set X=vertH ,a set Y=egdeH and two maps Y®XxX y®(o(y),t(y)) (o(y) for origin of y and t(y) for terminal of y) and Y®Y y® which satisfy the following condition: for each yÎY we have , y¹and o(y)=t().

We remark that although we define the set of edges as oriented edges (arrows) as we give always each edge with both directions the result is the non-oriented graph the definition .

Given an (oriented graph) it is always possible to add with every oriented edge (arrow) the one with oposite direction and to get the definition of non-oriented graph as before .This non-oriented graph we call non-oriented version (or corresponding non-oriented ) of the given graph .

For the definitions of the previous terms see [9 Munkres] pp 155 ,pp 161,pp 393.

Except of the basic concept of the topological space we require also the concepts of covering map ,covering space ,homotopy and fundamental group .

Given a topological space X , a path in X from x to y is a continuous map f:[a,b] ®X of some closed real interval into X ,such that f(a)=x and f(b)=y .A space X is said to be path connected if every pair of points of X can be joined by a path in X .

If f is a path in X from x to y ,and g is a path in X from y to z we define the composition f*g of f and g to be the path h given by the equations

Definition Let X be a space ; let x_obe a point of X .A path in X that begins and ends at x_ois called loop based at x_o. The set of path homotopy classes of loops based at x_o,with the operation * (of composition of representatives of homotopic classes paths ,[f]*[g]=[f*g] ) , is called the fundamental group ( or first homotopy group ) of X relative to the base point x_oIt is denoted by p₁(X, x_o) .

For a detailed definition of the fundamental group see again the same book [Munkress] pp 326.

We shall not enlarge on the definition of a path homotopy class but we shall mention that an honotopy transformation of a path is a continuous transformation of it that fixes the end points and is realizable in a continuous way inside the topological space.

Definition A space X is said to be simply connected if it is path-connected space (that is any two points can be connected with a continuous path ) and if p₁(X, x_o) is the trivial (one-element) group for some x_oÎX ,and hence for every x_oÎX .

A topological space B is said to be semilocally path connected if every point b of B has a neighborhood V such that the homomorphism of p₁(V,b) into p₁(B,b) induced by inclusion is trivial.

A topological space B is said to be locally path connected at x if for every neighborhood U of x ,there is a path-connected neighborhood V of x contained in U .If B is locally path connected at each of its points ,then it is said to be locally path connected .

For a detailed definition of covering map and universal covering space see [Munkress] pp 331 and 341.

Definition .Let p: E®B be a continuous surjective map. The open set U of B is said to be evenly covered by p if the inverse image p^-1(U) can be written as the union of disjoint open sets V_a in E such that for each a , the restricion of p to V_a onto U is an homeomorphism .The collection { V_a } will be called a partition of p^-1(U) into slices .If any point b of B has a neighborhood U that is evenly covered by p ,then p is called a covering map , and E is said to be a covering space of B .If E is a simply connected space and p is a covering map ,then we say that E is a universal covering space of B .

If B has a universal covering space E ,then E is uniquely determined up to homeomorphism (provided B is locally path connected ) .The reason we call E universal covering space is because it covers every other path-connected covering space of B. (see[Munkress] pp 342 excersise 12* ,theorems (b),(c) ).

A sufficient condition for the existence of universal covering space is given by the next theorem (see [Munkress] pp 303 ,theorem 14.4.

Theorem Let B be path connected ,locally path connected ,and semilocally simply connected .Let b₀ ÎB .Given a subgroup H of p₁(B,b₀) ,there exists a path connected covering space p:E®B and a point e₀ Î p^-1(b₀) such that the induced homomorphism p_* of the fundamental groups by the covering map ,gives p_*( p₁(B,b₀))=H .In particular B has a universal covering space(H={1}).

We sate also a basic result of «lifting» continuous function from a space to a covering space of it .

Definition Let p:E®B be a map .If f is a cintinuous mapping of some space X into B ,a lifting of f is a map :X®E such that p°=f .

Theorem Let p:E®B be a covering map ; let p(e₀) =b₀. Let f and g be two paths in B from b₀to ; b₁let and be their liftings to paths in E begining at e₀. If f and g are homotopic ,then and end at the same point of E and are homotopic .

In this paragraph we try to make formal an intuitive fact of which are aware many workers in the software engineering that «Any flow-graph or chart or petri-net of a program can be untied to a tree». It seems that there is more than one approach to this. One is purely algebraic associates flow-charts to groups and makes use of the fact that any group is the quotient of a free group The other is purely topological . We prefer the topological one ([4] pp. 14, 28).

Definition An non-oriented tree is a non-oriented graph without circles (or loops ) .A disjointunion of non-oriented trees is called non-oriented forest .

Let a non - oriented graph G with vertices X=vertG and edges Y=edgeG. That is we form the topological space T which is the disjoint union of X and Yx[0,1], where X and Y are provided with the discrete topology and the [0,1] has the topology of the real interval .Let R be the equivalence relation on T for which (y,t)= (, 1-t) ,(y,1)=t(y) for y in Y and t in [0,1] .By is denoted the edge y with the inverse direction .The quotient space real(G)=T/R is called the (topological) realization of the graph G.

Let a connected graph G . It is not difficult to prove that real(G) is path connected, locally path connected and semilocally simply connected topological space.

Lemma Let a connected graph G .This in particular means that any two vertices can be joint with a path (sequence of consecutive arrows ) It holds that real(G) is path connected, locally path connected and semilocally simply connected topological space.

Corollary 3.4.The realization real(G) of any connected non-oriented graph G has a universal covering space which is the realization real(T) of a non-oriented tree T. The realization real(G) of any non-oriented graph G has a universal covering space which is the realization real(T) of a non-oriented forest T.

The universal covering of real(G), let us denote it by , is simply connected ,path connected .It holds that there is a graph T such that real(T)= .By the lifting theorem all branches of real(G) (that are compacts arcs actulally ) are lifted as arcs in . By the covering mapping property each branche is lifted in to a disjoint set of arcs in . Any loop or cycle of the graph G is lifted to an infinite set of arcs that make a path infinite in both directions like consequtive intervals in a infinite line (the universal covring space of a circle is the infinite line ).Any point and any neighbourhood of belongs to these arcs .The set of these arcs makes a (possibly infinite ) graph T ,that is homomorphically mapped on G and real(T)= (this is also assured by noting that real (T) is a simply connected covering space of real (G) and using the uniquness of the universal covering space ).As is simply connected and path connected so is real(T) and the graph T .Thus T is a non-oriented tree .

If the graph is non-connected we apply the previous procedure to each connected component of it and we get the correspoonding assertion for the universal covering forests QED.

Definition 3.5 : A morphism of non-oriented graphs from T ,to H such that the induced continuous map on the realization of the graphs is also a topological covering map is called covering map of the graphs. The graph T is said to cover the graph H or that the T is a covering graph of H.

Definition 3.6 The non-oriented tree T of a connected non-oriented graph G defined by the universal covering space of real(G) we call universal covering tree of the graph.

If the graph is not connected then we apply the above procedure to each one of its connected components and the graph T is the disjoint union of non-oriened trees in other words the universal covering forest of the graph G .

Theorem 3.7. A universal covering tree of a graph G, covers any other covering graph of G.

Remark The flow-charts or flow petri-nets of programs are finite connected graphs with two pointed vertices called beginning and end and with all braches oriented .If any loop of the graph is transversed say only once then any maximal path (of monotone orientation ) has first vertice the beginning and the last the end.In particular any arrow (oriented branche )is contained in such a path. We shall call such graphs programs flow-chart graphs. If to any arrow is drawn say a square in the middle of it while every vertice a circle then it may very well be called program flow , petri-net .

Finally we remark that any morphism of graphs f:G®H defines a continuous function

in the obvious way (the correspondence of two branches defines an homeomorphism of two real open intervals ) .We call the mapping the topological morphism extracted by the graph morphism .

Definition An (oriented ) tree T is a graph such that its corresponding non-oriented graph is a is a non-oriented tree .An (oriented) forest is the disjoint union of a set of (oriented) trees .

Remark .The algebraic technique to lift or «untie» program flow-chart graphs to trees corresponds to any program flow-chart graph a ring- polynomial (called path generated function ) and vice versa. The ring polynomial to which is lifted in the free ring the polynomial of program flow-chart graph corresponds to a tree that we call the computation tree of the program flow-chart graph. The two techniques (the topological and the algebraic ) are not equivalent . We shall not formulate explicitly the algebraic technique in this paper.

In this paragraph we introduce the concept of universal covering of an entailment system.The idea is to “unfold” the category of deductions of the entailment to one that is actually the universal covering tree of them . The other aspects of the entailment system like the sorts and signatutes may not change. An additional technicality is that as the graph of the category of deductions of the entailment system may be non-connected the “lift” is for every connected component to its the universal covering tree and the “universal covering deduction category” is actually the free cartegory generated by the disjoint union of the (simply) connected universal covering trees thus a “forest” of trees .

a) The signatures are the same , the sets of sentences for each signature are all the subsets of all sentences of E (objects of the image of the functor sen ) of this signature .

b) The deduction category of is defined as following:Let all the subsets of the sentences of E,they are defined as the sentences of E’ . The entailment relation on all subsets of the sentences of is defined as the smallest extension to an entailment relation than includes the new deductions on the sentences of ,from the deduction of E. The extension of the entailment relation is defined explicitly as following: For any subset A of sentences of and any sentence a of it , we put AÃÄ a iff for every dÎa there is bÎA such that it holds b ÃÄ d in the entailment system of E .We notice that the sentences of are actually sets of sentences of the sentences of E .Thus it appears as a second Logical level or degree system .

Definition 4.2 : The entailment system E’ defined as before is called the derived entailment system of E .

Definition : A tree (forest )entailment system, is a Mesenquer entailment system E such that the category of deductions D(E’) is a the free category, that is generated by an oriented tree (forest) . The entailment system T is called connected iff the category D(E’) is a connected graph .

Remark: Let two entailment systems E_a and E_band their derived E_a’ and E_b’. Any morphism of the graphs of the deduction categories of the sentences of the derived systems ,D(P(sen_Ea))=D(E_a’) , D(P(sen_Eb))=D(E_b’) ,( where by P(x) we denote the power set of x) defines an entailment morphism of the derived entailment systems .The minimality of the extension of the entailment system in the derived ,gives that the graph D(E’) (actually a category ) defines completly the entailment system E, while the signatures are fixed . And any morphism between the derived entailment systems is projected directly to a morphism of the source entailment systems.And in addition any morphism of the two entailment systems E_a and E_bdefines a morphism of the derived systems .Actually the technique of the derived entailment system was introduced in order to have that (fixing the signature ) the entailment system E is completly determined by the deduction category D(E’) (also a graph ) of its derived entailement sets of sentences .

Definition 4.3 : A covering map f : E_a --> E_b between two entailment systems is a map of entailment systems such that the signatures are fixed ( the F is the identity functor ) and the continuous morphism which is extracted from the graph of the deduction category of the entailment systems real( D(P(sen_Ea)))=real(D(E_a’) to real(D(P(sen_Eb)))=real(D(E_b’) is a covering mapping of graphs .We say that the system E_a derives covering of the system E_b .We also say that the derived system E’_a covers the E’_b,or that the E’_a is a covering system of E_{b .}

Remark: Given a map of entailment systems f T_a --> T_b we extract a morphism of graphs from the graph D(P(sen_Ta))=D(T_a’ ) of the first system T_a to the D(P(sen_Tb))=D(_T’b) ,or of the graphs of the deductions systems of the derived systems .The fiber (inverse image ) of any vertice of D(P(sen_Tb))=D(T_b’ ) defines a partition on the set of vertices of D(T_a’ ) (the vertices of D(T_a’ ) are subsets of sentences ,of T_a) ,thus an equivalence relation .As the equivalence relation is one obtained by a system morphism it is a congruence R .If in addition the signatures of the system do not change (are the identity functor ) by the morphism f ,we can say that the system T_bis the quotient of the system T_a at the sentences under the congruence R and we write “T_a/R = T_b ” .

The Universal covering entailement system denoted by of the entailment system T is the system obtained from T such that the signatures are the same ,and the sets of sentences are the vertices of the universal covering of the graph D(P(sen_T))= D(T’) that is of the deduction category of the derived system . The category of deductions on all subsets of the sentences of is defined as the smallest extension of the entailment relation of T’ to an entailment relation (on ) than includes the new deductions on the new sentences introduced by the the .The extension of the entailment relation in is defined explicitly as following: For any subset A’ of sentences of C() =D() (where by C(G) we denote as we mentioned the free category of the graph G ) and any sentence a of we put A ÃÄ a if p(A) ÃÄ p(a) in the derived entailment system T’of T ,where p is the covering map p: ->D(T’) .We notice that the sentences of T’ and are actually sets of sentences of the sentences of T . Thus it seems as a second logical level or degree ,system.

We remark also that if the deduction category D(T’) is not a connected graph then we apply this process to each one of its connected components .

Definition 4.4 The entailment system defined as above is called universal covering system of T .

Theorem 4.5 (main result): Every entailment system has a universal covering entailment system .

Proof: We apply the theorem of the previous paragrapg that gives a universal covering forest to each graph .As the graph here we take the deduction graph of the derived system .The covering maps of the deduction graphs define covering maps of the entailment systems .QED

Theorem 4.6 Every entailment system E is isomorphic to a quotient system of a forest entailment system.

Proof: Direct from the previous theorem and the definition of quotient entailment system .

Theorem 4.7 There is forgetfull functor from the category of entailment systems E with arrows the covering maps, to the category of topological spaces (actually realisations of graphs) .

Proof:We correspond to each entailment system T the topological space real(D(T’)) .As we restrict from all entailement maps to covering entailment maps the corespondence preserves arrows and thus is functor .QED

Theorem 4.8 The universal covering entailment system of an entailment system T covers all other covering systems of the system T.

Proof:It holds as this holds for the universal covering topological spaces and due to the definition of the covering entailment maps .QED.

Corollary 4.9 The set of systems that cover a system admits the structure of a category with objects the systems and arrows the covering entailment maps such that the universal covering system is an initial object and arrows are the covering maps of entailment systems.

Proof: It holds as the universal covering space has the property to cover any other covering space , due to the definition of the covering entailment map and the choice opf the category with arrows only the covering entailment maps .An initial object in a category has arrows to all other objects in the category .QED.

Bibliography

[1] J. Goguen and R. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1): 95-146,1992.

[2] J. Lambek and P.J. Scott, Introduction to higher order categorical logic, Cambridge University Press 1986.

[3] J. Meseguer. General logics. In H.-D. Ebbinghaus et. al, editors, Logic Colloquim'87, pages 275-329. North-Holland,1989.

[6] J.A.Goguen. On Homomorphisms, Correctness, Termination, Unfoldments, and Equivalence of Flow Diagram Programs, Journal of Computer and System Sciences, pp. 333 - 365, Vol.8, No3, 1974.

[7] S. Mac Lane. Categories for the Working Mathematician, Graduate Texts in Mathematics 5, Springer-Verlag.

[10] J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96:73-155, 1992.

[11] R. Diaconescu. Category-Based Semantics For Equational and Constraint Logic Programming, D. Phil. Oxford University Computing Laboratory, Programming Research Group, 1994. Also, Technical Monograph PRG-116.

[1]Ph. D. Researcher, Software Engineering Laboratory, National Technical University of Athens

[2]Ph. D. Candidate, Department of Mathematics, National Technical University of Athens

v.3

universal coverings in the category of Meseguer's general logics

Costas Kyritsis[1] and Petros Stefaneas[2]

Bibliography