### From OntologPSMW

A formal ontology is a software artifact that captures intuitions about the world in a formal language. The following definition is adapted from Guarino (1998).
(1A)

An Ontology, Ok, is a set of logical formulae in some language L that aim
to capture the intended models of a particular conceptualization, C. The
language L consists of a set of logical symbols (i.e. and, not, exists etc.),
and a set of non-logical symbols which we refer to as the vocabulary, V which
consists of at least of variables and relations. A model for an ontology is
constructed via an interpretation I, assigning to each element of the vocabulary
V to the extensional structure of the conceptualization, S = {D,R} and thus to
either elements of the domain D or the conceptual relations R.
(1B1)

Occasionally, the labels "theory" or "set of axioms" may refer equivalently to a formal ontology. Moreover, some languages support the notion of a "module" which is a set of axioms. Similarly, "module" may also refer to an ontology. (1B2)

A very simple ontology written in the Common Logic Interchange Format might be one for partially ordered sets. It consists of three axioms collected as a single module, named poset.
(1C1)

(cl-module (poset) (forall (x) (leq x x) ) (forall (x y) (if (and (leq x y) (leq y x)) (x = y) ) ) (forall (x y z) (if (and (leq x y) (leq y z)) (leq x z) ) ) ) (1C2)

In the example above, the module or ontology or theory for "poset" was written in L = Common Logic. The vocabulary consisted of three variables: x, y, and z and one relation, "leq" (less than or equal to). Moreover, the ontology comprised of three axioms specifying Reflexivity, Anti-Symmetry and Transitivity which constrain which models are admissible for the ontology. (1C3)

The following are some valid models which satisfy the poset ontology (set of axioms):
(1C4)

Model 1: Domain D: { Natural Numbers } (i.e. 1, ... , infinity) Relations R: { (1 leq 2), (2 leq 2) } (1C5)

Model 2:
Domain D: { 100 }
Relations: { ( 100 leq 100 }
(1C6)

Model 3:
Domain D: { -5, 1.1, 200, 18 }
Relations: { (-5 leq 1.1), (-5 leq 18), (1.1 leq 200), (1.1 leq 1.1), .... }
(1C7)

The following are models that are ruled out:
(1C9)

Not_Model 2:
Domain D: { 1, ..., 2000000000}
Relations: { (1 leq 1), (1 leq 2), (3 leq 1)}
(1C11)