Theory 1 shows three axioms and two definitions, written in First Order Logic (FOL), that represents a fragment of a mereology theory. For this posting, it is important that the set of axioms is considered as a theory (i.e. a set of axioms together with theorems as a logical consequence of those axioms). In the context of this question, the particular axioms are not significant. Any other set of axioms forming a consistent theory would be equally acceptable.

Theory 1


Reflexivity $\forall x : part(x,x)$

Antisymmetry $\forall x \forall y : ((part(x,y) \land part(y,x)) \implies (x = y))$

Transitivity $\forall x \forall y \forall z :((part(x,y) \land part(y,z)) \implies part(x,z))$


Overlap : $\forall x,y \colon (overlap(x,y) \iff(\exists z \colon (part(z,x) \land part(z,y)))$

Proper Part : $\forall x,y \colon (proprPart(x,y) \iff (part(x,y) \land \neg part(y,x)))$

I am using CafeOBJ to represent the above logical axioms and definitions, shown in Listing 1:

Listing 1

   mod M{
    preds overlap part properPart : E E
 -- axioms
 ax [M1] : \A[x:E] part(x,x) .  
 ax [M2] : \A[x:E]\A[y:E] ((part(x,y) & part(y,x)) -> (x = y))  .
 ax [M3] : \A[x:E]\A[y:E]\A[z:E]((part(x,y) & part(y,z))  -> part(x,z)) .
 -- definitions
 ax [DM1] : \A[x:E]\A[y:E] (properPart(x,y) <-> (part(x,y) & ~(part(y,x)))) .  
 ax [DM2] : \A[x:E]\A[y:E] (overlap(x,y) <->  (\E[z:E] (part(z,x) & part(z,y)))) .  

Note that the logical theory is contained in a named module called M. The variables are over a domain of generic entities E, universal and existential quantification are denoted by \A[x:E] and \A[x:E] respectively. In CafeOBJ, named modules allow one to structure signatures, theories, sub/super theories, and models using the Theory of Institutions (TOI).

Below is my naïve attempt to present the axioms as a set of conceptual graphs (CG). My motivation for using CGs is that they provide an intuitive visualization of logic and have a direct relation to Common Logic (ISO zipped PDF).

enter image description here

The above CG was produced using CharGer software as Java zip file (manual).

My understanding of the above CGs is as follows:

  1. The variables are universally quantified, not default for CGs, but allowed in extended CG (ECG).
  2. The three graphs are all related by conjunction, which is default for GC.
  3. The arrow on graph representing reflexivity is bi-directional.
  4. Both antisymmetry and transitivity are represented by an IF-THEN contexts.
  5. Dotted lines are co-references.
  6. Equality (=) is actually commutative, but is represented as a directed relation .
  7. Each CG asserts a single proposition, labelled Proposition.


How do I present Theory 1 using CGs? Do I need some labeling that indicates that a set of concepts represent a theory. Or are theories represented by some enclosing special type of concept?

  • 1
    $\begingroup$ DOL project may be helpful omg.org/spec/DOL. see for ex. ![Annex I](i.stack.imgur.com/yYs5n.png) $\endgroup$ Jan 2, 2022 at 8:41
  • $\begingroup$ @Alex Thanks the link is useful, but I am more interested in FOL <-> CG mappings and model/theory representation using CGs. $\endgroup$ Jan 3, 2022 at 10:01
  • 1
    $\begingroup$ It seems that this post starts to become more complex. If you have multiple questions (even if they are related), I would recommend that you split them into multiple posts. $\endgroup$
    – nbro
    Jan 4, 2022 at 9:35
  • $\begingroup$ @nbro I have tried to simplify the question. $\endgroup$ Jan 8, 2022 at 10:41


You must log in to answer this question.

Browse other questions tagged .