key: cord-0060786-6q7rf6hu authors: Tiemens, Lucca; Scott, Dana S.; Benzmüller, Christoph; Benda, Miroslav title: Computer-Supported Exploration of a Categorical Axiomatization of Modeloids date: 2020-04-01 journal: Relational and Algebraic Methods in Computer Science DOI: 10.1007/978-3-030-43520-2_19 sha: 0babd70d93e1fc4470b3d12c9b91d0bd9293dfdf doc_id: 60786 cord_uid: 6q7rf6hu A modeloid, a certain set of partial bijections, emerges from the idea to abstract from a structure to the set of its partial automorphisms. It comes with an operation, called the derivative, which is inspired by Ehrenfeucht-Fraïssé games. In this paper we develop a generalization of a modeloid first to an inverse semigroup and then to an inverse category using an axiomatic approach to category theory. We then show that this formulation enables a purely algebraic view on Ehrenfeucht-Fraïssé games. Modeloids have been introduced by Benda [1] . They can be seen as an abstraction from a structure to a partial automorphism semigroup created in the attempt to study properties of structures from a different, more general angle which is independent of the language that is defining the structure. We do not follow Benda's original formulation in terms of an equivalence relation but treat modeloids as a certain set of partial bijections. Our recent interest in them was triggered by Scott's suggestion to look at the modeloidal concept from a categorical perspective. The new approach aims at establishing a framework in which the relationship between different structures of the same vocabulary can be studied by means of their partial isomorphisms. The overall project is work in progress, but as a first result we obtained a purely algebraic formulation of Ehrenfeucht-Fraïssé games. Throughout the project, computer-based theorem proving is employed in order to demonstrate and explore the virtues of automated and interactive theorem proving in context. The software used is Isabelle/HOL [13] in the 2019 Edition. We are generally interested in conducting as many proofs of lemmas and theorems as possible by using only the sledgehammer 1 command, and to study how far full proof automation scales in this area. Reporting on these practically motivated studies, however, will not be the focus of this paper. We only briefly mention here how we encoded, in Isabelle/HOL, an inverse semigroup and an inverse category, and we present a summary of our practical experience. Inverse semigroups (see e.g. [10] for more information) play a major role in this paper. They serve as a bridge between modeloids and category theory. The justification for this is given by the fact that an inverse semigroup can be faithfully embedded into a set of partial bijections by the Wagner-Preston representation theorem. This opens up the possibility of generalizing modeloids, which are sets of partial bijections, to the language of inverse semigroup theory. Once there, we have a natural transition from an inverse semigroup to an inverse category (for further reference see [12] ). We introduce the theory of inverse categories by an equational axiomatization that enables computer-supported reasoning. This serves as the basis for our formulation of a categorical modeloid. In each stage of generalization the derivative, a central operation in the theory of modeloids, can be adapted and reformulated. This operation is about extending the elements of a modeloid. Suppose that τ is a finite relational vocabulary meaning that τ consists only of finitely many relation and/or constant symbols. As it turns out, the derivative on a categorical modeloid on the category of finite τ -structures is equivalent to playing an Ehrenfeucht-Fraïssé game. This paper is organized in the following way. In Sect. 2 we define both modeloids and the derivative operation. We then turn to inverse semigroups in Sect. 3 and develop the axiomatization of a modeloid in inverse semigroup language. Section 4 shows how to represent a category in Isabelle/HOL and defines the categorical modeloid. After the derivative operation is established in this context, we give an introduction to Ehrenfeucht-Fraïssé games in Sect. 5 and present the close connection between the categorical derivative and Ehrenfeucht-Fraïssé games. Proofs for the stated theorems, propositions and lemmas are presented in the extended preprint [16] of this paper (cf. also [15] ); the Isabelle/HOL source files are available online. 2 Let us first recall the definitions of a partial bijection and of partial composition. A partial bijection f : X → Y is a partial injective function. The inverse of f , also a partial bijection and denoted by f −1 , is given by the preimage of the elements in the codomain of f : The composition between two partial functions f : X → Y and g : Y → Z is defined only on f −1 (dom(g) ∩ cod(f )). Then the partial composition Furthermore, let Σ be a finite non-empty set. We then define as the set of all partial bijections on Σ. As such, a modeloid is a set of partial bijections which is closed under composition and taking inverses, which has the identity on Σ as a member, and which satisfies the inclusion property. The inclusion property can be seen as a downward closure in regards of function restriction. In order to further illustrate the definition, we present a motivating example from model theory. The name modeloid originates from the above example since S is also called a model. For further motivation, background information and details on modeloids, we refer to Benda's paper [1] ; a nice example in there is the construction of a Scott Sentence presented through modeloidal glasses [1, p. 82] . We, on the other hand, turn to the core concept of the derivative which is defined in the following way. For convenience we represent a partial bijection as a set of tuples. is thus a set which only contains partial bijections that can be extended by an arbitrary element from Σ and which then still belong to M . This extension can take place either in the domain or in the range of the function. The next two results [1, Prop 2.3] provide some insight into why modeloids and the derivative operation are in harmony. The importance of these results is essentially due to the fact that they enable us to apply the derivative repeatedly. In this section we show how the Wagner-Preston representation theorem justifies our generalization of a modeloid to inverse semigroup language. We also discuss how well proof automation performs in the context of inverse semigroups. Some familiarity with the Isabelle/HOL proof assistant [3, 13] is assumed. We start with the equational definition of an inverse semigroup. [6] ). Let S be a set equipped with the binary operation * : S × S → S and the unary operation a → a −1 . (S, −1 , * ) is called an inverse semigroup if, and only if, it satisfies the axioms An inverse in semigroup theory is a generalization of the known group theoretical definition. This generalized definition does not depend on a specified unique neutral element. Intuitively, it can be thought of as the inverse map of a partial bijection. Let (S, * ) be a semigroup and x ∈ S. Then y ∈ S is called an inverse of x if, and only if, x * y * x = x and y * x * y = y. We encode an inverse semigroup as follows in Isabelle/HOL. The domain for individuals is chosen to be a, which is a type variable. This means we have encoded a polymorphic version of inverse semigroups. Using this implementation almost all results needed for proving the Wagner-Preston representation theorem, which we will discuss shortly, can be found by automated theorem proving. Occasionally, however, some additional lemmas to the ones usually presented in a textbook (e.g. [10] ) are needed. By automated theorem proving we here mean the use of sledgehammer [3] for finding the proofs of the given statements without any further interaction. Regarding equivalent definitions of an inverse semigroup, we were able to automate the proofs of the following theorem (except for 2. ⇒ 1., which is due to a Skolemization issue). ). Let (S, * ) be a semigroup. Then the following are equivalent: Our experiments confirm that automated theorem proving (and also model finding) can well support the exploration of an axiomatic theory as presented. However, the intellectual effort needed to model and formulate the presented mathematics in the first place is of course still crucial, and a great deal of work has gone into this intuitive aspect of the development process. A more technical challenge also is to find suitable intermediate steps that can be proven automatically by sledgehammer. We now show that every modeloid M ⊆ F (Σ) under partial composition is an inverse semigroup. We make use of Theorem 1 by using the third characterization. For this task regard (M, •) as a semigroup. This is clear since composition of partial functions is associative. Since the partial identities of M are exactly the idempotent elements in (M, •), commutativity is ensured by referring to the next proposition. Furthermore, also by using the next proposition, the closure of taking inverses required by a modeloid implies regularity for all elements in M . Hence, (M, −1 , •) is an inverse semigroup. ). Let f : X → Y be a partial bijection. 1. For a partial bijection g : Y → X, the equations f = fgf and g = gf g hold if, and only if, Not only is every modeloid an inverse semigroup, but by the Wagner-Preston representation theorem also every inverse semigroup can be faithfully embedded into F (Σ), which is itself a modeloid. This motivates the idea of formulating the axioms for a modeloid in inverse semigroup language. Our aim is to restate the derivative operation in this context. In order to achieve this, we shall translate the axioms from Definition 2, examining them one by one. 1. Closure of Composition: Because of the embedding, the composition of partial functions will simply be the * -operation in an inverse semigroup. 2. Closure of taking inverses: By Theorem 1 an inverse semigroup is such that the inverse exists for every element and is unique, hence resembling the inverses of partial functions and in particular the closure property. 3. The inclusion property: Here it is not immediately apparent how this can be expressed within an inverse semigroup. We shall see that the natural partial order is capable of doing that. 4. The identity on Σ: The identity is a certain idempotent element in an inverse semigroup. It will lead us to the notion of an inverse monoid. It is Axiom 3 that we focus our attention on next. We define the natural partial order and present the Wagner-Preston representation theorem, which establishes a connection to function restriction in F (Σ). We introduce notation for such a restriction. For two partial functions f, g we write g ⊆ f to say that Definition 6 (Natural partial order). Let Σ = (Σ, −1 , * ) be an inverse semigroup and s, t ∈ Σ. Then we define for some idempotent e ∈ Σ s ≤ t :⇔ s = t * e. From this theorem it is clear what we mean by a faithful embedding of an inverse semigroup into the set of partial bijections F (Σ). Faithfulness corresponds to the fact that the natural partial order in light of the representation theorem is equivalent to the partial order which function restriction defines. This nicely opens up the possibility to capture the essence of the inclusion property from Definition 2 by the natural partial order. Let M ⊂ S, where S is an inverse semigroup. Then the inclusion property can be stated as (2) By setting S = F (Σ), the dependency of M on F (Σ) can be seen explicitly. In the abstract formulation of a modeloid we will keep this subset property. It is immediate that a modeloid, seen as an inverse semigroup, fulfills (2) by the following proposition. In a modeloid M the inclusion property implies that the empty partial bijection, which we denote by 0, is also included in M . As a result we want to establish a similar behavior in the generalized modeloid. The deeper reason for this is found in the definition of the derivative operation, because it requires the notion of an atom, which can only be defined if a zero element is present. Seeing M as an inverse semigroup, 0 is an idempotent element for which the following property holds: ∀x ∈ M : 0 * x = 0. Hence, we will call the idempotent with this property the zero element. When defining a modeloid in semigroup language we require the zero element to be part of it. Turning to Axiom 4, which is id Σ ∈ M , we examine which element of an inverse semigroup S is most suitable for this task. To evaluate, we again look at the modeloid M as an inverse semigroup. In this semigroup, id Σ will be an idempotent e satisfying ∀x ∈ M : e * x = x. Such an element is known as a neutral element in the context of group theory. We require for the inverse semigroup, which we eventually call a modeloid, that e is part of it. What we get is known as an inverse monoid in the literature. Given an inverse monoid, denoted by S 1 , and the element e with e * x = x, ∀x ∈ S 1 . Consider the representation theorem again: this theorem is not guaranteeing uniqueness of the embedding, and in fact there can be several ones. Hence, we cannot assume that e will be mapped to the identity id Σ . However, for all idempotent f ∈ S 1 we have that f ≤ e because f = e * f by the assumption about e. Hence, e is always the upper bound of all idempotents in S 1 . We have prepared everything needed for defining a modeloid again. We shall call it a semimodeloid. Note, as mentioned before, that a modeloid is a subset of F (Σ) for some non-empty set Σ and, as discussed, we keep this subset property to state the inclusion axiom. A semimodeloid is again an inverse monoid with the zero element. Furthermore, by the considerations above, every modeloid is a semimodeloid. Now we develop the derivative operation in the setting of a semimodeloid. Consider again Definition 3 in which we have introduced the derivative operation. It is evident that the elements of Σ are of crucial importance. Furthermore, we are required to be able to extend the domain of a function by one element at a time. This poses a challenge because in an inverse monoid this information is not directly accessible. But as we shall see, it is possible to obtain. First we characterize the elements of Σ. Therefore, consider F (Σ) and realize that all the singleton-identities id {a} , for a ∈ Σ, are in natural bijection to the elements of Σ. The special property of such a singleton-identity is Seeing F (Σ) as an inverse monoid with zero element leads to the following definition. Our plan is to use the notion of an atom to define the derivative. The next lemma justifies this usage. This suffices to define the derivative for semimodeloids. We then ensure that the definition matches Definition 3 if the semimodeloid is on F (Σ). If we think about x in the above definition as a partial bijection, then x −1 x is the identity on the domain of x and, hence, the condition a ≤ x −1 x expresses that a is in the domain of x. Similarly b ≤ yy −1 states that b is in the range of y. We use an axiomatic approach to category theory based on free logic [8, 9, 14] . As demonstrated by Benzmüller and Scott [2] , this approach enables the encoding of category theory in Isabelle/HOL. Their encoding work is extended below to cover also inverse categories. Subsequently we formalize modeloids and derivatives in this setting. When looking at the definition of a category C, one can realize that the objects A, B, C, .. are in natural bijection with the identity morphisms 1 A , 1 B , 1 C , . .. because those are unique. This enables a characterization of a category just by its morphisms and their compositions, which is used to establish a formal axiomatization. However, in this axiomatic approach we are faced with the challenge of partiality, because the composition between two morphisms f, g ∈ C is defined if, and only if, dom(g) = cod(f ). As a result composition is a partial operation. An elegant way to deal with this issue is by changing the underlying logic to free logic. In free logic an explicit notion of existence is introduced for the objects in the domain that we quantify over. In our case the domain consists of the morphisms of a category. The idea now is to define the composition total, that is, any two morphisms can always be composed, but only those compositions "exist" that satisfy (4). Because we can distinguish between existing and non-existing morphisms, we are able to formulate statements that take only existing morphisms into account. In this paper we want to work with a unique non-existing morphism which will be denoted by . Hence a composition of morphisms, that does not satisfy (4), will result in . We refer to Benzmüller and Scott [2] for more information on the encoding of free logic in Isabelle/HOL. Based upon this groundwork, a category in Isabelle/HOL is defined as follows. For convenience, we will assume a category to be small for the rest of this paper. As a result, a category for us has only a set of morphisms which satisfies the above axiom schema. This allows us to use notation from set theory. We write (m : X → Y ) ∈ C to mean that m is a morphism from the category C. In addition, it says that dom(m) ∼ = X and cod(m) ∼ = Y , so X is the domain of m and Y the codomain. The identity morphisms X and Y , which are representing objects in the usual sense, are characterized by the property that X ∼ = dom(X) ∼ = cod(X), respectively for Y . Hence every c ∈ C satisfying c ∼ = dom(c) or c ∼ = cod(c) is representing an object, and we refer to such a morphism as an object. We want a categorical generalization of an inverse semigroup, so let's turn to the question of how to introduce generalized inverses to a category. In the above setting we found that by adding the axioms of an inverse semigroup, which are responsible for shaping these inverses (Definition 4, Axioms 2-4), we arrive at a notion that is equivalent to the usual definition of an inverse category. Note that this definition is adopted to our free logic foundation by using Kleene equality, which is denoted by ∼ =. We emphasize again that this equality between terms states that, if either term exists, so does the other one and they are equal. Definition 10 (Inverse category [7] ). A small category C is called an inverse category if for any morphism s : X → Y ∈ C there exists a unique morphismŝ s : Y → X such that s ∼ = s ·ŝ · s andŝ ∼ =ŝ · s ·ŝ. For the representation in Isabelle/HOL we skolemized the definition. Next, we see the quantifier free definition. The equivalence between the two formulations has been shown by interactive theorem proving. Again, a significant number of the required subproofs could be automated by sledgehammer. In addition, the minimality of the axioms for the quantifier free version above was checked effectively using sledgehammer and nitpick 3 . Inverse categories are interesting to us because of the following proposition. This allows us to generalize a semimodeloid to an inverse category by formulating the new axioms in such a way that this categorical construction will collapse to a semimodeloid under the condition of having just one object. The notion of the natural partial order is also definable in an inverse category. To state it, we first introduce a definition for idempotence. e · e ∼ = e. Whenever we do not assume that both sides of the equation exist, we use Kleene equality. Definition 12 (Natural partial order [12] ). Let C be an inverse category and let s, t : X → Y be morphisms in C. We define where End C (X) := {m ∈ C | m : X → X} is called an endoset. When defining a categorical modeloid M on an inverse category C, we will see that for each object X in C, End C (X) is a semimodeloid. We require the category to have a zero element in each of its endosets in order to define an atom. For this we simply write that C has all zero elements. Let C be an inverse category with all zero elements. Then a categorical modeloid M on C is such that M ⊆ C satisfies the following axioms: It is evident that this definition is close by its appearance to a semimodeloid. However, we are now dealing with a network of semimodeloids and have thus reached a much more expressive definition. M be a categorical modeloid on C. Then for each object X in M we get that End M (X) is a semimodeloid (on itself ). Remark 3. Every semimodeloid can easily be seen as a categorical modeloid by the fact that an inverse monoid with zero element is an one-object inverse category. We have formulated a generalization of a modeloid in category theory. What is left now is to define the derivative in this context. We will need the notion of a homset and of an atom, which we already introduced for semigroups. Let C be a small category. Then the homset between two elements X, Y ∈ C, satisfying X ∼ = dom(X) and Y ∼ = dom(Y ), is defined as Hence an endoset is a special case of a homset. We only assume zero elements to be present in endosets and as a result an atom needs to be part of an endoset. Then an element a ∈ End C (X), for some object X ∈ C, is an atom if, and only if, the existence of a implies that a is not the zero element and This concludes the preliminaries for defining the derivative on a homset. Let C be an inverse category with just one object X and a zero element. Then C is an inverse semigroup by Proposition 6 and the derivative on the homset D(Hom C (X, X)) is equal to the semimodeloidal derivative D(C). Now the key property of this operation is that it produces a categorical modeloid again if we apply it to all homsets simultaneously. is a categorical modeloid on C. As a result we define this to be the derivative operation on categorical modeloids. for n ∈ N. D m (M ) thus takes the derivative m-times. This notion is used in the next section. When moving from classical model theory to the finite case, some machinery for proving inexpressibility results in first-order logic, such as the compactness theorem, fails. However, Ehrenfeucht-Fraïssé (EF) games are still applicable and, therefore, play a central notion in finite model theory due to the possibility to show that a property is first-order axiomatizable. For more information see [11] . In this section we explicitly show that derivatives on categorical modeloids generalize EF games. To play an EF game, two finite τ -structures A and B, where τ is a finite relational vocabulary, are needed. In general EF games are not restricted to finite structures, but for our purpose we shall only deal with this case. In order to give an intuitive understanding we imagine two players, which we call the spoiler and the duplicator, playing the game. The rules are quite simple. In n ∈ N rounds the spoiler tries to show that the two given structures are not equal, while the duplicator tries to disprove the spoiler every time. A round consists of the following: -The spoiler picks either A or B and then makes a move by choosing an element from that structure, so a ∈ A or b ∈ B. -After the spoiler is done, the duplicator picks an element of the other structure and the round ends. Next we define what the winning condition for each round will be. For convenience let P art(A, B) be the set of all partial isomorphisms from A to B. Furthermore, given a constant symbole c from τ , we denote by c A the interpretation of c in the structure A. Definition 18 (Winning position [11] ). Suppose the EF game was played for n rounds. Then there are moves (a 1 , .., a n ) picked from A and moves (b 1 , .., b n ) picked from B. For this to be a winning position we require that for some r ∈ N the map In order to win, the duplicator needs to defeat the spoiler in every possible course of the game. We say the duplicator has an n-round winning strategy in the Ehrenfeucht-Fraïssé game on A and B [11] , if the duplicator is in a winning position after n moves regardless of what the spoiler does. This is made precise by the back-and-forth method due to Fraïssé. Definition 19 (Back-and-forth relation [5] ). We define a binary relation ≡ m , m ∈ N, on all τ -structures by A ≡ m B iff there is a sequence (I j ) for 0 ≤ j ≤ m such that -Every I j is a non-empty set of partial isomorphisms from A to B -(Forth property) ∀j < m we have ∀a ∈ A ∀f ∈ I j+1 ∃g ∈ I j : f ⊆ g ∧ a ∈ dom(g) -(Back property) ∀j < m we have ∀b ∈ B ∀f ∈ I j+1 ∃g ∈ I j : f ⊆ g ∧ b ∈ cod(g) Hence A ≡ n B means that the duplicator has a n-round winning strategy. We relate the categorical derivative to Fraïssé's method which we have just seen. In order to do this, we define a categorical modeloid on the category of finite τ -structures, where τ is a finite relational vocabulary. For that let A and B be two finite τ -structures. Denote by F (A, B) We construct two functions dom : C → C and cod : C → C such that for a partial isomorphism f : X → Y ∈ F (A, B) we set dom(f ) = id X and cod(f ) = id Y , and for the element we define dom( ) = and cod( ) = . Next we define a binary operation · : C → C by where • denotes the composition of partial functions. What we have just seen provides a general procedure for creating categories in our setting, which is founded on a free logic that is itself encoded in Isabelle/HOL. Corollary 1. D := (C, dom, cod, ·, , −1 ) is also a categorical modeloid on itself. Remark 5. Hence we have that every inverse category having a zero element for each of its endosets is also a categorical modeloid and thus admits a derivative. At this point we are able to use the derivative on D. The final theorem draws the concluding connection between modeloids and Fraïssé's method. We show that in the established setting, an m-round winning strategy between A and B is given by the sets which the derivative produces if applied m times. Note the abuse of notation in the way we are using ≡ m here. As a result the derivative on this modeloid is equivalent to playing an EF game between the two structures. Hence on an arbitrary categorical modeloid the derivative can be seen as a generalization of EF games. In this paper we have shown how to arrive at the notion of a categorical modeloid using axiomatic category theory. We started out with a set of partial bijections abstracting from a structure, then we interpreted this set as an inverse semigroup by the embedding due to the Wagner-Preston representation theorem, and, finally, we were able to axiomatize a modeloid in an inverse category. The key feature we employed is the natural partial order which also enabled us to present the derivative operation in each step of abstraction. The categorical derivative on the category of finite structures of a finite vocabulary can then be used to play Ehrenfeucht-Fraïssé games between two structures. As a result a more abstract representation of these games is possible. Using our encoding of inverse categories in Isabelle/HOL, we are currently extending this encoding work to cover also categorical modeloids and their derivatives. This naturally extends the framework established by Benzmüller and Scott so far [2] . Furthermore, an investigation of the generalized Ehrenfeucht-Fraïssé games in terms of applicability has to be conducted. We believe that the notion of a categorical modeloid will continue to play a role when connecting model theoretical and categorical concepts. Automating free logic in HOL, with an experimental application in category theory Extending sledgehammer with SMT solvers Nitpick: a counterexample generator for higher-order logic based on a relational model finder Finite Model Theory Fundamentals of Semigroup Theory Inverse categories. Algebraische Modelle, Kategorien und Gruppoide The definition of e! in free logic Free Logic: Selected Essays Elements of Finite Model Theory On inverse categories and transfer in cohomology Isabelle/HOL: A Proof Assistant for Higher-Order Logic Existence and description in formal logic Computer-supported Exploration of a Categorical Axiomatization of Miroslav Benda's Modeloids. Bachelor's thesis Computer-supported exploration of a categorical axiomatization of modeloids We wish to thank the anonymous referees for their helpful comments and suggestions.