# universal coverings in the category of Meseguer's general logics

## Costas Kyritsis and Petros Stefaneas

Abstract

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 . This is achieved by extending further Dana Scott's definition of entailment system and combining it with institutions of Goguen and Burstall . 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 . 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.

1. Introduction

1.1 Categorical logic

We follow J. Lambek and P. Scott  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 1a : 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:

f 1A = f = 1B f , (hg) f = h(gf)

1.2. General Logics

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.

This paper deals with systems of propositions  in the context of general logics.

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 . This is achieved by extending further Dana Scott's definition of entailment system and combining it with institutions of Goguen and Burstall . 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.

1.2.1 Entailment systems

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

Sign is a category whose objects are called signatures

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:

1.         reflexivity: for any f Îsen(S), {f} ÃÄ S f ,

2.         monotonicity: if G ÃÄ S f and G ' Ê G  then G'ÃÄ S f,

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

G ÃÄ S y,

4.         ÃÄ - translation: if G ÃÄ S f, then for any H: S ® S' in Sign,

sen(H)(G) ÃÄ S' sen(H)(f).

***

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

denoted by D(E) : an arrow a:x->y  belongs to D(E)  iff {x}ÃÄ y

(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) .

1.2.2 Institutions

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

Sign is a category whose objects are called signatures,

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

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

ÆÍ is a function associating to each S Î|Sign| a binary relation ÆÍS Í |Mod(S)| ´ sen(S) called S-satisfaction satisfying the following satisfaction condition for each S ® S' in Sign: for all M' Î|Mod(S)| and all f Îsen(S),

M' ÆÍS' sen(H)(f) ÛMod(H)(M') ÆÍS' f.

1.2.3 Logics

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:

(Sign, sen, ÃÄ) is an entailment system,

(Sign, sen, Mod, ÆÍ) is an institution,

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

G ÃÄS fÞ       G ÆÍS f

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

1.2.4 Map of entailment systems

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: Th0 ® Th0'satifying the following property:

G ÃÄ S Þ aS(G) ÃÄ' F(S,Æ) aS(f).

1.3 Graphs and Free Categories

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 .

2. Topological prerequisites

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

h(s)={f(2s) for sÎ[0,1/2] and g(2s-1) for sÎ[1/2, 1]

Definition Let X be a space ; let xo be a point of X .A  path in X that begins and ends at xo is called loop  based at xo . The set of path homotopy classes of loops based at x,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 xIt is denoted by p1(X, xo) .

Example

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  p1(X, xo) is the trivial (one-element) group for some xoÎX ,and hence for every xoÎ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  p1(V,b) into  p1(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 Va in E such that for each a , the restricion of p to Va  onto U is an     homeomorphism  .The collection { Va } 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 b0 ÎB .Given a subgroup H of p1(B,b0) ,there exists a path connected covering space p:E®B and a point e0 Î p-1 (b0) such that the induced homomorphism p* of the fundamental groups by the covering map ,gives p( p1(B,b0))=H .In particular B has a universal covering space(H={1}).

( The proof of this lemma is based also on Corollary 14.5 in  pp. 397).

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(e0) =b0 . Let f and g be two paths in B from  b0   to ; b1   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 .

3. Trees as universal covering topological spaces of  graphs.

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 ( pp. 14, 28).

First let us remember what is a  tree:

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 .

Definition 3.1

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.

Remark 3.2 Realization is a functor that commutes with direct limits .

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.

Proof:

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.

Example and Figure .

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 .

Example and figure

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 .

The concept of oriented tree is defined as following

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.

5. Universal coverings of entailment systems.

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  .

The derived system of a system  E is the system  obtained from E such that

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 .

Example

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 Ea and Eb   and their derived Ea’ and Eb’. Any morphism  of the graphs of the deduction categories of the  sentences of the derived systems ,D(P(senEa))=D(Ea’) , D(P(senEb))=D(Eb’) ,( 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 Ea and Edefines 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 : Ea --> Eb 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(senEa)))=real(D(Ea’)  to   real(D(P(senEb)))=real(D(Eb’) is a covering mapping of graphs .We say that the system  Ea derives covering of  the system  Eb  .We also say that the derived system E’a covers the E’b,or that the E’a is a covering system of    Eb  .

Remark: Given a map of entailment systems  f Ta --> Tb  we extract a morphism of graphs from the graph D(P(senTa))=D(Ta’ ) of the first system  Ta to the  D(P(senTb))=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(senTb))=D(Tb’ ) defines a partition on the set of vertices of D(Ta’ ) (the vertices of D(Ta’ ) are  subsets of sentences ,of Ta ) ,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 Tis the quotient of the system Ta at the sentences under the congruence R and we write “T/R = Tb  ” .

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(senT ))= 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 .

Example and figure

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

Example and figure .

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 .

QED

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

 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.

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

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

 J. P. Serre. Trees. Springer - Verlag.

 M. Barr and C. Wells. Toposes, Triples and Theories, Springer 1985.

 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.

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

 G. Graetzer. Universal Algebra, Second Edition, Springer 1979.

 J. Munkeres. Topology a first course, Prentice-Hall 1975.

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

 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.

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

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