The Mereology Theory below contains three first-order axioms that represent a part of a mereology theory. For this posting, it is important that the set of axioms should be considered as a theory.
Mereology Theory
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))$
Here is my naïve attempt to present the theory as a set of conceptual graphs (CG).
My understanding of the above CGs is as follows:
- The variables are universally quantified, not default for CGs, but allowed in extended CG (ECG).
- The inner graphs are all related by conjunction, which is default for GCs and I assume for ECGs.
- The arrow on graph representing reflexivity is bi-directional.
- Both antisymmetry and transitivity are represented by an IF-THEN contexts.
- Dotted lines are co-references.
- Equality (=) is actually commutative, but is represented as a directed relation .
- Each inner graph asserts a single proposition, labelled Proposition.
- The outer graph is labeled MereologyTheory, I am not sure that this is correct ECG syntax.
Below is a possible model of the above theory:
Mereology Model Mathematical notation
$Entities = \{ a,b \}$
$Relations = \{part(a,a),part(a,b),part(b.b)\}$
Obviously there are many other possible models. MereologyModel below is my attempt to visualize this model as a CG. I am not sure that putting the label MereologyModel is correct CG syntax or denotes it as a model of MereologyTheory .
Question:
In CG visual notation, how are theories and models related? It seems to me that basic CGs can represent FOL sentences and the relation between such sentences. According to Chein and Mugnier the subsumption relation is defined by graph homomorphisms between CGs. Is the model/theory relation for CGs also defined in terms of graph homomorphisms? I am aware that in general a model satisfies a theory i.e. $M \vDash T$. Does the graph homomorphism provide the necessary syntactic mapping to enable model and theory to be related?
Note CGs can be represented in Common Logic (ISO zipped PDF), which would permit a formal proof that all the axioms of the theory are satisfied in the model.