This work focuses on the de nition of a consequence relation between contexts with which we can decide whether certain contextual information is a logical consequence from a set of contexts considered as underlying hypotheses.
In real life, one often faces situations in which the underlying knowledge is given as a set of tables which can be interpreted as formal contexts, and we should decide on whether certain contextual information is a consequence from them.
This problem clearly resembles the notion of a formula being a logical consequence of a set of hypotheses, and suggests the possibility or convenience of de ning a formal (mathematical) notion of logical consequence between contexts.
The only attempts to introduce logical content within the machinery
of Formal Concept Analysis (FCA), apart from its ancient roots anchored
in the Port-Royal logic, are the so-called logical information systems and
the logical concept analysis [
Of course, di erent links between FCA and logic have been studied
but, to the best of our knowledge, the problem considered in this paper has
not been explicitly studied in the literature. Nevertheless, it is worth to
remark that the concluding section of [
In the present work, we consider the fact that the category ChuCors of contexts and Chu correspondences is *-autonomous, and hence a model of linear logic, in order to build some preliminary links with the conjunctive fragment of this logic. ? Partially supported by grants VEGA 1/0073/15 and APVV-15-0091 ?? Partially supported by Spanish Ministry of Science project TIN2015-70266-C2-1-P, co-funded by the European Regional Development Fund (ERDF)
In order to make the manuscript self-contained, the fundamental notions and their main properties are recalled in this section. 2.1
De nition 1. A formal context is any triple C = hB; A; Ri where B and A are nite sets and R B A is a binary relation. It is customary to say that B is a set of objects, A is a set of attributes and R represents a relation between objects and attributes.
Given a formal context hB; A; Ri, the derivation (or concept-forming) operators are a pair of mappings " : 2B ! 2A and # : 2A ! 2B such that if X B, then "X is the set of all attributes which are related to every object in X and, similarly, if Y A, then # Y is the set of all objects which are related to every attribute in Y .
De nition 2. A formal concept of a formal context C = hB; A; Ri is a pair of sets hX; Y i 2 2B 2A which is a xpoint of the pair of conceptforming operators, namely, " X = Y and # Y = X. The object part X is called the extent and the attribute part Y is called the intent. The set of all formal concepts of a context C will be denoted by CL(C), set of all extents or intents of C will be denoted by Ext(C) or Int(C) respectively. 2.2
Two main constructions have been traditionally considered in order to relate two formal contexts: the bonds and the Chu correspondences. De nition 3. Let C1 = hB1; A1; R1i and C2 = hB2; A2; R2i be two formal contexts. A bond between C1 and C2 is any relation 2 2B1 A2 such that, when interpreted as a table, its columns are extents of C1 and its rows are intents of C2. All bonds between such contexts will be denoted by Bonds(C1; C2).
Another equivalent de nition of bond between C1 and C2 de nes it as any relation 2 2B1 A2 such that Ext(hB1; A2; i) Ext(C1) and Int(hB1; A2; i) Int(C2)
Dual bonds between C1 and C2 are bonds between C1 and transposition of C2. Transposition of any context C = hB; A; Ri is de ned as a new context C = hA; B; Rti with Rt(a; b) holds i R(b; a) holds.
The notion of Chu correspondence between contexts can be seen as an alternative inter-contextual structure which, instead, links intents of C1 and extents of C2.
De nition 4. Consider C1 = hB1; A1; R1i and C2 = hB2; A2; R2i two formal contexts. A Chu correspondence between C1 and C2 is any pair ' = h'L; 'Ri of mappings 'L : B1 ! Ext(C2) and 'R : A2 ! Int(C1) such that for all (b1; a2) 2 B1 A2 it holds that "2 'L(b1) (a2) = #1 'R(a2) (b1).
All Chu correspondences between such contexts will be denoted by Chu(C1; C2).
The notions of bond and Chu correspondence are interchangeable; speci cally, we can consider the bond ' associated to a Chu correspondence ' from C1 to C2 de ned for b1 2 B1; a2 2 A2 as follows '(b1; a2) = "2 'L(b1) (a2) = #1 'R(a2) (b1) Similarly, we can consider the Chu correspondence ' associated to a bond de ned by the following pair of mappings: ' L(b1) = #2 (b1) ' R(a2) = "1 t(a2) for all a2 2 A2 and o1 2 B1
The set of all bonds (resp. Chu correspondences) between two formal contexts endowed with the ordering given by set inclusion is a complete lattice. Moreover, both complete lattices are dually isomorphic. 2.3
Recall that it is possible to consider a category in which the objects are
formal contexts and morphisms between two contexts are the Chu
correspondences between them. This category, denoted ChuCors, has been
proved to be *-autonomous and equivalent to the category of complete
lattices and isotone Galois connections, more results on this category and
its L-fuzzy extensions can be found in [
Cartesian product in ChuCors The following de nition provides a speci c construction of the notion of (binary) cartesian product in the category ChuCors.
De nition 5. Consider C1 = hB1; A1; R1i and C2 = hB2; A2; R2i two formal contexts. The product of such contexts is a new formal context C1 C2 = hB1 ] B2; A1 ] A2; R1 2i where the relation R1 2 is given by ((i; b); (j; a)) 2 R1 2 if and only if (i = j) ) (b; a) 2 Ri for any (b; a) 2 Bi
Aj and (i; j) 2 f1; 2g f1; 2g.
If we recall the well-known categorical theorem which states that if a category has a terminal object and binary product, then it has all nite products, we need to prove just the existence of a terminal object (namely, the nullary product) in order to prove the category ChuCors to be Cartesian.
Any formal context of the form hB; A; B Ai where the incidence relation is the full Cartesian product of the sets of objects and attributes is (isomorphic to) the terminal object of ChuCors. Such a formal context has just one formal concept hB; Ai; hence, from any other formal context there is just one Chu correspondence to hB; A; B Ai.
The explicit construction of a general product (not necessarily either binary or nullary) is given below: De nition 6. Let fCigi2I be an indexed family of formal contexts Ci = hBi; Ai; Rii, the product Qi2I Ci is the formal context given by * Y Ci = i2I ] Bi; ] Ai; R I i2I i2I + where (k; b); (m; a) 2 R I , (k = m) ) (b; a) 2 Rk .
It is worth to note that the arbitrary product of contexts commutes with both the concept lattice construction and the bonds between contexts. These two results are explicitly stated below.
Lemma 1. Let Ci = hBi; Ai; Rii be a formal context for i 2 I. It holds that CL(Qi2I Ci) is isomorphic to Qi2I CL(Ci).
Lemma 2. Let I and J be two index sets, and consider the two sets of formal contexts fCigi2I and fDj gj2J . The following isomorphism holds Bonds Y Ci; Y
Dj i2I j2J =
Y (i;j)2I J
Tensor product Another product-like construction can be given in the category ChuCors.
Note that if ' 2 Chu(C1; C2), then we can consider ' 2 Chu(C2 ; C1 ) de ned by 'L = 'R and 'R = 'L.
De nition 7. The tensor product C1 C2 of contexts Ci = hBi; Ai; Rii for i 2 f1; 2g is de ned as the context hB1 B2; Chu(C1; C2 ); R i where R
(b1; b2); ' = #2 'L(b1) (b2):
The properties of the tensor product were shown in [
Due to the monoidal properties of on ChuCors we can add a notion of n-ary tensor product of n formal contexts in=1Ci of any n formal contexts Ci for i 2 f1; : : : ; ng. Hence, it is possible to consider a notion of n-ary bond that we can imagine as any extent of n-ary tensor product. De nition 8. Let Ci = hBi; Ai; Rii be formal contexts for i 2 f1; : : : ; ng. A dual n-ary bond between fCigin=1 is an n-ary relation Qin=1 Bi such that for all i 2 f1; 2; : : : ; ng and any (b1; : : : ; bi 1; bi+1; : : : ; bn) 2 Qn j=1;j6=i Bi it holds that
(b1; : : : ; bi 1; ( ); bi+1; : : : ; bn) 2 Ext(Ci) : Lemma 4. Let fC1; : : : ; Cng be a set of n formal contexts and be some n-ary bond between such contexts. Let Di be a new formal context dened as hBi; Qn
j=1;j6=i Bj ; Rii where Ri(bi; (b1; : : : ; bi 1; bi+1; : : : ; bn)) = (b1; : : : ; bn) for any i 2 f1; 2; : : : ; ng. Then Ext(Di ) Ext(Ci). 3
One of the main di erences between linear and classical logic is the coexistence of two di erent conjunctions in linear logic, in both cases the underlying semantics is that two actions are possible, or can be executed, but the di erence relies on how these actions are actually performed: on the one hand, we have the multiplicative conjunction (times) which expresses that both actions will be performed; on the other hand, the additive conjunction & (with) states that, although both actions are possible, actually just one will be performed. 3.1
The categorical product on ChuCors plays the role of additive conjunction &. Recall that the product C1 C2 is de ned as hB1]B2; A1]A2; R1 2i where R1 2(b; a) = (i = j) ) (b; a) 2 Ri for all b 2 Bi and a 2 Aj for all i; j 2 f1; 2g.
The semantics of the additive conjunction is that, in order to perform the action of C1 C2, we have rst to choose which among the two possible actions we want to perform, and then to do the one selected. And this is exactly what happens here. From the previous section about the categorical product of ChuCors, it is known that a concept lattice of a product of formal contexts is equal to a product of concept lattices of the input formal contexts. Hence no interaction or parallel action of input formal contexts occurs in case of the categorical product. 3.2
Any dual bond between two formal contexts C1 and C2 plays a role of multiplicative conjunction . From the de nition of bonds one can see the parallelism of use of input contexts, where every value in the bond, as a relation, is from both extents of input contexts.
The existing isomorphism between Chu correspondences and bonds, and monoidal properties of Chu correspondences which follows from the fact that Chu correspondences form a category, bonds satis es all properties of conjunction.
In the sense of category theory, any dual bond can be seen as a Galois connection between concept lattices of their input contexts, because of the categorical equivalence between category ChuCors and the category of complete lattices and isotone Galois connections.
In [
The idea here is to develop a logic between contexts and, speci cally, a proof theory for this logic.
We will consider the problem of de ning a consequence relation j= which allows for developing formally a sequent calculus between contexts. De nition 9. Two contexts C and D are isomorphic if their concept lattices are isomorphic.
De nition 10. Given formal contexts C1; : : : ; Cn; C, we say that C is a consequence of contexts C1; : : : ; Cn, denoted as C1; : : : ; Cn j= C, if C is isomorphic to a bond between all contexts in the left hand side. Speci cally, C1; : : : ; Cn j= C if and only if C is isomorphic to some n-ary bond between input formal contexts C1; : : : ; Cn.
The relation just de ned satis es the properties of closure operator and, hence, can be considered as a relation of logical consequence between contexts, since any consequence relation can be viewed as a nitary closure operator on a set (of sentences or formulas).
Lemma 5. The relation j= above is a consequence relation.
Recall the notion of sequent of Gentzen calculus. Any sequent is of the form ` and has the following meaning: from the conjunction of all hypothesis of follows some formula of . Hence as a conjunction of all contexts we use some n-ary bond between input contexts.
Without entering into the details, the following sequent rules from conjunctive linear logic can be proved in terms of this de nition. Axiom rule: As a unary bond we use a context itself Constants rule Due to isomorphism Bonds (C; >) = Ext(C) where > = hf g; f g; 6=i we can write the following rule
C j= C
C1; : : : ; Cn j= C >; C1; : : : ; Cn j= C -left From the de nition of j= and associativity of tensor product, or of associativity inside of n-ary product, we can write -left Due to the distributivity of tensor and categorical product on formal contexts, n-ary bond between C1; : : : ; Cn 1; Cn
product of n-ary bonds between C1; : : : ; Cn 1; Cn and C1; : : : ; Cn 1; D. Hence it is easy to use a full relation as the n-ary bond between
-right One of the possibilities here is to add to hypothesis a special context, product of two singletons > >. We have obtained a preliminary notion of logical consequence relation between contexts which, together with the interpretation of the multiplicative (resp. additive) conjunction as the cartesian product (resp. bond) of contexts, enable to prove the correctness of the corresponding rules of the sequent calculus of the conjunctive fragment of linear logic.
Of course, we are just scratching the surface of the problem of providing a full calculus since we still need to nd the adequate context-related constructions to interpret the rest of connectives. This is future work.